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

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 holding until 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 ...

• Type: Conference
• Year: 2000
• Where: TACAS
• Authors: Luca de Alfaro, Marta Z. Kwiatkowska, Gethin Norman, David Parker, Roberto Segala
• Keywords: Algorithms, Model Checking, Nondeterministic Choices, Probabilistic, TACAS 2000