Symbolic Model Checking of Concurrent Probabilistic Processes Using MTBDDs and the Kronecker Representation

Appears: Proceedings of TACAS 2000, Berlin, LNCS 1785, April 2000.

Abstract: This paper reports on experimental results with symbolic model checking of probabilistic processes based on Multi-Terminal Binary Decision Diagrams (MTBDDs). We consider concurrent probabilistic systems as models; these allow nondeterministic choice between probability distributions and are particularly well suited to modelling distributed systems with probabilistic behaviour, e.g. randomized consensus algorithms and probabilistic failures. As a specification formalism we use the probabilistic branching-time temporal logic PBTL which allows one to express properties such as ``under any scheduling of nondeterministic choices, the probability of \phi holding until \psi is true is at least 0.78/at most 0.04''. We adapt the Kronecker representation of (Plateau 1985), which yields a very compact MTBDD encoding of the system. We implement an experimental model checker using the CUDD package and demonstrate that model construction and reachability-based model checking is possible in a matter of seconds for certain classes of systems consisting of up to 10^{30} states.

Download:
Download the paper from the publisher.

Download an author-created copy of the paper (© Springer-Verlag).