Open Systems Laboratory at Illinois

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.




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.


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