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
IEEE Press, Piscataway, NJ, USA

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
 @article{KwonTSE2011,
author = {Kwon, YoungMin and Agha, Gul},
title = {Verifying the Evolution of Probability Distributions Governed by a DTMC},
journal = {IEEE Transactions on Software Engineering},
volume = 37,
number = 1,
month = jan,
year = 2011,
issn = {0098-5589},
pages = {126--141},
doi = {10.1109/TSE.2010.80},
url = {http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=5557891},
acmid = {1936543},
publisher = {IEEE Press},
address = {Piscataway, NJ, USA},
keywords = {Probabilistic model checking, linear temporal logic, Discrete Time Markov Chain, pharmacokinetics}}
 

Tags:

Publication

— authors

YoungMin Kwon, Gul Agha

— status

published

— sort

article in journal

Venue

— journal

IEEE Transactions on Software Engineering

— volume

37

— issue

1

— pages

126-141

— publication date

January 2011

URLs

original page

Identifiers

— DOI

10.1109/TSE.2010.80

— print ISSN

0098-5589

BibTeX

— BibTeX ID
KwonTSE2011
— BibTeX category
article

Partita IVA: 01131710376 - Copyright © 2008-2022 APICe@DISI Research Group - PRIVACY