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...

• Type: Conference
• Year: 2005
• Where: QEST
• Authors: YoungMin Kwon, Gul A. Agha
• Keywords: Discrete Time Markov, Probabilistic Temporal Logics, QEST 2005, Quantitative Evaluation Of Systems, Time Markov Chain