Game-Based Probabilistic Predicate Abstraction in PRISM

Citations of this article
Mendeley users who have this article in their library.


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. © 2008 Elsevier B.V. All rights reserved.




Kattenbelt, M., Kwiatkowska, M., Norman, G., & Parker, D. (2008). Game-Based Probabilistic Predicate Abstraction in PRISM. Electronic Notes in Theoretical Computer Science, 220(3), 5–21.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free