Name
Abstract | ||
|---|---|---|
The quantitative analysis of a randomized system, modeled by a Markov decision process, against an LTL formula can be performed by a combination of graph algorithms, automata-theoretic concepts and numerical methods to compute maximal or minimal reachability probabilities. In this paper, we present various reduction techniques that serve to improve the performance of the quantitative analysis, and report on their implementation on the top of the probabilistic model checker LiQuor. Although our techniques are purely heuristic and cannot improve the worst-case time complexity of standard algorithms for the quantitative analysis, a series of examples illustrates that the proposed methods can yield a major speed-up. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1109/QEST.2008.45 | St. Malo |
Keywords | Field | DocType |
selection process,model checking markov decision,diverse community,accepted paper,reduction techniques,great variety,wide range,titanium,algorithm design and analysis,model checking,automata theory,reactive power,markov decision processes,markov processes,numerical methods,computational complexity,linear program,probability,quantitative analysis,computational modeling,formal verification,numerical method,probabilistic model,system modeling,markov decision process,time complexity,context modeling,probabilistic logic | Discrete mathematics,Heuristic,Markov process,Model checking,Computer science,Markov decision process,Theoretical computer science,Reachability,Probabilistic logic,Time complexity,Computational complexity theory | Conference |
ISBN | Citations | PageRank |
978-0-7695-3360-5 | 21 | 0.88 |
References | Authors | |
21 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Frank Ciesinski | 1 | 299 | 14.52 |
| Christel Baier | 2 | 3053 | 185.85 |
| Marcus Gröβer | 3 | 21 | 0.88 |
| Joachim Klein | 4 | 91 | 5.77 |