{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T19:37:21Z","timestamp":1774294641884,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540229407","type":"print"},{"value":"9783540286448","type":"electronic"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-28644-8_3","type":"book-chapter","created":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T14:48:13Z","timestamp":1267109293000},"page":"35-48","source":"Crossref","is-referenced-by-count":74,"title":["A Survey of Regular Model Checking"],"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":"Mayank","family":"Saksena","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/BFb0028754","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"1998","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy fifo channels. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 305\u2013318. Springer, Heidelberg (1998)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1007\/3-540-45657-0_47","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"2002","unstructured":"Abdulla, P.A., Jonsson, B., Mahata, P., d\u2019Orso, J.: Regular tree model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 555. Springer, Heidelberg (2002)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular model checking for MSO + LTL. In: Proc. 16th Int. Conf. on Computer Aided Verification (to appear, 2004)","DOI":"10.1007\/978-3-540-27813-9_27"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/3-540-45694-5_9","volume-title":"CONCUR 2002 - Concurrency Theory","author":"P.A. Abdulla","year":"2002","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Regular model checking made simple and efficient. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 116\u2013130. Springer, Heidelberg (2002)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-540-45069-6_25","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"2003","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Algorithmic improvements in regular model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 236\u2013248. Springer, Heidelberg (2003)"},{"key":"3_CR6","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098, 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243. Springer, Heidelberg (1997)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-61474-5_53","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1996","unstructured":"Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 1\u201312. Springer, Heidelberg (1996)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. of the Fourth International Static Analysis Symposium","author":"B. Boigelot","year":"1997","unstructured":"Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs. In: Proc. of the Fourth International Static Analysis Symposium. LNCS. Springer, Heidelberg (1997)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of fifochannel systems with nonregular sets of configurations. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.\u00a01256. Springer, Heidelberg (1997)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-27813-9_29","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2004","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 372\u2013386. Springer, Heidelberg (2004) (to appear)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 403\u2013418. Springer, Heidelberg (2000)"},{"issue":"3","key":"3_CR13","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1023\/A:1008644009416","volume":"13","author":"D.A. Basin","year":"1998","unstructured":"Basin, D.A., Klarlund, N.: Automata based symbolic reasoning in hardware verification. Formal Methods in Systems Design\u00a013(3), 255\u2013288 (1998)","journal-title":"Formal Methods in Systems Design"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-45069-6_24","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 223\u2013235. Springer, Heidelberg (2003)"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/978-3-540-24730-2_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Boigelot","year":"2004","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Omega-regular model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 561\u2013575. Springer, Heidelberg (2004)"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/3-540-45657-0_46","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2002","unstructured":"Bouajjani, A., Touili, T.: Extrapolating Tree Transformations. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 539. Springer, Heidelberg (2002)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1994","unstructured":"Boigelot, B., Wolper, P.: Symbolic verification with periodic sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 55\u201367. Springer, Heidelberg (1994)"},{"issue":"1","key":"3_CR18","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/0304-3975(92)90278-N","volume":"106","author":"D. Caucal","year":"1992","unstructured":"Caucal, D.: On the regular structure of prefix rewriting. Theoretical Computer Science\u00a0106(1), 61\u201386 (1992)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"3_CR19","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028751","volume-title":"Computer Aided Verification","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/3-540-44585-4_27","volume-title":"Computer Aided Verification","author":"D.R. Dams","year":"2001","unstructured":"Dams, D.R., Lakhnech, Y., Steffen, M.: Iterating transducers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 286. Springer, Heidelberg (2001)"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 324\u2013336. Springer, Heidelberg (2001)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/3-540-45294-X_14","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"D. Fisman","year":"2001","unstructured":"Fisman, D., Pnueli, A.: Beyond regular model checking. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, p. 156. Springer, Heidelberg (2001)"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems (extended abstract). In: Proc.Infinity 1997, Electronic Notes in Theoretical Computer Science, Bologna (August 1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.G. Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019. Springer, Heidelberg (1995)"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/3-540-46419-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Jonsson","year":"2000","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, p. 220. Springer, Heidelberg (2000)"},{"key":"3_CR27","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(00)00103-1","volume":"256","author":"Y. Kesten","year":"2001","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theoretical Computer Science\u00a0256, 93\u2013112 (2001)","journal-title":"Theoretical Computer Science"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055036","volume-title":"Automata, Languages and Programming","author":"Y. Kesten","year":"1998","unstructured":"Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 1\u201316. Springer, Heidelberg (1998)"},{"issue":"3","key":"3_CR29","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. on Programming Languages and Systems\u00a016(3), 872\u2013923 (1994)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"3","key":"3_CR30","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G.E. Peterson","year":"1981","unstructured":"Peterson, G.E., Stickel, M.E.: Myths about the mutal exclusion problem. Information Processing Letters\u00a012(3), 115\u2013116 (1981)","journal-title":"Information Processing Letters"},{"key":"3_CR31","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":"J.P. 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.\u00a0137, pp. 337\u2013352. Springer, Heidelberg (1982)"},{"key":"#cr-split#-3_CR32.1","doi-asserted-by":"crossref","unstructured":"Touili, T.: Regular Model Checking using Widening Techniques. Electronic Notes in Theoretical Computer Science\u00a050(4) (2001);","DOI":"10.1016\/S1571-0661(04)00187-2"},{"key":"#cr-split#-3_CR32.2","unstructured":"In: Proc. Workshop on Verification of Parametrized Systems (VEPAS 2001), Crete (July 2001)"},{"key":"3_CR33","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. LICS 1986, 1st IEEE Int. Symp. on Logic in Computer Science, pp. 332\u2013344 (June 1986)"},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2004 - Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-28644-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T07:53:31Z","timestamp":1558857211000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-28644-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540229407","9783540286448"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-28644-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}