Abstract

The generic representatives (or counter abstraction) approach has been shown to be an effective symmetry reduction method for model checking. This method was extended to a probabilistic setting via a specialised language, Symmetric Probabilistic Specification Language (SPSL) and an associated tool, GRIP, for use with the PRISM model checker. However, SPSL does not support synchronisation-based communication, making this method inapplicable to systems that require synchronisation. We show how synchronisation can be added to SPSL, and develop new counter abstraction translation rules for synchronous statements. We extend GRIP accordingly and demonstrate the feasibility and effectiveness of the new abstraction rules via a range of examples. This extends the applicability of the generic representatives technique to the wide class of probabilistic systems that rely on synchronisation. Experimental results show that our approach works well for systems that are composed of a large number of simple symmetric modules that feature a small amount of synchronisation-based communication.