Name
Abstract | ||
|---|---|---|
Modelling and verification of systems such as communication, network and security protocols, which exhibit both probabilistic and non-deterministic behaviour, typically use Markov Decision Processes (MDPs). For large, complex systems, abstraction techniques are essential. This paper builds on a promising approach for abstraction of MDPs based on stochastic two-player games which provides distinct lower and upper bounds for minimum and maximum probabilistic reachability properties. Existing implementations work at the model level, limiting their scalability. In this paper, we develop language-level abstraction techniques that build game-based abstractions of MDPs directly from high-level descriptions in the PRISM modelling language, using predicate abstraction and SMT solvers. For efficiency, we develop a compositional framework for abstraction. We have applied our techniques to a range of case studies, successfully verifying models larger than was possible with existing implementations. We are also able to demonstrate the benefits of adopting a compositional approach. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1016/j.entcs.2008.11.016 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
probabilistic model checking,game-based probabilistic predicate abstraction,implementations work,markov models,game-based abstraction,compositional approach,language-level abstraction technique,maximum probabilistic reachability property,compositional framework,automatic verification,promising approach,prism modelling language,predicate abstraction,abstraction technique,complex system,security protocol,markov model,markov decision process | Abstraction model checking,Programming language,Abstraction,Predicate abstraction,Computer science,Markov model,Markov decision process,Theoretical computer science,Reachability,Probabilistic logic,Scalability | Journal |
Volume | Issue | ISSN |
220 | 3 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
17 | 0.76 | 19 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mark Kattenbelt | 1 | 70 | 4.48 |
| Marta Z. Kwiatkowska | 2 | 6118 | 322.21 |
| Gethin Norman | 3 | 4163 | 193.68 |
| David Parker | 4 | 4018 | 184.00 |