Issue No. 01 - January/February (2011 vol. 37)

ISSN: 0098-5589

pp: 126-141

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2010.80

Gul Agha , University of Illinois at Urbana-Champaign, Urbana

YoungMin Kwon , Microsoft Corporation, Redmond

ABSTRACT

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.

INDEX TERMS

Probabilistic model checking, linear temporal logic, Discrete Time Markov Chain, pharmacokinetics.

CITATION

Gul Agha, YoungMin Kwon, "Verifying the Evolution of Probability Distributions Governed by a DTMC",

*IEEE Transactions on Software Engineering*, vol. 37, no. , pp. 126-141, January/February 2011, doi:10.1109/TSE.2010.80