{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T12:12:39Z","timestamp":1774095159635,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906596","type":"print"},{"value":"9783031906602","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checking. OBDDs allow for efficient algorithms using top-down dynamic programming. From an automata-theoretic perspective, OBDDs essentially are minimal deterministic finite automata recognizing languages whose words have a fixed length (the arity of the Boolean function). We introduce weakly acyclic diagrams (WADs), a generalization of OBDDs that maintains their algorithmic advantages, but can also represent infinite languages. We develop the theory of WADs and show that they can be used for symbolic model checking of various models of infinite-state systems.<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_2","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:19Z","timestamp":1746005899000},"page":"23-42","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Weakly Acyclic Diagrams: A Data Structure for Infinite-State Symbolic Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2914-2734","authenticated-orcid":false,"given":"Michael","family":"Blondin","sequence":"first","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9828-9129","authenticated-orcid":false,"given":"Micha\u00ebl","family":"Cadilhac","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Xin-Yi","family":"Cui","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1786-9592","authenticated-orcid":false,"given":"Philipp","family":"Czerner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-2596-0920","authenticated-orcid":false,"given":"Jakob","family":"Schulz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A.: Regular model checking. International Journal on Software Tools for Technology Transfer 14(2), 109\u2013118 (2012). https:\/\/doi.org\/10.1007\/S10009-011-0216-8","DOI":"10.1007\/S10009-011-0216-8"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A.: Regular model checking: Evolution and perspectives. In: Model Checking, Synthesis, and Learning \u2013 Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 13030, pp. 78\u201396. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-91384-7_5","DOI":"10.1007\/978-3-030-91384-7_5"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: Proc. $$\\text{11}^\\text{th }$$ Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 313\u2013321. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561359","DOI":"10.1109\/LICS.1996.561359"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: Proc. $$\\text{8 }^\\text{ th }$$ Annual Symposium on Logic in Computer Science (LICS). pp. 160\u2013170 (1993). https:\/\/doi.org\/10.1109\/LICS.1993.287591","DOI":"10.1109\/LICS.1993.287591"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Proc. $$\\text{15 }^\\text{ th }$$ International Conference on Concurrency Theory (CONCUR). vol.\u00a03170, pp. 35\u201348. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-28644-8_3","DOI":"10.1007\/978-3-540-28644-8_3"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Kindahl, M.: Decidability of simulation and bisimulation between lossy channel systems and finite state systems (extended abstract). In: Proc. $$\\text{6 }^\\text{ th }$$ International Conference on Concurrency Theory (CONCUR). vol.\u00a0962, pp. 333\u2013347. Springer (1995). https:\/\/doi.org\/10.1007\/3-540-60218-6_25","DOI":"10.1007\/3-540-60218-6_25"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Sistla, A.P., Talupur, M.: Model checking parameterized systems. In: Handbook of Model Checking, pp. 685\u2013725. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_21","DOI":"10.1007\/978-3-319-10575-8_21"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Akers, S.: Binary decision diagrams. IEEE Transactions on Computers 27(6), 509\u2013516 (1978), https:\/\/doi.org\/10.1109\/TC.1978.1675141","DOI":"10.1109\/TC.1978.1675141"},{"key":"2_CR9","unstructured":"Andersen, H.R.: An introduction to binary decision diagrams (1998)"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Blondin, M., Cadilhac, M., Cui, X., Czerner, P., Esparza, J., Schulz, J.: Weakly acyclic diagrams: A data structure for infinite-state symbolic verification. CoRR abs\/2411.17250 (2024). https:\/\/doi.org\/10.48550\/arXiv.2411.17250","DOI":"10.48550\/arXiv.2411.17250"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. Formal Methods in System Design (FMSD) 14(3), 237\u2013255 (1999). https:\/\/doi.org\/10.1023\/A:1008719024240","DOI":"10.1023\/A:1008719024240"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Muscholl, A., Touili, T.: Permutation rewriting and algorithmic verification. Information and Computation 205(2), 199\u2013224 (2007). https:\/\/doi.org\/10.1016\/J.IC.2005.11.007","DOI":"10.1016\/J.IC.2005.11.007"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677\u2013691 (1986). https:\/\/doi.org\/10.1109\/TC.1986.1676819","DOI":"10.1109\/TC.1986.1676819"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Bryant, R.E.: Binary decision diagrams. In: Handbook of Model Checking, pp. 191\u2013217. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_7","DOI":"10.1007\/978-3-319-10575-8_7"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Brzozowski, J.A., Fich, F.E.: Languages of $$\\cal{R}$$-trivial monoids. Journal of Computer and System Sciences 20(1), 32\u201349 (1980), https:\/\/doi.org\/10.1016\/0022-0000(80)90003-3","DOI":"10.1016\/0022-0000(80)90003-3"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Chaki, S., Gurfinkel, A.: BDD-based symbolic model checking. In: Handbook of Model Checking, pp. 219\u2013245. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_8","DOI":"10.1007\/978-3-319-10575-8_8"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Czerner, P., Esparza, J., Krasotin, V., Welzel-Mohr, C.: Computing inductive invariants of regular abstraction frameworks. In: Proc. $$\\text{35 }^\\text{ th }$$ International Conference on Concurrency Theory (CONCUR). LIPIcs, vol.\u00a0311, pp. 19:1\u201319:18 (2024). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2024.19, The tool dodo and the instances are available at https:\/\/zenodo.org\/records\/8354894.","DOI":"10.4230\/LIPICS.CONCUR.2024.19"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Delzanno, G., Raskin, J., Begin, L.V.: Covering sharing trees: a compact data structure for parameterized verification. International Journal on Software Tools for Technology Transfer (STTT) 5(2-3), 268\u2013297 (2004). https:\/\/doi.org\/10.1007\/S10009-003-0110-0","DOI":"10.1007\/S10009-003-0110-0"},{"key":"2_CR19","unstructured":"Eilenberg, S.: Automata, Languages, and Machines, vol.\u00a0B. Academic Press (1976)"},{"key":"2_CR20","unstructured":"Esparza, J., Blondin, M.: Automata theory: An algorithmic approach. MIT Press (2023)"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proc. $$\\text{14 }^\\text{ th }$$ Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 352\u2013359. IEEE Computer Society (1999). https:\/\/doi.org\/10.1109\/LICS.1999.782630","DOI":"10.1109\/LICS.1999.782630"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P.J., Niksic, F.: An SMT-based approach to coverability analysis. In: Proc. $$\\text{26 }^\\text{ th }$$ International Conference on Computer Aided Verification (CAV). pp. 603\u2013619. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_40","DOI":"10.1007\/978-3-319-08867-9_40"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Finkel, A., Schnoebelen, Ph.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63\u201392 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00102-X","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"2_CR24","unstructured":"Ganty, P., Meuter, C., Delzanno, G., Kalyon, G., Raskin, J.F., Van Begin, L.: Symbolic data structure for sets of $$k$$-uples. Tech. Rep.\u00a0570, Universit\u00e9 Libre de Bruxelles, Belgium (2007)"},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Geffroy, T., Leroux, J., Sutre, G.: Backward coverability with pruning for lossy channel systems. In: Proc. $$\\text{24 }^\\text{ th }$$ ACM SIGSOFT International Symposium on Model Checking of Software (SPIN). pp. 132\u2013141. ACM (2017). https:\/\/doi.org\/10.1145\/3092282.3092292, The tool BML and the lossy channel system instances are available at https:\/\/dept-info.labri.fr\/~tgeffroy\/lcs\/.","DOI":"10.1145\/3092282.3092292"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"Heu\u00dfner, A., Gall, T.L., Sutre, G.: Extrapolation-based path invariants for abstraction refinement of FIFO systems. In: Proc. $$\\text{16 }^\\text{ th }$$ International on Model Checking Software (SPIN). pp. 107\u2013124. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02652-2_11, The tool mcscm is available at https:\/\/svn.labri.fr\/repos\/acs\/www\/redmine\/projects\/mcscm\/wiki.html","DOI":"10.1007\/978-3-642-02652-2_11"},{"key":"2_CR27","doi-asserted-by":"publisher","unstructured":"Heu\u00dfner, A., Gall, T.L., Sutre, G.: McScM: A general framework for the verification of communicating machines. In: Proc. $$\\text{18 }^\\text{ th }$$ International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 478\u2013484. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_34","DOI":"10.1007\/978-3-642-28756-5_34"},{"key":"2_CR28","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Version 1.4 User Manual. BRICS, Department of Computer Science, University of Aarhus (January 2001), notes Series NS-01-1. Available from http:\/\/www.brics.dk\/mona\/"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Kr\u00f6tzsch, M., Masopust, T., Thomazo, M.: Complexity of universality and related problems for partially ordered NFAs. Information and Computation 255, 177\u2013192 (2017). https:\/\/doi.org\/10.1016\/j.ic.2017.06.004","DOI":"10.1016\/j.ic.2017.06.004"},{"key":"2_CR30","doi-asserted-by":"publisher","unstructured":"Masopust, T., Kr\u00f6tzsch, M.: Partially ordered automata and piecewise testability. Logical Methods in Computer Science 17(2) (2021). https:\/\/doi.org\/10.23638\/LMCS-17(2:14)2021","DOI":"10.23638\/LMCS-17(2:14)2021"},{"key":"2_CR31","doi-asserted-by":"publisher","unstructured":"Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541\u2013580 (1989). https:\/\/doi.org\/10.1109\/5.24143","DOI":"10.1109\/5.24143"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"\u00c9ric Pin, J.: Varieties of formal languages. North Oxford, London and Plenum (1986)","DOI":"10.1007\/978-1-4613-2215-3"},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Ryzhikov, A., Wolf, P.: Monoids of upper triangular matrices over the Boolean semiring. In: Proc. $$\\text{49 }^\\text{ th }$$ International Symposium on Mathematical Foundations of Computer Science (MFCS). LIPIcs, vol.\u00a0306, pp. 81:1\u201381:18 (2024). https:\/\/doi.org\/10.4230\/LIPICS.MFCS.2024.81","DOI":"10.4230\/LIPICS.MFCS.2024.81"},{"key":"2_CR34","doi-asserted-by":"publisher","unstructured":"Schwentick, T., Th\u00e9rien, D., Vollmer, H.: Partially-ordered two-way automata: A new characterization of DA. In: Proc. $$\\text{5 }^\\text{ th }$$ International Conference on Developments in Language Theory (DLT). vol.\u00a02295, pp. 239\u2013250. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-46011-X_20","DOI":"10.1007\/3-540-46011-X_20"},{"key":"2_CR35","unstructured":"Welzel-Mohr, C.: Inductive Statements for Regular Transition Systems. Ph.D. thesis, Technical University of Munich, Germany (2024), https:\/\/mediatum.ub.tum.de\/1721365"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90660-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:25Z","timestamp":1746005905000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}