Sciweavers

Share
CONCUR
2001
Springer

Symbolic Computation of Maximal Probabilistic Reachability

9 years 11 months ago
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....
Marta Z. Kwiatkowska, Gethin Norman, Jeremy Sprost
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where CONCUR
Authors Marta Z. Kwiatkowska, Gethin Norman, Jeremy Sproston
Comments (0)
books