swMATH ID: 13369
Software Authors: Patel, Reema; Patel, Kevin; Patel, Dhiren
Description: ExplicitPRISMSymm: symmetry reduction technique for explicit models in PRISM. Probabilistic model checking of concurrent system involves exhaustive search of the reachable state space associated with the system model. Symmetry reduction is a commonly employed technique that enables model checking of exponentially large models. Most work on symmetry reduction focuses on symbolically represented probabilistic models, which are easy to build and perform reasonably well at property checking. In this work, we rather focus on explicitly represented probabilistic models. We report that explicitly represented models perform well at property checking, but face hurdles in model construction. We present an on-the-fly symmetry reduction technique for explicitly represented models. It significantly reduces build time and thus explicit model representation as an efficient alternative to symbolic model representation.
Homepage: http://link.springer.com/chapter/10.1007%2F978-3-319-17142-5_34
Dependencies: PRISM
Keywords: on-the-fly symmetry reduction; probabilistic model checking; explicit state representation
Related Software: PRISM
Cited in: 2 Documents

Citations by Year