Symbolic Computation of Maximal Probabilistic Reachability

We study the maximal reachability probability problem for infinite-state systems featuring both nondeterministic and probabilistic choice. The problem involves the computation of the maximal probability of reaching a given set of states, and underlies decision procedures for the automatic verification of probabilistic systems. We extend the framework of symbolic transition systems, which equips an infinite-state system with an algebra of symbolic operators on its state space, with a symbolic encoding of probabilistic transitions to obtain a model for an infinite-state probabilistic system called a symbolic probabilistic system. An exact answer to the maximal reachability probability problem for symbolic probabilistic systems is obtained algorithmically via iteration of a refined version of the classical predecessor operation, combined with intersection operations. As in the non-probabilistic case, our state space exploration algorithm is semi-decidable for infinite-state systems....

• Type: Conference
• Year: 2001
• Where: CONCUR
• Authors: Marta Z. Kwiatkowska, Gethin Norman, Jeremy Sproston
• Keywords: CONCUR 2001, Distributed And Parallel Computing, Maximal Reachability Probability, Probabilistic, Reachability Probability