Paper Info
Title
Stochastic Games for Verification of Probabilistic Timed Automata
Abstract
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 using abstraction 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 also present 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 verifying PTAs, such as backwards reachability and digital clocks, our techniques exhibit superior performance and scalability.
Year
DOI
Venue
2009
10.1007/978-3-642-04368-0_17
FORMATS
Keywords
Field
DocType
upper bound,real time
Discrete mathematics,Nondeterministic algorithm,Computer science,Automaton,Algorithm,Markov decision process,Theoretical computer science,Reachability,Timed automaton,Probabilistic logic,Stochastic game,Scalability
Conference
Volume
ISSN
Citations 
5813
0302-9743
34
PageRank 
References 
Authors
2.83
24
3
Name
Order
Citations
PageRank
Marta Z. Kwiatkowska16118322.21
Gethin Norman24163193.68
David Parker34018184.00