Abstract
The bottleneck in the quantitative analysis of Markov chains and Markov decision processes against specifications given in LTL or as some form of nondeterministic Büchi automata is the inclusion of a determinisation step of the automaton under consideration. In this paper, we show that full determinisation can be avoided: subset and breakpoint constructions suffice. We have implemented our approach - both explicit and symbolic versions - in a prototype tool. Our experiments show that our prototype can compete with mature tools like PRISM.
Original language | English |
---|---|
Title of host publication | 26th International Conference on Concurrency Theory, CONCUR 2015 |
Editors | Luca Aceto, David de Frutos Escrig |
Place of Publication | Dagstuhl |
Publisher | Dagstuhl |
Pages | 354-367 |
Number of pages | 14 |
ISBN (Electronic) | 9783939897910 |
DOIs | |
Publication status | Published - 2015 |
Externally published | Yes |
Event | 26th International Conference on Concurrency Theory, CONCUR 2015 - Madrid, Spain Duration: 1 Sep 2015 → 4 Sep 2015 Conference number: 26 |
Publication series
Name | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Publisher | Dagstuhl |
Volume | 42 |
ISSN (Print) | 1868-8969 |
Conference
Conference | 26th International Conference on Concurrency Theory, CONCUR 2015 |
---|---|
Abbreviated title | CONCUR |
Country/Territory | Spain |
City | Madrid |
Period | 1/09/15 → 4/09/15 |
Keywords
- Determinisation
- Markov decision processes
- Model checking
- PLTL