iLTLChecker: A Probabilistic Model Checker for Multiple DTMCs

12 years 11 months ago
iLTLChecker: A Probabilistic Model Checker for Multiple DTMCs
iLTL is a probabilistic temporal logic that can specify properties of multiple discrete time Markov chains (DTMCs). In this paper, we describe two related tools: MarkovEstimator a tool to estimate a Markov transition matrix, and iLTLChecker, a tool to model check iLTL properties of DTMCs. These tools work together to verify iLTL properties of DTMCs. 1 iLTLChecker iLTL [6] is a Linear Temporal Logic (LTL) [5] that can specify temporal changes of expected rewards of a Markov process. Unlike existing probabilistic temporal logics such as Probabilistic Computation Tree Logic (PCTL) [3] and Continuous Stochastic Logic (CSL) [1] which build a probability space on the paths of computation and reason about the probability space, iLTL specifies directly on the transitions of Probability Mass Function (pmf). 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 st...
YoungMin Kwon, Gul A. Agha
Added 25 Jun 2010
Updated 25 Jun 2010
Type Conference
Year 2005
Where QEST
Authors YoungMin Kwon, Gul A. Agha
Comments (0)