# 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

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.