Sciweavers

QEST
2007
IEEE

GRIP: Generic Representatives in PRISM

13 years 10 months ago
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...
Alastair F. Donaldson, Alice Miller, David Parker
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where QEST
Authors Alastair F. Donaldson, Alice Miller, David Parker
Comments (0)