# iLTL Checker

iLTL is a Linear Temporal Logic (LTL) that can specify temporal changes of expected rewards of a Markov process. Given the Markov chain representation of a system, the iLTL checker verifies whether an iLTL formula holds for the system.

iLTL captures the frequency interpretation of probability in large scale systems. Consider the following simple example: suppose that there is a Discrete Time Markov Chain (DTMC) of two states, say \(\{a, b\}\), and two transitions to other states with probability one. Suppose also that a predicate \(\alpha\) is true in \(a\) but not in \(b\). Because, this DTMC alternates states in every step, there is no path with consecutive sequences of a state. However, suppose that there are 100 nodes, initially 50 in state \(a\) and 50 in state \(b\). Then there are always 50% of the nodes in state \(a\) or in state \(b\) and the formula \(\square(P[\alpha] \geq 0.5)\) is true in iLTL.

## Publications

- YoungMin Kwon and Gul A. Agha. Verifying the evolution of probability distributions governed by a DTMC. IEEE Trans. Software Eng, 37(1):126–141, 2011.
- YoungMin Kwon and Gul A. Agha. iLTLChecker: A probabilistic model checker for multiple DTMCs. In QEST, 245–246. IEEE Computer Society, 2005.
- YoungMin Kwon and Gul Agha. Linear inequality LTL (iLTL): A model checker for discrete time Markov chains. In ICFEM, volume 3308 of Lecture Notes in Computer Science, 194–208. Springer, 2004.

## Downloads

- Version 1.0: Sources

## License

The iLTL Checker is open source software and is available under a BSD style license. See the preamble in the source files for details. Copyright (c) 2011 Open Systems Lab. All rights reserved.

## History

YoungMin Kwon designed and implemented the iLTL Checker between 2004 and 2005.