{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:43:16Z","timestamp":1746006196883,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030913830"},{"type":"electronic","value":"9783030913847"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91384-7_5","type":"book-chapter","created":{"date-parts":[[2021,12,2]],"date-time":"2021-12-02T13:03:12Z","timestamp":1638450192000},"page":"78-96","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Regular Model Checking: Evolution and Perspectives"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,1,1]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Arora, J., Atig, M.F., Krishna, S.N.: Verification of programs under the release-acquire semantics. In: McKinley, K.S., Fisher, K. (Eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, 22\u201326 June 2019, pp. 1117\u20131132. ACM (2019)","DOI":"10.1145\/3314221.3314649"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification, CAV 1998. LNCS, vol. 1427, pp. 305\u2013318. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028754","DOI":"10.1007\/BFb0028754"},{"key":"5_CR3","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings of the LICS 1996 $${11}^{th}$$ IEEE International Symposium on Logic in Computer Science, pp. 313\u2013321 (1996)"},{"key":"5_CR4","doi-asserted-by":"publisher","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.) Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007. LNCS, vol. 4424, pp. 721\u2013736. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_56","DOI":"10.1007\/978-3-540-71209-1_56"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification, CAV 2007. LNCS, vol. 4590, pp. 145\u2013157. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_17","DOI":"10.1007\/978-3-540-73368-3_17"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Deneux, J., Mahata, P.: Multi-clock timed networks. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14\u201317 July 2004, Turku, Finland, Proceedings, pp. 345\u2013354. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319629"},{"issue":"5","key":"5_CR7","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s10009-015-0406-x","volume":"18","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transfer 18(5), 495\u2013516 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0406-x","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Ben Henda, N., Delzanno, G., Rezine, A.: Handling parameterized systems with non-atomic global conditions. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) Verification, Model Checking, and Abstract Interpretation, VMCAI 2008. LNCS, vol. 4905, pp. 22\u201336. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78163-9_7","DOI":"10.1007\/978-3-540-78163-9_7"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Jonsson, B., Kindahl, M., Peled, D.: A general approach to partial order reductions in symbolic verification. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification, CAV 1998. LNCS, vol. 1427, pp. 379\u2013390. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028760","DOI":"10.1007\/BFb0028760"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Jonsson, B., Mahata, P., d\u2019Orso, J.: Regular tree model checking. In: Brinksma, Ed., Larsen, K.G. (eds.) Computer Aided Verification, CAV 2002. LNCS, vol. 2404, pp. 555\u2013568. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_47","DOI":"10.1007\/3-540-45657-0_47"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Regular model checking made simple and effcient*. In: Brim, L., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A., Jan\u010dar, P. (eds.) CONCUR 2002\u2014Concurrency Theory, CONCUR 2002. LNCS, vol. 2421, pp. 116\u2013131. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45694-5_9","DOI":"10.1007\/3-540-45694-5_9"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Algorithmic improvements in regular model checking. In: Hunt, W.A., Somenzi, F. (eds.) Computer Aided Verification, CAV 2003. LNCS, vol. 2725, pp. 236\u2013248. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_25","DOI":"10.1007\/978-3-540-45069-6_25"},{"key":"5_CR13","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS 1990), Philadelphia, Pennsylvania, USA, 4\u20137 June 1990, pp. 414\u2013425. IEEE Computer Society (1990)"},{"issue":"3","key":"5_CR14","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1023\/A:1008644009416","volume":"13","author":"DA Basin","year":"1998","unstructured":"Basin, D.A., Klarlund, N.: Automata based symbolic reasoning in hardware verification. Formal Methods Syst. Des. 13(3), 255\u2013288 (1998)","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification, CAV 1996. LNCS, vol. 1102, pp. 1\u201312. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_53","DOI":"10.1007\/3-540-61474-5_53"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs (extended abstract). In: Van Hentenryck, P. (ed.) Static Analysis, SAS 1997. LNCS, vol. 1302, pp. 172\u2013186. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0032741","DOI":"10.1007\/BFb0032741"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Boigelot, B., Wolper, P.: Symbolic verification with periodic sets. In: Dill, D.L. (ed.) Computer Aided Verification, CAV 1994. LNCS, vol. 818, pp. 55\u201367. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_43","DOI":"10.1007\/3-540-58179-0_43"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model checking. In: Proceedings of the International Conference on Concurrency Theory (CONCUR 1997). LNCS 1243 (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) Automata, Languages and Programming, ICALP 1997. LNCS, vol. 1256, pp. 560\u2013570. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63165-8_211","DOI":"10.1007\/3-540-63165-8_211"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, CAV 2000. LNCS, vol. 1855, pp. 403\u2013418. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_31","DOI":"10.1007\/10722167_31"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Symbolic model checking: $$10^{20}$$ states and beyond. Inf. Comput. 98, 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992, CONCUR 1992. LNCS, vol. 630, pp. 123\u2013137. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0084787","DOI":"10.1007\/BFb0084787"},{"issue":"1\u20132","key":"5_CR23","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0304-3975(99)00034-1","volume":"221","author":"O Burkart","year":"1999","unstructured":"Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. Theor. Comput. Sci. 221(1\u20132), 251\u2013270 (1999)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"5_CR24","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. Theoret. Comput. Sci. 106(1), 61\u201386 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"5_CR25","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM 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. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification, CAV 1998. LNCS, vol. 1427, pp. 268\u2013279. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028751","DOI":"10.1007\/BFb0028751"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification, vol. 2102. Lecture Notes in Computer Science (2001)","DOI":"10.1007\/3-540-44585-4_27"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification, CAV 2001. LNCS, vol. 2102, pp. 324\u2013336. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_30","DOI":"10.1007\/3-540-44585-4_30"},{"key":"5_CR29","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere. Tech. Rep. LSV-98-4, Ecole Normale Sup\u00e9rieure de Cachan (1998)"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems (extended abstract). In: Proceedings of the Infinity 1997, Electronic Notes in Theoretical Computer Science, Bologna, August 1997","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"5_CR31","doi-asserted-by":"crossref","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: Proceedings of the TACAS 1995, $${1}^{th}$$ International Confererence on Tools and Algorithms for the Construction and Analysis of Systems, vol. 1019, Lecture Notes in Computer Science (1996)","DOI":"10.1007\/3-540-60630-0_5"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Graf, S., Schwartzbach, M. (eds.) Proceedings of the TACAS 1900, $$6^{th}$$ International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 1785, Lecture Notes in Computer Science (2000)","DOI":"10.1007\/3-540-46419-0_16"},{"key":"5_CR33","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. Theoret. Comput. Sci. 256, 93\u2013112 (2001)","journal-title":"Theoret. Comput. Sci."},{"key":"5_CR34","doi-asserted-by":"publisher","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming, Programming 1982. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/3-540-11494-7_22","DOI":"10.1007\/3-540-11494-7_22"},{"key":"5_CR35","doi-asserted-by":"publisher","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification, CAV 1998. LNCS, vol. 1427, pp. 88\u201397. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028736","DOI":"10.1007\/BFb0028736"}],"container-title":["Lecture Notes in Computer Science","Model Checking, Synthesis, and Learning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91384-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T15:46:08Z","timestamp":1726242368000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91384-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030913830","9783030913847"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91384-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"1 January 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}