Three-valued abstraction for probabilistic systems

Abstract

This paper proposes a novel abstraction technique for fully probabilistic systems. The models of our study are classical discrete-time and continuous-time Markov chains (DTMCs and CTMCs, for short). A DTMC is a Kripke structure in which each transition is equipped with a discrete probability; in a CTMC, in addition, state residence times are governed by negative exponential distributions. Our abstraction technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key ingredients of our technique are a partitioning of the state space combined with an abstraction of transition probabilities by intervals. It is shown that this provides a conservative abstraction for both negative and affirmative verification results for a three-valued semantics of PCTL (Probabilistic Computation Tree Logic). In the continuous-time setting, the key idea is to apply abstraction on uniform CTMCs which are readily obtained from general CTMCs. In a similar way as for the discrete case, this is shown to yield a conservative abstraction for a three-valued semantics of CSL (Continuous Stochastic Logic). Abstract CTMCs can be verified by computing time-bounded reachability probabilities in continuous-time MDPs.

@article{katoenThreeValuedAbstractionForProbabilistic2012,
 author = {Joost-Pieter Katoen and Daniel Klink and Martin Leucker and Verena Wolf},
 doi = {10.1016/j.jlap.2012.03.007},
 journal = {The Journal of Logic and Algebraic Programming (JLAP)},
 month = {5},
 number = {4},
 pages = {356-389},
 publisher = {Elsevier, Amsterdam},
 title = {Three-valued abstraction for probabilistic systems},
 volume = {81},
 year = {2012}
}