Abstract
The verification of probabilistic timed automata involves finding schedulers that optimise their nondeterministic choices with respect to the probability of a property. In practice, approaches based on model checking fail due to state-space explosion, while simulation-based techniques like statistical model checking are not applicable due to the nondeterminism. We present a new lightweight on-the-fly algorithm to find near-optimal schedulers for probabilistic timed automata. We make use of the classical region and zone abstractions from timed automata model checking, coupled with a recently developed smart sampling technique for statistical verification of Markov decision processes. Our algorithm provides estimates for both maximum and minimum probabilities. We compare our new approach with alternative techniques, first using tractable examples from the literature, then motivate its scalability using case studies that are intractable to numerical model checking and challenging for existing statistical techniques.
Original language | English |
---|---|
Title of host publication | Proceedings of the 12th International Conference on Integrated Formal Methods (IFM 2016) |
Place of Publication | Cham |
Publisher | Springer |
Pages | 99-114 |
Number of pages | 16 |
ISBN (Print) | 978-3-319-33692-3 |
DOIs | |
Publication status | Published - Jun 2016 |
Event | 12th International Conference on integrated Formal Methods 2016 - Reykjavik Iceland, Reykjavik, Iceland Duration: 1 Jun 2016 → 5 Jun 2016 Conference number: 12 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Verlag |
Volume | 9681 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 12th International Conference on integrated Formal Methods 2016 |
---|---|
Abbreviated title | iFM 2016 |
Country/Territory | Iceland |
City | Reykjavik |
Period | 1/06/16 → 5/06/16 |
Keywords
- METIS-317210
- EWI-27044
- IR-100708