{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T13:58:01Z","timestamp":1773323881842,"version":"3.50.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319171418","type":"print"},{"value":"9783319171425","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17142-5_34","type":"book-chapter","created":{"date-parts":[[2015,4,15]],"date-time":"2015-04-15T11:19:29Z","timestamp":1429096769000},"page":"400-412","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["ExplicitPRISMSymm: Symmetry Reduction Technique for Explicit Models in PRISM"],"prefix":"10.1007","author":[{"given":"Reema","family":"Patel","sequence":"first","affiliation":[]},{"given":"Kevin","family":"Patel","sequence":"additional","affiliation":[]},{"given":"Dhiren","family":"Patel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,16]]},"reference":[{"key":"34_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-45657-0_8","volume-title":"Computer Aided Verification","author":"S Barner","year":"2002","unstructured":"Barner, S., Grumberg, O.: Combining symmetry reduction and under-approximation for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 93\u2013106. Springer, Heidelberg (2002)"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200\u2013204. Springer, Heidelberg (2002). http:\/\/www.prismmodelchecker.org\/casestudies\/index.php"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013116, September 2007","DOI":"10.1109\/QEST.2007.30"},{"key":"34_CR4","doi-asserted-by":"crossref","unstructured":"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\u2013298, September 2009","DOI":"10.1109\/QEST.2009.21"},{"key":"34_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/11901914_4","volume-title":"Automated Technology for Verification and Analysis","author":"AF Donaldson","year":"2006","unstructured":"Donaldson, A.F., Miller, A.: Symmetry reduction for probabilistic model checking using generic representatives. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 9\u201323. Springer, Heidelberg (2006)"},{"key":"34_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-31980-1_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EA Emerson","year":"2005","unstructured":"Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 382\u2013396. Springer, Heidelberg (2005)"},{"issue":"2\u20133","key":"34_CR7","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M Fujita","year":"1997","unstructured":"Fujita, M., McGeer, P.C., Yang, J.C.Y.: Multi-terminal binary decision diagrams: an efficient datastructure for matrix representation. Formal Methods Syst. Des. 10(2\u20133), 149\u2013169 (1997)","journal-title":"Formal Methods Syst. Des."},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-63166-6_24","volume-title":"Computer Aided Verification","author":"V Gyuris","year":"1997","unstructured":"Gyuris, V., Prasad Sistla, A.: On-the-fly model checking under fairness that exploits symmetry. In: Grumberg, O. (ed.) Computer Aided Verification. LNCS, vol. 1254, pp. 232\u2013243. Springer, Heidelberg (1997)"},{"issue":"5","key":"34_CR9","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"key":"34_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"34_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-44585-4_17","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2001","unstructured":"Kwiatkowska, M., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 194\u2013206. Springer, Heidelberg (2001)"},{"issue":"7","key":"34_CR12","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027\u20131077 (2007)","journal-title":"Inf. Comput."},{"key":"34_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/11817963_23","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 234\u2013248. Springer, Heidelberg (2006)"},{"issue":"3","key":"34_CR14","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/1132960.1132962","volume":"38","author":"A Miller","year":"2006","unstructured":"Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3), 8 (2006)","journal-title":"ACM Comput. Surv."},{"key":"34_CR15","unstructured":"Parker, D.: Implementation of symbolic model checking for probabilistic systems. Ph.d. thesis, University of Birmingham (2002)"},{"key":"34_CR16","unstructured":"Power, C.: Probabilistic symmetry reduction. Ph.d. thesis, University of Glasgow (2012). http:\/\/theses.gla.ac.uk\/3493\/"},{"issue":"3\u20134","key":"34_CR17","first-page":"99","volume":"30","author":"A Sistla","year":"2004","unstructured":"Sistla, A.: Employing symmetry reductions in model checking. Comput. Lang. Syst. & Struct. 30(3\u20134), 99\u2013137 (2004)","journal-title":"Comput. Lang. Syst. & Struct."},{"issue":"2","key":"34_CR18","doi-asserted-by":"publisher","first-page":"799","DOI":"10.3390\/sym2020799","volume":"2","author":"T Wahl","year":"2010","unstructured":"Wahl, T., Donaldson, A.: Replication and abstraction: symmetry in automated formal verification. Symmetry 2(2), 799\u2013847 (2010)","journal-title":"Symmetry"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Models of Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17142-5_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T07:23:14Z","timestamp":1676445794000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17142-5_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319171418","9783319171425"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17142-5_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}