Verifying the Evolution of Probability Distributions Governed by a DTMC

YoungMin Kwon, Gul Agha

IEEE Transactions on Software Engineering 37(1), pages 126-141
January 2011

We propose a new probabilistic temporal logic, iLTL, which captures properties of systems whose state can be represented by probability mass functions (pmfs). Using iLTL, we can specify reachability to a state (i.e., a pmf), as well as properties representing the aggregate (expected) behavior of a system. We then consider a class of systems whose transitions are governed by a Markov Chain-in this case, the set of states a system may be in is specified by the transitions of pmfs from all potential initial states to the final state. We then provide a model checking algorithm to check iLTL properties of such systems. Unlike existing model checking techniques, which either compute the portions of the computational paths that satisfy a specification or evaluate properties along a single path of pmf transitions, our model checking technique enables us to do a complete analysis on the expected behaviors of large-scale systems. Desirable system parameters may also be found as a counterexample of a negated goal. Finally, we illustrate the usefulness of iLTL model checking by means of two examples: assessing software reliability and ensuring the results of administering a drug.

(keywords) Probabilistic model checking, linear temporal logic, Discrete Time Markov Chain, pharmacokinetics



— authors

YoungMin Kwon, Gul Agha

— status


— sort

article in journal

— publication date

January 2011

— journal

IEEE Transactions on Software Engineering

— volume


— issue


— pages


— address

Piscataway, NJ, USA


original page




— print ISSN


Partita IVA: 01131710376 — Copyright © 2008–2023 APICe@DISI – PRIVACY