Verifying Randomized Distributed Algorithms with PRISM
Marta Kwiatkowska, Gethin Norman, David A. Parker · 2000
. 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 the probabilistic temporal logic PCTL (also under fairness constraints). Our experiments indicate that using MTBDD variable ordering induced from the structure of the high-level description of the model yields very ecient MTBDD representations of randomized distributed algorithms. 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 eciency of numerical computation with MTBDDs, however, and hence also model checking of quantitative probabilistic temp...