Game-Based Probabilistic Predicate Abstraction in PRISM

ion in PRISM1 Mark Kattenbelt Marta Kwiatkowska Gethin Norman David Parker Oxford University Computing Laboratory, Oxford, UK 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 omplex systems, abstraction techniques are essential. This paper builds on a promising approach raction 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 odel level, limiting their scalability. In this paper, we develop language-level abstraction techniques ld game-based abstractions of MDPs directly from high-level descriptions in the PRISM modelling , using predicate abstraction and SMT solvers. For efficiency, we develop a compositional framework raction. We have applied our techniques to a range of case studies, succe...

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, David Parker
• Keywords: Abstraction Techniques, ENTCS 2008, Marta Kwiatkowska Gethin, Oxford University Computing Laboratory