AIB 2007-20: Three-Valued Abstraction for Probabilistic Systems

The following technical report is available from
http://aib.informatik.rwth-aachen.de:

Three-Valued Abstraction for Probabilistic Systems
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, and Verena Wolf
AIB 2007-20

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. The uncertainty of
intervals is resolved by history-dependent schedulers that may choose
extreme values only. 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). The verification of abstract DTMCs is inspired by the standard
MDP (Markov Decision Process) model-checking problem. Abstract CTMCs
can be verified by computing time-bounded reachability probabilities in
continuous-time MDPs. Some experiments on an infinite-state stochastic
Petri net indicate the feasibility of our abstraction technique.

.