Abstract.
In this paper we describe our experience with model checking
randomized distributed algorithms using PRISM,
a symbolic model checker for concurrent probabilistic
systems currently being developed.
PRISM uses Multi-Terminal Binary Decision Diagrams (MTBDDs) as
supplied by the CUDD package of Fabio Somenzi.
Implemented in Java, PRISM has a system description language similar
to Reactive Modules and supports model checking of probabilistic temporal logic PCTL
(also under fairness constraints).
Our experiments indicate that using
the BDD variable ordering induced from the Kronecker representation
yields very efficient MTBDD representations of randomized distributed
algorithms. In particular, we are able to construct models of up to
1030 states in
seconds. Model checking of "with probability 1" PCTL
properties is also fast. The efficiency of numerical computation with MTBDDs, however,
and hence also model checking of quantitative probabilistic temporal
logic properties, is still
considerably poorer than e.g. for sparse matrices.
Descriptions and statistics obtained for several case studies can be
found at the PRISM web page.
|