GRIP: Generic Representatives in PRISM

We give an overview of GRIP, a symmetry reduction tool for the probabilistic model checker PRISM, together with experimental results for a selection of example specifications. 1 An Overview of GRIP GRIP (generic representatives in PRISM), introduced in [1], is a symmetry reduction tool for the PRISM model checker [6]. GRIP is based on the generic representatives approach of [2], which aims to overcome the inherent problem of combining symmetry reduction with symbolic state-space representation. We present an overview of GRIP version 2.0 (referred to henceforth as GRIP), an improved version of the original tool, and compare GRIP to PRISM-symm, an alternative symmetry reduction tool for PRISM [5]. GRIP, together with the PRISM examples used for experiments in Section 3 can be downloaded from our website [4]. The top panel of Figure 1 shows a simple leader election protocol in PRISM, adapted from [1]. The underlying model here is a Markov decision process (MDP). GRIP works by translatin...

• Type: Conference
• Year: 2007
• Where: QEST
• Authors: Alastair F. Donaldson, Alice Miller, David Parker
• Keywords: Generic Representatives, Generic Representatives Approach, QEST 2007, Quantitative Evaluation Of Systems, Symmetry Reduction Tool