{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:20:50Z","timestamp":1770279650326,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540374060","type":"print"},{"value":"9783540374114","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_23","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T01:07:51Z","timestamp":1154740071000},"page":"234-248","source":"Crossref","is-referenced-by-count":65,"title":["Symmetry Reduction for Probabilistic Model Checking"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"23_CR1","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"15","author":"J. Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. Journal of Algorithms\u00a015(1), 441\u2013460 (1990)","journal-title":"Journal of Algorithms"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1995","unstructured":"Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, Springer, Heidelberg (1995)"},{"issue":"2\/3","key":"23_CR3","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"I. Bahar","year":"1997","unstructured":"Bahar, I., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. Formal Methods in System Design\u00a010(2\/3), 171\u2013206 (1997)","journal-title":"Formal Methods in System Design"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_28","volume-title":"Computer Aided Verification","author":"C. Baier","year":"2000","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"23_CR5","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.\u00a02404, p. 93. Springer, Heidelberg (2002)"},{"key":"23_CR6","unstructured":"Buchholz, P.: Markovian process algebra: Composition and equivalence. In: Proc. PAPM 1994, pp. 11\u201330 (1994)"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Cachin, C., Kursawe, K., Shoup, V.: Random oracles in Constantinople: Practical asynchronous Byzantine agreement using cryptography (extended abstract). In: Proc. Symposium on Principles of Distributed Computing, pp. 123\u2013132 (2000)","DOI":"10.1145\/343477.343531"},{"issue":"1\/2","key":"23_CR8","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E. Clarke","year":"1996","unstructured":"Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design\u00a09(1\/2), 77\u2013104 (1996)","journal-title":"Formal Methods in System Design"},{"issue":"2\/3","key":"23_CR9","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1008695706493","volume":"10","author":"E. Clarke","year":"1997","unstructured":"Clarke, E., Fujita, M., McGeer, P., McMillan, K., Yang, J., Zhao, X.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. Formal Methods in System Design\u00a010(2\/3), 149\u2013169 (1997)","journal-title":"Formal Methods in System Design"},{"key":"23_CR10","unstructured":"Donaldson, A., Miller, A.: Symmetry reduction for probabilistic systems. In: Proc. 12th workshop on Automated Reasoning, pp. 17\u201318 (2005)"},{"issue":"1\/2","key":"23_CR11","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E. Emerson","year":"1996","unstructured":"Emerson, E., Sistla, A.: Symmetry and model checking. Formal Methods in System Design\u00a09(1\/2), 105\u2013131 (1996)","journal-title":"Formal Methods in System Design"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-48153-2_12","volume-title":"Correct Hardware Design and Verification Methods","author":"E. Emerson","year":"1999","unstructured":"Emerson, E., Trefler, R.: From asymmetry to full symmetry: New techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 142\u2013157. Springer, Heidelberg (1999)"},{"key":"23_CR13","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":"E. Emerson","year":"2005","unstructured":"Emerson, E., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 382\u2013396. Springer, Heidelberg (2005)"},{"issue":"1-2","key":"23_CR14","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/S1567-8326(02)00066-8","volume":"56","author":"H. Hermanns","year":"2003","unstructured":"Hermanns, H., Kwiatkowska, M., Norman, G., Parker, D., Siegle, M.: On the use of MTBDDs for performability analysis and verification of stochastic systems. Journal of Logic and Algebraic Programming\u00a056(1-2), 23\u201367 (2003)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"23_CR15","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 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"23_CR16","unstructured":"IEEE 802.3-2002. IEEE Standard for Carrier Sense Multiple Access with Collision Detection (CSMA\/CD) (2002), http:\/\/standards.ieee.org\/getieee802\/802.3.html"},{"issue":"1-2","key":"23_CR17","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"C. Ip","year":"1996","unstructured":"Ip, C., Dill, D.: Better verification through symmetry. Formal Methods In System Design\u00a09(1-2), 41\u201375 (1996)","journal-title":"Formal Methods In System Design"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-36135-9_13","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G.: Verifying randomized Byzantine agreement. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 194\u2013209. Springer, Heidelberg (2002)"},{"issue":"2","key":"23_CR19","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","volume":"6","author":"M. Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer (STTT)\u00a06(2), 128\u2013142 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"issue":"4","key":"23_CR20","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/1059816.1059820","volume":"32","author":"M. Kwiatkowska","year":"2005","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking in practice: Case studies with PRISM. ACM SIGMETRICS Performance Evaluation Review\u00a032(4), 16\u201321 (2005)","journal-title":"ACM SIGMETRICS Performance Evaluation Review"},{"key":"23_CR21","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.\u00a02102, pp. 194\u2013206. Springer, Heidelberg (2001)"},{"key":"23_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K. Larsen","year":"1991","unstructured":"Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Information and Computation\u00a094, 1\u201328 (1991)","journal-title":"Information and Computation"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1, \u221e)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"key":"23_CR24","unstructured":"PRISM web site: http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/"},{"key":"23_CR25","doi-asserted-by":"crossref","unstructured":"Rutten, J., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. In: Panangaden, P., van Breugel, F. (eds.) American Mathematical Society (2004)","DOI":"10.1090\/crmm\/023"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/BFb0015027","volume-title":"CONCUR \u201994: Concurrency Theory","author":"R. Segala","year":"1994","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol.\u00a0836, pp. 481\u2013496. Springer, Heidelberg (1994)"},{"key":"23_CR27","unstructured":"Somenzi, F.: CUDD: Colorado University decision diagram package. Public software, Colorado Univeristy, Boulder, http:\/\/vlsi.colorado.edu\/~fabio\/"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:15:57Z","timestamp":1605626157000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/11817963_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}