o
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
supports model checking of the probabilistic temporal logic PCTL (also
under fairness constraints) and has a system description language similar
to Reactive Modules, based on modular composition. Our experiments
indicate that through a direct translation from this language into MTBDDs,
an efficient symbolic encoding is obtained, exploiting structure in the
system
being modelled. In particular, we are able to construct models of up to
10^30
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 for example sparse matrices.
Descriptions and statistics obtained for several case studies can be found
at