Name
Abstract | ||
|---|---|---|
This paper investigates relative precision and optimality of analyses for concurrent probabilistic systems. Aiming at the problem at the heart of probabilistic model checking – computing the probability of reaching a particular set of states – we leverage the theory of abstract interpretation. With a focus on predicate abstraction, we develop the first abstract-interpretation framework for Markov decision processes which admits to compute both lower and upper bounds on reachability probabilities. Further, we describe how to compute and approximate such abstractions using abstraction refinement and give experimental results. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-11319-2_26 | VMCAI |
Keywords | Field | DocType |
markov decision process | Abstraction model checking,Predicate abstraction,Abstract interpretation,Computer science,Markov decision process,Probabilistic CTL,Theoretical computer science,Probabilistic logic,Probabilistic argumentation,Probabilistic relevance model | Conference |
Volume | ISSN | ISBN |
5944 | 0302-9743 | 3-642-11318-4 |
Citations | PageRank | References |
14 | 0.63 | 21 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Björn Wachter | 1 | 326 | 20.09 |
| Lijun Zhang | 2 | 451 | 24.40 |