Name
Abstract | ||
|---|---|---|
The limiting factor for quantitative analysis of Markov decision processes (MDP) against specifications given in linear temporal logic (LTL) is the size of the generated product. As recently shown, a special subclass of limit-deterministic Buchi automata (LDBA) can replace deterministic Rabin automata in quantitative probabilistic model checking algorithms. We present an extension of PRISM for LTL model checking of MDP using LDBA. While existing algorithms can be used only with minimal changes, the new approach takes advantage of the special structure and the smaller size of the obtained LDBA to speed up the model checking. We demonstrate the speed up experimentally by a comparison with other approaches. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-46520-3_9 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Abstraction model checking,Discrete mathematics,Model checking,Computer science,Automaton,Markov decision process,Algorithm,Theoretical computer science,Linear temporal logic,Probabilistic logic,Temporal logic,Büchi automaton | Conference | 9938 |
ISSN | Citations | PageRank |
0302-9743 | 4 | 0.39 |
References | Authors | |
25 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Salomon Sickert | 1 | 34 | 8.01 |
| Jan Kretínský | 2 | 159 | 16.02 |