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.
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Jain, Rahul (ed.); Jain, Sanjay (ed.); Stephan, Frank (ed.): Theory and applications of models of computation. 12th annual conference, TAMC 2015, Singapore, May 18--20, 2015. Proceedings (2015)
- Patel, Reema; Patel, Kevin; Patel, Dhiren: ExplicitPRISMSymm: symmetry reduction technique for explicit models in PRISM (2015)