{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T14:16:12Z","timestamp":1778249772190,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540440437","type":"print"},{"value":"9783540456940","type":"electronic"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"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":[[2002]]},"DOI":"10.1007\/3-540-45694-5_9","type":"book-chapter","created":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T03:44:18Z","timestamp":1191555858000},"page":"116-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["Regular Model Checking Made Simple and Effcient*"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcus","family":"Nilsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"d'Orso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,18]]},"reference":[{"key":"9_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/BFb0028754","volume-title":"On-the-fly analysis of systems with unbounded, lossy fifo channels","author":"P. A. Abdulla","year":"1998","unstructured":"Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson. On-the-fly analysis of systems with unbounded, lossy fifo channels. In Proc. CAV\u2019 98, volume 1427 of LNCS, pages 305\u2013318, 1998."},{"key":"9_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"Handling global conditions in parameterized system verification","author":"P. A. Abdulla","year":"1999","unstructured":"Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, and Marcus Nilsson. Handling global conditions in parameterized system verification. In Proc. CAV\u201999, volume 1633 of LNCS, pages 134\u2013145, 1999."},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"9_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Reachability Analysis of Pushdown Automata: Application to Model Checking","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata: Application to Model Checking. In Proc. CONCUR\u201997. LNCS 1243, 1997."},{"key":"9_CR5","unstructured":"B. Boigelot, J.-M. Fran\u00c7ois, and L. Latour. The Li\u00e9ge automata-based symbolic handler (lash). Available at http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/ research\/lash\/."},{"key":"9_CR6","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Symbolic verification of communication protocols with infinite state spaces using QDDs","author":"B. Boigelot","year":"1996","unstructured":"B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In Alur and Henzinger, editors, Proc. CAV\u201996, volume 1102 of LNCS, pages 1\u201312. Springer Verlag, 1996."},{"key":"9_CR7","series-title":"Lect Notes Comput Sci","volume-title":"The power of QDDs","author":"B. Boigelot","year":"1997","unstructured":"B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In Proc. of the Fourth International Static Analysis Symposium, LNCS. Springer Verlag, 1997."},{"key":"9_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Symbolic reachability analysis of fifochannel systems with nonregular sets of configurations","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani and P. Habermehl. Symbolic reachability analysis of fifochannel systems with nonregular sets of configurations. In Proc. ICALP\u2019 97, 24th International Colloquium on Automata, Lnaguages, and Programming, volume 1256 of LNCS, 1997."},{"key":"9_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Regular model checking","author":"A. Bouajjani","year":"2000","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In Emerson and Sistla, editors, Proc. CAV \u2ad70, volume 1855 of LNCS, pages 403\u2013418, 2000."},{"key":"9_CR10","unstructured":"A. Bouajjani, A. Muscholl, and T. Touili. Permutation rewriting and algorithmic verification. In Proc. LICS\u2019 01 17th IEEE Int. Symp. on Logic in Computer Science. IEEE, 2001."},{"key":"9_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"Symbolic verification with periodic sets","author":"B. Boigelot","year":"1994","unstructured":"B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Proc. CAV\u201994, volume 818 of LNCS, pages 55\u201367. Springer Verlag, 1994."},{"issue":"1","key":"9_CR12","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/0304-3975(92)90278-N","volume":"106","author":"D. Caucal","year":"1992","unstructured":"Didier Caucal. On the regular structure of prefix rewriting. Theoretical Computer Science, 106(1):61\u201386, Nov. 1992.","journal-title":"Theoretical Computer Science"},{"key":"9_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/3-540-46432-8_4","volume-title":"FOSSACS 2000","author":"D. Caucal","year":"2000","unstructured":"Didier Caucal. On word rewriting systems having a rational derivation. In FOSSACS 2000, volume 1784 of LNCS, pages 48\u201362, April 2000."},{"key":"9_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027094","volume-title":"CAV\u201998","author":"H. Comon","year":"1998","unstructured":"H. Comon and Y. Jurski. Multiple counters automata, safety analysis and presburger arithmetic. In CAV\u201998. LNCS 1427, 1998."},{"key":"9_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Iterating transducers","author":"D. Dams","year":"2001","unstructured":"D. Dams, Y. Lakhnech, and M. Steffen. Iterating transducers. In G. Berry, H. Comon, and A. Finkel, editors, Proc. CAV\u2019 01, volume 2102 of LNCS, 2001."},{"key":"9_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"A bdd-based model checker for recursive programs","author":"J. Esparza","year":"2001","unstructured":"J. Esparza and S. Schwoon. A bdd-based model checker for recursive programs. In Proc. CAV\u201901, volume 2102 of LNCS, pages 324\u2013336, 2001."},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems (extended abstract). In Proc. Infinity\u2019 97, Electronic Notes in Theoretical Computer Science, Bologna, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"9_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Mona: Monadic second-order logic in practice","author":"J. G. Henriksen","year":"1996","unstructured":"J. G. Henriksen, J. Jensen, M. J\u00f8rgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Proc. TACAS\u201995, volume 1019 of LNCS, 1996."},{"key":"9_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Transitive closures of regular relations for verifying infinite-state systems","author":"B. Jonsson","year":"2000","unstructured":"Bengt Jonsson and Marcus Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In S. Graf and M. Schwartzbach, editors, Proc. TACAS\u201900, volume 1785 of LNCS, 2000."},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In O. Grumberg, editor, Proc. CAV\u201997, volume 1254, pages 424\u2013435, Haifa, Israel, 1997. Springer Verlag.","DOI":"10.1007\/3-540-63166-6_41"},{"key":"9_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BFb0035388","volume-title":"Mosel: A fiexible toolset for monadic second-order logic","author":"P. Kelb","year":"1997","unstructured":"P. Kelb, T. Margaria, M. Mendler, and C. Gsottberger. Mosel: A fiexible toolset for monadic second-order logic. In Proc. TACAS\u201997, volume 1217 of LNCS, pages 183\u2013202, Heidelberg, Germany, March 1997. Springer Verlag."},{"key":"9_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/10722167_26","volume-title":"Liveness and acceleration in parameterized verification","author":"A. Pnueli","year":"2000","unstructured":"A. Pnueli and E. Shahar. Liveness and acceleration in parameterized verification. In Proc. CAV '00, volume 1855 of LNCS, pages 328\u2013343, 2000."},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"T. Touili. Regular Model Checking using Widening Techniques. Electronic Notes in Theoretical Computer Science, 50(4), 2001. Proc. Workshop on Verification of Parametrized Systems (VEPAS\u201901), Crete, July, 2001.","DOI":"10.1016\/S1571-0661(04)00187-2"},{"key":"9_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Verifying systems with infinite but regular state spaces","author":"P. Wolper","year":"1998","unstructured":"Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. In Proc. CAV\u201998, volume 1427 of LNCS, pages 88\u201397, Vancouver, July 1998. Springer Verlag."}],"container-title":["Lecture Notes in Computer Science","CONCUR 2002 \u2014 Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45694-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T13:50:23Z","timestamp":1778248223000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-45694-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440437","9783540456940"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45694-5_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"18 September 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}