{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T04:59:32Z","timestamp":1773723572726,"version":"3.50.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031661488","type":"print"},{"value":"9783031661495","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-66149-5_3","type":"book-chapter","created":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:01:54Z","timestamp":1728716514000},"page":"49-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Synchronisation in\u00a0Language-Level Symmetry Reduction for\u00a0Probabilistic Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1116-875X","authenticated-orcid":false,"given":"Ivaylo","family":"Valkov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7448-7961","authenticated-orcid":false,"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0941-1717","authenticated-orcid":false,"given":"Alice","family":"Miller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,13]]},"reference":[{"key":"3_CR1","unstructured":"Prism - case studies. https:\/\/www.prismmodelchecker.org\/casestudies\/index.php. Accessed 15 Mar 2024"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/10722468_1","volume-title":"SPIN Model Checking and Software Verification","author":"D Bo\u0161na\u010dki","year":"2000","unstructured":"Bo\u0161na\u010dki, D., Dams, D., Holenderski, L.: Symmetric spin. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 1\u201319. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722468_1"},{"issue":"8","key":"3_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986). https:\/\/doi.org\/10.1109\/TC.1986.1676819","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"3_CR4","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992). https:\/\/doi.org\/10.1145\/136035.136043","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"3_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10-20 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90017-A","journal-title":"Inf. Comput."},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Cachin, C., Kursawe, K., Shoup, V.: Random oracles in constantipole: practical asynchronous byzantine agreement using cryptography (extended abstract). In: Neiger, G. (ed.) Proceedings of the Nineteenth Annual ACM Symposium on Principles of Distributed Computing, 16\u201319 July 2000, Portland, Oregon, USA, pp. 123\u2013132. ACM (2000). https:\/\/doi.org\/10.1145\/343477.343531","DOI":"10.1145\/343477.343531"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. STTT 2, 410\u2013425 (2000). https:\/\/doi.org\/10.1007\/s100090050046","journal-title":"STTT"},{"issue":"2","key":"3_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986). https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR9","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model Checking, second edition. Cyber Physical Systems Series. MIT Press (2018). https:\/\/books.google.co.uk\/books?id=qJl8DwAAQBAJ"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., McMillan, K., Zhaor, X., Fujita, M., Yang, J.: Spectral transforms for large boolean functions with applications to technology mapping. In: Proceedings of the 30th ACM\/IEEE Design Automation Conference, pp. 54\u201360. IEEE Computer Society Press (1993)","DOI":"10.1145\/157485.164569"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9, 77\u2013104 (1996). https:\/\/api.semanticscholar.org\/CorpusID:14472493","DOI":"10.1007\/BF00625969"},{"key":"3_CR12","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). https:\/\/doi.org\/10.1007\/11901914_4"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Donaldson, A.F., Miller, A., Parker, D.: Language-level symmetry reduction for probabilistic model checking. In: QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, pp. 289 \u2013 298. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/QEST.2009.21","DOI":"10.1109\/QEST.2009.21"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/11813040_36","volume-title":"FM 2006: Formal Methods","author":"AF Donaldson","year":"2006","unstructured":"Donaldson, A.F., Miller, A.: Exact and approximate strategies for symmetry reduction in model checking. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 541\u2013556. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_36"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Miller, A., Parker, D.: GRIP: generic representatives in PRISM. In: Proceedings of the 4th International Conference on Quantitative Evaluation of Systems (QEST 2007), pp. 115\u2013116. IEEE Computer Society (2007)","DOI":"10.1109\/QEST.2007.30"},{"key":"3_CR16","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":"EA Emerson","year":"1999","unstructured":"Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: new techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142\u2013157. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_12"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-39724-3_20","volume-title":"Correct Hardware Design and Verification Methods","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Wahl, T.: On combining symmetry reduction and symbolic representation for efficient model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 216\u2013230. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39724-3_20"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-40903-8_5","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Hendriks","year":"2004","unstructured":"Hendriks, M., Behrmann, G., Larsen, K., Niebert, P., Vaandrager, F.: Adding symmetry reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 46\u201359. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-40903-8_5"},{"key":"3_CR19","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. CoRR abs\/2002.07080 (2020). https:\/\/arxiv.org\/abs\/2002.07080"},{"key":"3_CR20","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2011","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2011)","edition":"1"},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-319-10575-8_5","volume-title":"Handbook of Model Checking","author":"GJ Holzmann","year":"2018","unstructured":"Holzmann, G.J.: Explicit-state model checking. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 153\u2013171. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_5"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"IEEE Computer Society: IEEE standard for information technology-telecommunications and information exchange between systems-local and metropolitan area networks-specific requirements part 3: Carrier sense multiple access with collision detection (CSMA\/CD) access method and physical layer specifications. IEEE STD 802.3-2002 (Revision of IEEE STD 802.3, 2000 edn), pp. 1\u20131550 (2002). https:\/\/doi.org\/10.1109\/IEEESTD.2002.93570","DOI":"10.1109\/IEEESTD.2002.93570"},{"key":"3_CR23","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). https:\/\/doi.org\/10.1007\/11817963_23"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Miller, A., Donaldson, A.F., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3) (2006). https:\/\/doi.org\/10.1145\/1132960.1132962. http:\/\/eprints.gla.ac.uk\/3197\/","DOI":"10.1145\/1132960.1132962"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"JP Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/3-540-11494-7_22"},{"key":"3_CR27","unstructured":"Valkov, I.: Formal analysis of communication protocols for wireless sensor systems. Ph.D. thesis, University of Glasgow, Glasgow, UK (2024, to appear)"},{"issue":"2","key":"3_CR28","doi-asserted-by":"publisher","first-page":"799","DOI":"10.3390\/SYM2020799","volume":"2","author":"T Wahl","year":"2010","unstructured":"Wahl, T., Donaldson, A.F.: Replication and abstraction: symmetry in automated formal verification. Symmetry 2(2), 799\u2013847 (2010). https:\/\/doi.org\/10.3390\/SYM2020799","journal-title":"Symmetry"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66149-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:03:44Z","timestamp":1728716624000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66149-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,13]]},"ISBN":["9783031661488","9783031661495"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66149-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,13]]},"assertion":[{"value":"13 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}