{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:05:13Z","timestamp":1781172313474,"version":"3.54.1"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,12,7]],"date-time":"2011-12-07T00:00:00Z","timestamp":1323216000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10009-011-0216-8","type":"journal-article","created":{"date-parts":[[2011,12,6]],"date-time":"2011-12-06T17:50:45Z","timestamp":1323193845000},"page":"109-118","source":"Crossref","is-referenced-by-count":27,"title":["Regular model checking"],"prefix":"10.1007","volume":"14","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2011,12,7]]},"reference":[{"key":"216_CR1","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular model checking for S1S + LTL, In this volume (2012)"},{"issue":"4","key":"216_CR2","doi-asserted-by":"crossref","first-page":"457","DOI":"10.2178\/bsl\/1294171129","volume":"16","author":"P.A. Abdulla","year":"2010","unstructured":"Abdulla P.A.: Well (and better) quasi-ordered transition systems. Bull. Symb. Log. 16(4), 457\u2013515 (2010)","journal-title":"Bull. Symb. Log."},{"key":"216_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bjesse, P., E\u00e9n, N.: Symbolic reachability analysis based on sat-solvers. In: Graf, S., Schwartzbach, M.I. (eds.), Tools and algorithms for construction and analysis of systems, Proceedings of the 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25\u2013April 2, 2000. Lecture Notes in Computer Science, vol. 1785, pp 411\u2013425. Springer, Berlin (2000)","DOI":"10.1007\/3-540-46419-0_28"},{"key":"216_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy fifo channels. In: Hu, AJ., Vardi, M.Y. (eds.), Computer Aided Verification, Proceedings of the 10th International Conference, CAV \u201998, Vancouver, BC, Canada, June 28\u2013July 2, 1998. Lecture Notes in Computer Science, vol. 1427, pp. 305\u2013318, Springer, Berlin (1998)","DOI":"10.1007\/BFb0028754"},{"key":"216_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M.: Handling global conditions in parameterized system verification. In: Halbwachs, N., Peled, D. (eds.), CAV. Lecture Notes in Computer Science, vol. 1633, pp. 134\u2013145. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48683-6_14"},{"key":"216_CR6","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"216_CR7","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Chen, Y.-F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.), TACAS. Lecture Notes in Computer Science, vol. 6015, pp. 158\u2013174. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"216_CR8","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.), TACAS. Lecture Notes in Computer Science, vol. 4424, pp. 721\u2013736. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71209-1_56"},{"key":"216_CR9","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: LICS, pp. 160\u2013170. IEEE Computer Society, Montreal, Canada (1993)","DOI":"10.1109\/LICS.1993.287591"},{"key":"216_CR10","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Mahata, P., d\u2019Orso, J.: Regular tree model checking. In: Brinksma, E., Larsen, K.G. (eds.), Computer Aided Verification, Proceedings of the 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27\u201331, 2002. Lecture Notes in Computer Science, vol. 2404, pp. 555\u2013568, Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_47"},{"key":"216_CR11","first-page":"116","volume-title":"CONCUR. Lecture Notes in Computer Science, vol. 2421","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., Jancar, P., Kret\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR. Lecture Notes in Computer Science, vol. 2421, pp. 116\u2013130. Springer, Berlin (2002)"},{"key":"216_CR12","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: LICS. pp. 414\u2013425. IEEE Computer Society, USA (1990)","DOI":"10.1109\/LICS.1990.113766"},{"key":"216_CR13","first-page":"474","volume-title":"ATVA. Lecture Notes in Computer Science, vol. 3707","author":"S. Bardin","year":"2005","unstructured":"Bardin S., Finkel A., Leroux J., Schnoebelen P.: Flat acceleration in symbolic model checking. In: Peled, D., Tsay, Y.-K. (eds.) ATVA. Lecture Notes in Computer Science, vol. 3707, pp. 474\u2013488. Springer, Berlin (2005)"},{"key":"216_CR14","unstructured":"Boigelot, B.: Domain-specific regular accelaration, 2012. In this volume"},{"key":"216_CR15","first-page":"1","volume-title":"CAV. Lecture Notes in Computer Science, vol. 1102","author":"B. Boigelot","year":"1996","unstructured":"Boigelot B., Godefroid P.: Symbolic verification of communication protocols with infinite state spaces using qdds (extended abstract). In: Alur, R., Henzinger, T.A. (eds.) CAV. Lecture Notes in Computer Science, vol. 1102, pp. 1\u201312. Springer, Berlin (1996)"},{"key":"216_CR16","first-page":"172","volume-title":"SAS. Lecture Notes in Computer Science, vol. 1302","author":"B. Boigelot","year":"1997","unstructured":"Boigelot B., Godefroid P., Willems B., Wolper P.: The power of qdds (extended abstract). In: Hentenryck, P.V. (ed.) SAS. Lecture Notes in Computer Science, vol. 1302, pp. 172\u2013186. Springer, Berlin (1997)"},{"key":"216_CR17","first-page":"223","volume-title":"CAV. Lecture Notes in Computer Science, vol. 2725","author":"B. Boigelot","year":"2003","unstructured":"Boigelot B., Legay A., Wolper P.: Iterating transducers in the large (extended abstract). In: Warren, A.H., Somenzi, F. (eds.) CAV. Lecture Notes in Computer Science, vol. 2725, pp. 223\u2013235. Springer, Berlin (2003)"},{"key":"216_CR18","first-page":"561","volume-title":"TACAS. Lecture Notes in Computer Science, vol. 2988","author":"B. Boigelot","year":"2004","unstructured":"Boigelot B., Legay A., Wolper P.: Omega-regular model checking. In: Jensen, K., Podelski, A. (eds.) TACAS. Lecture Notes in Computer Science, vol. 2988, pp. 561\u2013575. Springer, Berlin (2004)"},{"key":"216_CR19","first-page":"55","volume-title":"CAV. Lecture Notes in Computer Science, vol. 818","author":"B. Boigelot","year":"1994","unstructured":"Boigelot B., Wolper P.: Symbolic verification with periodic sets. In: Dill, D.L. (ed.) CAV. Lecture Notes in Computer Science, vol. 818, pp. 55\u201367. Springer, Berlin (1994)"},{"key":"216_CR20","first-page":"135","volume-title":"CONCUR. Lecture Notes in Computer Science, vol. 1243","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani A., Esparza J., Maler O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A.W., Winkowski, J. (eds.) CONCUR. Lecture Notes in Computer Science, vol. 1243, pp. 135\u2013150. Springer, Berlin (1997)"},{"key":"216_CR21","first-page":"560","volume-title":"ICALP. Lecture Notes in Computer Science, vol. 1256","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani A., Habermehl P.: Symbolic reachability analysis of fifo channel systems with nonregular sets of configurations (extended abstract). In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP. Lecture Notes in Computer Science, vol. 1256, pp. 560\u2013570. Springer, Berlin (1997)"},{"key":"216_CR22","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking of complex dynamic data structures. In: Yi, K. (ed.), SAS. Lecture Notes in Computer Science, vol. 4134, pp. 52\u201370. Springer (2006)","DOI":"10.1007\/11823230_5"},{"key":"216_CR23","first-page":"372","volume-title":"CAV. Lecture Notes in Computer Science, vol. 3114","author":"A. Bouajjani","year":"2004","unstructured":"Bouajjani A., Habermehl P., Vojnar T.: Abstract regular model checking. In: Alur, R., Peled, D. (eds.) CAV. Lecture Notes in Computer Science, vol. 3114, pp. 372\u2013386. Springer, Berlin (2004)"},{"key":"216_CR24","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.), Computer Aided Verification, Proceedings of the 12th International Conference, CAV 2000, Chicago, IL, USA, July 15\u201319, 2000. Lecture Notes in Computer Science, vol. 1855, pp. 403\u2013418, Springer, Berlin (2000)","DOI":"10.1007\/10722167_31"},{"key":"216_CR25","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Rogalewicz, A., Habermehl, P., Vojnar, T.: Abstract regular (tree) model checking, 2012. In this volume","DOI":"10.1007\/s10009-011-0205-y"},{"key":"216_CR26","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Touili, T.: Extrapolating tree transformations. In: Brinksma, E., Larsen, K.G. (eds.), Computer Aided Verification, Proceedings of the 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27\u201331, 2002. Lecture Notes in Computer Science, vol. 2404, pp. 539\u2013554. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_46"},{"key":"216_CR27","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Touili, Tayssir.: Widening techniques for regular tree model checking, 2012. In this volume","DOI":"10.1007\/s10009-011-0208-8"},{"key":"216_CR28","doi-asserted-by":"crossref","unstructured":"Brinksma, E., Larsen, K.G. (eds.): Computer Aided Verification, Proceedings of the 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27\u201331, 2002. Lecture Notes in Computer Science, vol. 2404. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0"},{"issue":"2","key":"216_CR29","doi-asserted-by":"crossref","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., Hwang L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"216_CR30","first-page":"123","volume-title":"CONCUR. Lecture Notes in Computer Science, vol. 630","author":"Olaf. Burkart","year":"1992","unstructured":"Burkart Olaf., Steffen Bernhard.: Model checking for context-free processes. In: Cleaveland, R. (ed.) CONCUR. Lecture Notes in Computer Science, vol. 630, pp. 123\u2013137. Springer, Berlin (1992)"},{"key":"216_CR31","first-page":"98","volume-title":"CONCUR. Lecture Notes in Computer Science, vol. 836","author":"O. Burkart","year":"1994","unstructured":"Burkart O., Steffen B.: Pushdown processes: parallel composition and model checking. In: Jonsson, B., Parrow, J. (eds.) CONCUR. Lecture Notes in Computer Science, vol. 836, pp. 98\u2013113. Springer, Berlin (1994)"},{"issue":"1","key":"216_CR32","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 106(1), 61\u201386 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"216_CR33","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke E.M., Biere A., Raimi R., Zhu Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"216_CR34","first-page":"52","volume-title":"Logic of Programs. Lecture Notes in Computer Science, vol. 131","author":"E.M. Clarke","year":"1981","unstructured":"Clarke E.M., Emerson E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs. Lecture Notes in Computer Science, vol. 131, pp. 52\u201371. Springer, Berlin (1981)"},{"issue":"3","key":"216_CR35","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/s100090050030","volume":"2","author":"R. Cleaveland","year":"1999","unstructured":"Cleaveland R.: Pragmatics of model checking: an sttt special section. STTT 2(3), 208\u2013218 (1999)","journal-title":"STTT"},{"key":"216_CR36","first-page":"286","volume-title":"CAV. Lecture Notes in Computer Science, vol. 2102","author":"D. Dams","year":"2001","unstructured":"Dams D., Lakhnech Y., Steffen M.: Iterating transducers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV. Lecture Notes in Computer Science, vol. 2102, pp. 286\u2013297. Springer, Berlin (2001)"},{"key":"216_CR37","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Rezine, A.: A lightweight regular model checking approach for parameterized systems, 2012. In this volume","DOI":"10.1007\/s10009-011-0213-y"},{"issue":"1","key":"216_CR38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-5(1:5)2009","volume":"5","author":"L. Doyen","year":"2009","unstructured":"Doyen L., Raskin J.-F.: Antichains for the automata-based approach to model-checking. Log. Methods Comput. Sci. 5(1), 1\u201320 (2009)","journal-title":"Log. Methods Comput. Sci."},{"key":"216_CR39","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Sistla, A.P. (eds.): Computer Aided Verification, Proceedings of the 12th International Conference, CAV 2000, Chicago, IL, USA, July 15\u201319, 2000. Lecture Notes in Computer Science, vol. 1855. Springer, Berlin (2000)","DOI":"10.1007\/10722167"},{"key":"216_CR40","doi-asserted-by":"crossref","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.), Computer Aided Verification, Proceedings of the 12th International Conference, CAV 2000, Chicago, IL, USA, July 15\u201319, 2000. Lecture Notes in Computer Science, vol. 1855. pp. 232\u2013247. Springer, Berlin (2000)","DOI":"10.1007\/10722167_20"},{"key":"216_CR41","doi-asserted-by":"crossref","unstructured":"Graf, S., Schwartzbach, M.I. (eds.): Tools and algorithms for construction and analysis of systems, Proceedings of the 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25\u2013April 2, 2000. Lecture Notes in Computer Science, vol. 1785, Springer, Berlin (2000)","DOI":"10.1007\/3-540-46419-0"},{"key":"216_CR42","doi-asserted-by":"crossref","unstructured":"Hu, A.J., Vardi, M.Y. (eds.): Computer Aided Verification, Proceedings of the 10th International Conference, CAV \u201998, Vancouver, BC, Canada, June 28\u2013July 2, 1998. Lecture Notes in Computer Science, vol. 1427, Springer, Berlin (1998)","DOI":"10.1007\/BFb0028725"},{"key":"216_CR43","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Graf, S., Schwartzbach, M.I. (eds.), Tools and algorithms for construction and analysis of systems, Proceedings of the 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25\u2013April 2, 2000. Lecture Notes in Computer Science, vol. 1785, pp. 220\u2013234. Springer, Berlin (2000)"},{"issue":"1\u20132","key":"216_CR44","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 256(1\u20132), 93\u2013112 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"216_CR45","doi-asserted-by":"crossref","first-page":"571","DOI":"10.1142\/S012905410200128X","volume":"13","author":"N. Klarlund","year":"2002","unstructured":"Klarlund N., M\u00f8ller A., Schwartzbach M.I.: Mona implementation secrets. Int. J. Found. Comput. Sci. 13(4), 571\u2013586 (2002)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"216_CR46","doi-asserted-by":"crossref","unstructured":"Legay, A.: Extrapolating (omega-)regular model checking, 2012. In this volume","DOI":"10.1007\/s10009-011-0209-7"},{"key":"216_CR47","first-page":"337","volume-title":"Symposium on Programming. Lecture Notes in Computer Science, vol. 137","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.) Symposium on Programming. Lecture Notes in Computer Science, vol. 137, pp. 337\u2013351. Springer, Berlin (1982)"},{"issue":"4","key":"216_CR48","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1016\/S1571-0661(04)00187-2","volume":"50","author":"T. Touili","year":"2001","unstructured":"Touili T.: Regular model checking using widening techniques. Electr. Notes Theor. Comput. Sci. 50(4), 342\u2013356 (2001)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"216_CR49","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Hu, A.J., Vardi, M.Y. (eds.), Computer Aided Verification, Proceedings of the 10th International Conference, CAV \u201998, Vancouver, BC, Canada, June 28\u2013July 2, 1998. Lecture Notes in Computer Science, vol. 1427, pp. 88\u201397. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028736"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0216-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0216-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0216-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,15]],"date-time":"2025-03-15T00:35:26Z","timestamp":1741998926000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0216-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12,7]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["216"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0216-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12,7]]}}}