{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:20:03Z","timestamp":1784830803580,"version":"3.55.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319899626","type":"print"},{"value":"9783319899633","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89963-3_22","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T18:53:00Z","timestamp":1523645580000},"page":"379-395","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Symmetry Reduction for the Local Mu-Calculus"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard J.","family":"Trefler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-35873-9_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 476\u2013495. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_28"},{"issue":"6","key":"22_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-02658-4_9","volume-title":"Computer Aided Verification","author":"G Basler","year":"2009","unstructured":"Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Symbolic counter abstraction for concurrent software. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 64\u201378. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_9"},{"issue":"1","key":"22_CR4","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"MC Browne","year":"1989","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81(1), 13\u201331 (1989)","journal-title":"Inf. Comput."},{"issue":"1\u20132","key":"22_CR5","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1\u20132), 77\u2013104 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-540-73368-3_9","volume-title":"Computer Aided Verification","author":"A Cohen","year":"2007","unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 55\u201367. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_9"},{"key":"22_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E Dijkstra","year":"1990","unstructured":"Dijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Springer, New York (1990). https:\/\/doi.org\/10.1007\/978-1-4612-3228-5"},{"issue":"1\u20132","key":"22_CR8","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 Syst. Des. 9(1\u20132), 105\u2013131 (1996)","journal-title":"Formal Methods Syst. Des."},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Havlicek, J., Trefler, R.J.: Virtual symmetry reduction. In: LICS, pp. 121\u2013131. IEEE Computer Society (2000)","DOI":"10.1109\/LICS.2000.855761"},{"key":"22_CR10","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":"22_CR11","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1090\/S0273-0979-06-01108-6","volume":"43","author":"M Golubitsky","year":"2006","unstructured":"Golubitsky, M., Stewart, I.: Nonlinear dynamics of networks: the groupoid formalism. Bull. Am. Math. Soc. 43, 305\u2013364 (2006)","journal-title":"Bull. Am. Math. Soc."},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Shoham, S., Meshman, Y.: SMT-based verification of parameterized systems. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, New York, NY, USA, pp. 338\u2013348 (2016)","DOI":"10.1145\/2950290.2950330"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: a pearl in compositional verification. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017, pp. 473\u2013485. ACM (2017)","DOI":"10.1145\/3009837.3009893"},{"issue":"1\/2","key":"22_CR14","first-page":"41","volume":"9","author":"C Ip","year":"1996","unstructured":"Ip, C., Dill, D.: Better verification through symmetry. Formal Methods Syst. Des. 9(1\/2), 41\u201375 (1996)","journal-title":"Formal Methods Syst. Des."},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/BFb0012782","volume-title":"Automata, Languages and Programming","author":"D Kozen","year":"1982","unstructured":"Kozen, D.: Results on the propositional $$\\upmu $$ \u03bc -calculus. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 348\u2013359. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0012782"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-69738-1_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KS Namjoshi","year":"2007","unstructured":"Namjoshi, K.S.: Symmetry and completeness in the analysis of parameterized systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 299\u2013313. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_22"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-27940-9_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KS Namjoshi","year":"2012","unstructured":"Namjoshi, K.S., Trefler, R.J.: Local symmetry and compositional verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 348\u2013362. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_23"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-662-46681-0_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KS Namjoshi","year":"2015","unstructured":"Namjoshi, K.S., Trefler, R.J.: Analysis of dynamic process networks. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 164\u2013178. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_11"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-19195-9_7","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"KS Namjoshi","year":"2015","unstructured":"Namjoshi, K.S., Trefler, R.J.: Loop freedom in AODVv2. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 98\u2013112. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19195-9_7"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-662-49674-9_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KS Namjoshi","year":"2016","unstructured":"Namjoshi, K.S., Trefler, R.J.: Parameterized compositional model checking. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 589\u2013606. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_39"},{"issue":"5","key":"22_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279\u2013285 (1976)","journal-title":"Commun. ACM"},{"key":"22_CR22","volume-title":"Applied Combinatorics","author":"F Roberts","year":"1984","unstructured":"Roberts, F.: Applied Combinatorics. Prentice-Hall, Upper Saddle River (1984). ISBN 0-13-039313-4"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-74061-2_5","volume-title":"Static Analysis","author":"S Shoham","year":"2007","unstructured":"Shoham, S., Grumberg, O.: Compositional verification and 3-valued abstractions join forces. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 69\u201386. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_5"},{"key":"22_CR24","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/3-540-52148-8_13","volume-title":"Automatic Verification Methods for Finite State Systems","author":"Ze'ev Shtadler","year":"1990","unstructured":"Shtadler, Z., Grumberg, O.: Network grammars, communication behaviors and automatic verification. In: Sifakis [25], pp. 151\u2013165"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52148-8","volume-title":"Automatic Verification Methods for Finite State Systems","year":"1990","unstructured":"Sifakis, J. (ed.): CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8"},{"key":"22_CR26","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume-title":"Automatic Verification Methods for Finite State Systems","author":"Pierre Wolper","year":"1990","unstructured":"Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis [25], pp. 68\u201380"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89963-3_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,3]],"date-time":"2025-07-03T17:29:23Z","timestamp":1751563763000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89963-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319899626","9783319899633"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89963-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"14 April 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thessaloniki","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/index.php\/2018\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}