{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:50Z","timestamp":1761597050557},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422877"},{"type":"electronic","value":"9783540482246"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-48224-5_3","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T02:29:04Z","timestamp":1193538544000},"page":"24-39","source":"Crossref","is-referenced-by-count":18,"title":["Languages, Rewriting Systems, and Verification of Infinite-State Systems"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"3_CR1","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u201999","author":"P. Abdulla","year":"1999","unstructured":"P. Abdulla, A. Annichini, and A. Bouajjani. Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol. In TACAS\u201999. LNCS 1579, 1999."},{"key":"3_CR2","series-title":"Lect Notes Comput Sci","volume-title":"ICALP\u201901","author":"P. Abdulla","year":"2001","unstructured":"P. Abdulla, L. Boasson, and A. Bouajjani. Effective Lossy Queue Languages. In ICALP\u201901. LNCS, Springer-Verlag, 2001."},{"key":"3_CR3","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201998","author":"P. Abdulla","year":"1998","unstructured":"P. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In CAV\u201998. LNCS 1427, 1998."},{"key":"3_CR4","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201999","author":"P. Abdulla","year":"1999","unstructured":"P. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling Global Conditions in Parametrized System Verification. In CAV\u201999. LNCS 1633, 1999."},{"key":"3_CR5","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201901","author":"A. Annichini","year":"2001","unstructured":"A. Annichini, A. Bouajjani, and M. Sighireanu. TReX: A Tool for Reachability Analysis of Complex Systems. In CAV\u201901. LNCS, Springer-Verlag, 2001."},{"key":"3_CR6","unstructured":"P. Abdulla, K. \u010cer\u0101ns, B. Jonsson, and Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In LICS\u201996. IEEE, 1996."},{"key":"3_CR7","series-title":"Lect Notes Comput Sci","volume-title":"CONCUR\u201997","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Push-down Automata: Application to Model Checking. In CONCUR\u201997. LNCS 1243, 1997."},{"key":"3_CR8","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201996","author":"B. Boigelot","year":"1996","unstructured":"B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In CAV\u201996. LNCS 1102, 1996."},{"key":"3_CR9","series-title":"Lect Notes Comput Sci","volume-title":"SAS\u201997","author":"B. Boigelot","year":"1997","unstructured":"B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In SAS\u201997. LNCS 1302, 1997."},{"key":"3_CR10","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 Nonregular Sets of Configurations. In ICALP\u201997. LNCS 1256, 1997. Full version in TCS 221 (1\/2), pp 221-250, 1999."},{"key":"3_CR11","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201900","author":"A. Bouajjani","year":"2000","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular Model Checking. In CAV\u201900. LNCS 1855, 2000."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, A. Muscholl, and T. Touili. Permutation Rewriting and Algorithmic Verification. In LICS\u201901. IEEE, 2001.","DOI":"10.1109\/LICS.2001.932515"},{"key":"3_CR13","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201994","author":"B. Boigelot","year":"1994","unstructured":"B. Boigelot and P. Wolper. Symbolic Verification with Periodic Sets. In CAV\u201994. LNCS 818, 1994."},{"issue":"1","key":"3_CR14","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/0304-3975(92)90278-N","volume":"106","author":"D. Caucal","year":"1992","unstructured":"D. Caucal. On the Regular Structure of Prefix Rewriting. TCS, 106(1):61\u201386, 1992.","journal-title":"TCS"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Static Determination of Dynamic Properties of Recursive Procedures. In IFIP Conf. on Formal Description of Programming Concepts. North-Holland Pub., 1977.","DOI":"10.1145\/390017.808314"},{"issue":"1","key":"3_CR16","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1006\/inco.1996.0003","volume":"124","author":"G. C\u00e9c\u00e9","year":"1996","unstructured":"G\u00e9rard C\u00e9c\u00e9, Alain Finkel, and S. Purushothaman Iyer. Unreliable Channels Are Easier to Verify Than Perfect Channels. Inform. and Comput., 124(1):20\u201331, 1996.","journal-title":"Inform. and Comput."},{"key":"3_CR17","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201901","author":"D. Dams","year":"2001","unstructured":"D. Dams, Y. Lakhnech, and M. Steffen. Iterating transducers. In CAV\u201901. LNCS, Springer-Verlag, 2001."},{"key":"3_CR18","series-title":"Lect Notes Comput Sci","volume-title":"FOSSACS\u201999","author":"J. Esparza","year":"1999","unstructured":"J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural dataflow analysis. In FOSSACS\u201999. LNCS 1578, 1999."},{"key":"3_CR19","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201901","author":"J. Esparza","year":"2001","unstructured":"J. Esparza and S. Schwoon. A BDD-based Model Checker for Recursive Programs. In CAV\u201901. LNCS, Springer-Verlag, 2001."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"L. Fribourg and H. Ols\u00e9n. Reachability sets of parametrized rings as regular languages. Electronic Notes in Theoretical Computer Science, 1997.","DOI":"10.1016\/S1571-0661(05)80427-X"},{"key":"3_CR21","series-title":"Lect Notes Comput Sci","volume-title":"CONCUR\u201900","author":"A. Finkel","year":"2000","unstructured":"A. Finkel, S. Purushothaman Iyer, and G. Sutre. Well-abstracted transition systems. In CONCUR\u201900. LNCS 1877, 2000."},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A Direct Symbolic Approach to Model Checking Pushdown Systems. In Infinity\u201997, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"3_CR23","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u201900","author":"B. Jonsson","year":"2000","unstructured":"B. Jonsson and M. Nilsson. Transitive Closures of Regular Relations for Verifying Infinite-State Systems. In TACAS\u201900. LNCS 1785, 2000."},{"key":"3_CR24","series-title":"Lect Notes Comput Sci","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. In CAV\u201997. LNCS 1254, 1997."},{"key":"3_CR25","unstructured":"D. Lugiez, and P. Schnoebelen. The regular viewpoint on PA-processes. In Theoretical Computer Science. to appear, 2001."},{"key":"3_CR26","unstructured":"R. Mayr. Decidability and Complexity of Model Checking Problems for Infinite State Systems. PhD Thesis, Technische Universitaet Muenchen, April 1998."},{"key":"3_CR27","series-title":"Lect Notes Comput Sci","volume-title":"LATIN\u201900","author":"R. Mayr","year":"2000","unstructured":"R. Mayr. Undecidable Problems in Unreliable Computations. In LATIN\u201900. LNCS 1776, 2000."},{"key":"3_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60915-6","volume-title":"CONCUR\u201996","author":"F. Moller","year":"1996","unstructured":"F. Moller. Infinite results. In CONCUR\u201996. LNCS 1119, 1996."},{"key":"3_CR29","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201900","author":"A. Pnueli","year":"2000","unstructured":"A. Pnueli and E. Shahar. Liveness and acceleration in parametrized verification. In CAV\u201900. LNCS 1855, 2000."},{"key":"3_CR30","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/BF02679467","volume":"30","author":"J.-E. Pin","year":"1997","unstructured":"J.-E. Pin and P. Weil. Polynomial closure and unambiguous product. Theory of Computing Systems, 30:383\u2013422, 1997.","journal-title":"Theory of Computing Systems"},{"key":"3_CR31","unstructured":"T. Touili. V\u00e9rification de R\u00e9seaux Param\u00e9tr\u00e9s Bas\u00e9e sur des Techniques de R\u00e9\u00e9criture. MSc. Thesis (French DEA) report, Liafa Lab., University of Paris 7, July 2000. http:\/\/verif.liafa.jussieu.fr\/~touili ."},{"key":"3_CR32","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201998","author":"P. Wolper","year":"1998","unstructured":"P. Wolper and B. Boigelot. Verifying systems with infinite but regular state spaces. In CAV\u201998. LNCS 1427, 1998."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48224-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:28:26Z","timestamp":1556922506000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48224-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422877","9783540482246"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-48224-5_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}