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

Patel, Reema; Patel, Kevin; Patel, Dhiren

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.)

Keywords:

on-the-fly symmetry reduction; probabilistic model checking; explicit state representation

Software:

PRISM; ExplicitPRISMSymm

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 · doi:10.1007/3-540-45657-0_8
[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 · doi:10.1007/11901914_4
[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 · Zbl 1087.68587 · doi:10.1007/978-3-540-31980-1_25
[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) · doi:10.1023/A:1008647823331
[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 · doi:10.1007/3-540-63166-6_24
[9]	Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal Aspects Comput., 6, 5, 512-535 (1994) · Zbl 0820.68113 · doi:10.1007/BF01211866
[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 · doi:10.1007/11691372_29
[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 · doi:10.1007/3-540-44585-4_17
[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 · doi:10.1016/j.ic.2007.01.004
[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 · doi:10.1007/11817963_23
[14]	Miller, A.; Donaldson, A.; Calder, M., Symmetry in temporal logic model checking, ACM Comput. Surv., 38, 3, 8 (2006) · doi:10.1145/1132960.1132962
[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) · doi:10.3390/sym2020799