{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T03:56:09Z","timestamp":1768276569613,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540430025","type":"print"},{"value":"9783540452942","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45294-x_14","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T22:45:12Z","timestamp":1181601912000},"page":"156-170","source":"Crossref","is-referenced-by-count":13,"title":["Beyond Regular Model Checking"],"prefix":"10.1007","author":[{"given":"Dana","family":"Fisman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,11,26]]},"reference":[{"key":"14_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/BFb0028754","volume-title":"CAV\u201998","author":"P.A. Abdulla","year":"1998","unstructured":"P.A. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. CAV\u201998, LNCS, volume 1427, p. 305\u2013318. Springer-Verlag, 1998."},{"key":"14_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"CAV\u201999","author":"P.A. Abdulla","year":"1999","unstructured":"P.A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling global conditions in parametrized system verification. CAV\u201999, volume 1633 of LNCS, p. 134 Springer-Verlag, 1999."},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"K. R. Apt and D. Kozen. Limits for automatic program verification of finite-state concurrent systems. Information Processing Letters, 22(6), 1986.","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"14_CR4","unstructured":"J-P. Bodeveix and M. Filali. Experimenting acceleration methods for the validation of infinite state systems. In DSVV\u20192000, Taipei, Taiwan, April 2000."},{"key":"14_CR5","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"CAV\u201996","author":"B. Boigelot","year":"1996","unstructured":"B. Boigelot and P. Godefroid. Symbolic verification of coomunication protocols with infinite state spaces using QDDs. CAV\u201996, volume 1102 of LNCS, p. 1\u201312. Springer-Verlag, 1996."},{"key":"14_CR6","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":"14_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. CONCUR\u201997, LNCS, volume 1243, p. 135. Springer-Verlag, 1997."},{"key":"14_CR8","series-title":"Lect Notes Comput Sci","volume-title":"ICALP\u201997","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani and P. Habermehl. Symbolic reachability analysis of FIFO-channel systems with non-regular sets of configurations. In ICALP\u201997, volume 1256 of LNCS Springer-Verlag, 1997."},{"key":"14_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"CAV\u201900","author":"A. Bouajjani","year":"2000","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touilli. Regular model checking. CAV\u201900, volume 1855 of LNCS, p. 403\u2013418. Springer-Verlag, 2000."},{"key":"14_CR10","unstructured":"A. Bouajjani and O. Maler. Reachability analysis of push-down automata. In Workshop on Infinite-state Systems, Pisa, 1996."},{"issue":"2","key":"14_CR11","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, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, 1992.","journal-title":"Information and Computation"},{"issue":"2","key":"14_CR12","first-page":"89","volume":"2","author":"O. Burkat","year":"1995","unstructured":"O. Burkat and B. Steffen. Composition, decomposition and model checking of pushdown processes. Nordic Journal of Computing, 2(2):89\u2013125, 1995.","journal-title":"Nordic Journal of Computing"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. In CONCUR\u201995, p. 395\u2013407, Philadelphia, PA, August 1995.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"14_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/BFb0028751","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, p. 268\u2013279, 1998."},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL\u201997.","DOI":"10.1145\/512950.512973"},{"key":"14_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"CAV\u201900","author":"J. Esparza","year":"2000","unstructured":"J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. CAV\u201900, volume 1855 of LNCS, p. 232\u2013247. Springer-Verlag, 2000."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. In Proc. Infinity\u201997, Electronic Notes in Theoretical Computer Science, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"L. Fribourg and H. Olsen. Reachability sets of parametrized rings as regular languages. In Proc. Infinity\u201997, Electronic Notes in Theoretical Computer Science, volume 9, July 1997.","DOI":"10.1016\/S1571-0661(05)80427-X"},{"key":"14_CR19","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, Massachusetts, 1979."},{"key":"14_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Transitive closures of regular relations for verifying infinite-state systems","author":"B. Jonsson","year":"2000","unstructured":"B. Jonsson and M. Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In S. Graf, editor, Proceedings of TACAS\u201900, LNCS, 2000. To Appear."},{"key":"14_CR21","series-title":"Lect Notes Comput Sci","first-page":"424","volume-title":"CAV\u201997","author":"Y. Kesten","year":"1997","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. CAV\u201997, LNCS, p. 424\u2013435. Springer-Verlag, 1997."},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL\u201997, Paris, 1997.","DOI":"10.1145\/263699.263747"},{"issue":"3","key":"14_CR23","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G.L. Peterson","year":"1981","unstructured":"G.L. Peterson. Myths about the mutual exclusion problem. Info. Proc. Lett., 12(3):115, 1981.","journal-title":"Info. Proc. Lett."},{"key":"14_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/10722167_26","volume-title":"CAV\u201900","author":"A. Pnueli","year":"2000","unstructured":"A. Pnueli and E. Shahar. Liveness and acceleration in parameterized verification. CAV\u201900, volume 1855 of LNCS, p. 328\u2013343. Springer-Verlag, 2000."},{"issue":"1","key":"14_CR25","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/358527.358537","volume":"24","author":"G. Ricart","year":"1981","unstructured":"G. Ricart and A.K. Agrawala. An optimal algorithm for mutual exclusion in computer networks. Comm. ACM, 24(1):9\u201317, 1981. Corr. ibid. 1981, p.581.","journal-title":"Comm. ACM"},{"key":"14_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1007\/3-540-63165-8_221","volume-title":"The equivalence problem for deterministic pushdown automata is decidable","author":"G. Senizergues","year":"1997","unstructured":"G. Senizergues. The equivalence problem for deterministic pushdown automata is decidable. volume 1256 of LNCS, p. 671\u2013681, 1997."},{"key":"14_CR27","unstructured":"E. Shahar. The tlv system and its application. Master\u2019s thesis,Weizmann Institute, 1996."},{"key":"14_CR28","series-title":"Lect Notes Comput Sci","volume-title":"FODDACS\u201901","author":"C. Stirling","year":"2001","unstructured":"Colin Stirling. Decidability of dpda equivalence. FODDACS\u201901, LNCS Springer-Verlag, 2001."},{"key":"14_CR29","series-title":"Lect Notes Comput Sci","first-page":"55","volume-title":"CAV\u201994","author":"P. Wolper","year":"1994","unstructured":"P. Wolper and B. Boigelot. Symbolic verification with periodic sets. In D. Dill, editor, CAV\u201994, volume 818 of LNCS, p. 55\u201367. Springer-Verlag, 1994."},{"key":"14_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"CAV\u201998","author":"P. Wolper","year":"1998","unstructured":"Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. CAV\u201998, LNCS, volume 1427, p. 88\u201397. Springer-Verlag, 1998."}],"container-title":["Lecture Notes in Computer Science","FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45294-X_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T21:28:00Z","timestamp":1556486880000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45294-X_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430025","9783540452942"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-45294-x_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}