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 Multi-Terminal Binary Decision Diagrams (MTBDDs). We consider concurrent systems as models; these allow nondeterministic choice between probability distributions and are particularly well suited to modelling distributed behaviour, e.g. randomized consensus algorithms failures. As a specification formalism we use the branching-time temporal logic PBTL which allows one express properties such "under any scheduling choices, Φ holding until ψ is true at least 0.78/at most 0.04". adapt Kronecker representation (Plateau 1985), yields very compact MTBDD encoding system. implement an checker using CUDD package demonstrate that construction reachability-based possible in matter seconds for certain classes consisting up 1030 states.