On the Representation of Probabilities over Structured Domains

. In this paper we extend one of the main tools used in verification of discrete systems, namely Binary Decision Diagrams (BDD), to treat probabilistic transition systems. We show how probabilistic vectors and matrices can be represented canonically and succinctly using probabilistic trees and graphs, and how simulation of large-scale probabilistic systems can be performed. We consider this work as an important contribution of the verification community to numerous domains which need to manipulate very large matrices. 1 Introduction Many problems in discrete verification can be reduced to the the following one: given a non-deterministic finite-state automaton A = (Q; ffi) and a set P ` Q of states, find the set P of all the states reachable from P . One common way to do this calculation is to let P 0 = P and P i+1 = ffi(P i ) until P i is included in the union P 0 [ : : : [ P i\Gamma1 . Here P i is the set of states reachable from P after exactly i steps. This method..