Sciweavers

Share
FORMATS
2009
Springer

Stochastic Games for Verification of Probabilistic Timed Automata

8 years 10 months ago
Stochastic Games for Verification of Probabilistic Timed Automata
Probabilistic timed automata (PTAs) are used for formal modelling and verification of systems with probabilistic, nondeterministic and real-time behaviour. For non-probabilistic timed automata, forwards reachability is the analysis method of choice, since it can be implemented extremely efficiently. However, for PTAs, such techniques are only able to compute upper bounds on maximum reachability probabilities. In this paper, we propose a new approach to the analysis of PTAs straction and stochastic games. We show how efficient forwards reachability techniques can be extended to yield both lower and upper bounds on maximum (and minimum) reachability probabilities. We sent abstraction-refinement techniques that are guaranteed to improve the precision of these probability bounds, providing a fully automatic method for computing the exact values. We have implemented these techniques and applied them to a set of large case studies. We show that, in comparison to alternative approaches to ver...
Marta Z. Kwiatkowska, Gethin Norman, David Parker
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2009
Where FORMATS
Authors Marta Z. Kwiatkowska, Gethin Norman, David Parker
Comments (0)
books