Sciweavers

Share
TACAS
2000
Springer

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

8 years 9 months ago
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 ...
Luca de Alfaro, Marta Z. Kwiatkowska, Gethin Norma
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where TACAS
Authors Luca de Alfaro, Marta Z. Kwiatkowska, Gethin Norman, David Parker, Roberto Segala
Comments (0)
books