×

ExplicitPRISMSymm: symmetry reduction technique for explicit models in PRISM. (English) Zbl 1459.68122

Jain, Rahul (ed.) et al., Theory and applications of models of computation. 12th annual conference, TAMC 2015, Singapore, May 18–20, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9076, 400-412 (2015).
Summary: 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.
For the entire collection see [Zbl 1320.68020].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barner, S.; Grumberg, O.; Brinksma, E.; Larsen, KG, Combining symmetry reduction and under-approximation for symbolic model checking, Computer Aided Verification, 93-106 (2002), Heidelberg: Springer, Heidelberg · Zbl 1010.68510
[2] Kwiatkowska, M.; Norman, G.; Parker, D.; Field, T.; Harrison, PG; Bradley, J.; Harder, U., PRISM: probabilistic symbolic model checker, Computer Performance Evaluation, 200-204 (2002), Heidelberg: Springer, Heidelberg · Zbl 1047.68533
[3] Donaldson, A., Miller, A., Parker, D.: GRIP: generic representatives in PRISM. In: Proceeding of the Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), pp. 115-116, September 2007
[4] Donaldson, A., Miller, A., Parker, D.: Language-level symmetry reduction for probabilistic model checking. In: Proceeding of the Sixth International Conference on the Quantitative Evaluation of Systems (QEST 2009), pp. 289-298, September 2009
[5] Donaldson, AF; Miller, A.; Graf, S.; Zhang, W., Symmetry reduction for probabilistic model checking using generic representatives, Automated Technology for Verification and Analysis, 9-23 (2006), Heidelberg: Springer, Heidelberg · Zbl 1161.68564
[6] Emerson, EA; Wahl, T.; Halbwachs, N.; Zuck, LD, Dynamic symmetry reduction, Tools and Algorithms for the Construction and Analysis of Systems, 382-396 (2005), Heidelberg: Springer, Heidelberg
[7] Fujita, M.; McGeer, PC; Yang, JCY, Multi-terminal binary decision diagrams: an efficient datastructure for matrix representation, Formal Methods Syst. Des., 10, 2-3, 149-169 (1997)
[8] Gyuris, V.; Prasad Sistla, A.; Grumberg, O., On-the-fly model checking under fairness that exploits symmetry, Computer Aided Verification, 232-243 (1997), Heidelberg: Springer, Heidelberg
[9] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal Aspects Comput., 6, 5, 512-535 (1994) · Zbl 0820.68113
[10] Hinton, A.; Kwiatkowska, M.; Norman, G.; Parker, D.; Hermanns, H.; Palsberg, J., PRISM: a tool for automatic verification of probabilistic systems, Tools and Algorithms for the Construction and Analysis of Systems, 441-444 (2006), Heidelberg: Springer, Heidelberg
[11] Kwiatkowska, M.; Norman, G.; Segala, R.; Berry, G.; Comon, H.; Finkel, A., Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM, Computer Aided Verification, 194-206 (2001), Heidelberg: Springer, Heidelberg · Zbl 0991.68503
[12] Kwiatkowska, M.; Norman, G.; Sproston, J.; Wang, F., Symbolic model checking for probabilistic timed automata, Inf. Comput., 205, 7, 1027-1077 (2007) · Zbl 1122.68075
[13] Kwiatkowska, M.; Norman, G.; Parker, D.; Ball, T.; Jones, RB, Symmetry reduction for probabilistic model checking, Computer Aided Verification, 234-248 (2006), Heidelberg: Springer, Heidelberg · Zbl 1188.68194
[14] Miller, A.; Donaldson, A.; Calder, M., Symmetry in temporal logic model checking, ACM Comput. Surv., 38, 3, 8 (2006)
[15] Parker, D.: Implementation of symbolic model checking for probabilistic systems. Ph.d. thesis, University of Birmingham (2002)
[16] Power, C.: Probabilistic symmetry reduction. Ph.d. thesis, University of Glasgow (2012). http://theses.gla.ac.uk/3493/
[17] Sistla, A., Employing symmetry reductions in model checking, Comput. Lang. Syst. & Struct., 30, 3-4, 99-137 (2004) · Zbl 1072.68068
[18] Wahl, T.; Donaldson, A., Replication and abstraction: symmetry in automated formal verification, Symmetry, 2, 2, 799-847 (2010)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.