TY - JOUR

T1 - Verifying the evolution of probability distributions governed by a DTMC

AU - Kwon, Youngmin

AU - Agha, Gul

N1 - Funding Information:
The authors thank Eunhee Kim and Kent Cheung for their helpful comments. The authors also thank the anonymous referees for numerous comments that have helped improve the exposition of this paper. This research has been supported in part by CNS 05-09321 and by the US Office of Naval Research under US Department of Defense MURI award N0014-020100715.

PY - 2011

Y1 - 2011

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

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

KW - Discrete Time Markov Chain

KW - Probabilistic model checking

KW - linear temporal logic

KW - pharmacokinetics

UR - http://www.scopus.com/inward/record.url?scp=79551538969&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79551538969&partnerID=8YFLogxK

U2 - 10.1109/TSE.2010.80

DO - 10.1109/TSE.2010.80

M3 - Article

AN - SCOPUS:79551538969

VL - 37

SP - 126

EP - 141

JO - IEEE Transactions on Software Engineering

JF - IEEE Transactions on Software Engineering

SN - 0098-5589

IS - 1

M1 - 5557891

ER -