{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:45:44Z","timestamp":1762458344026,"version":"build-2065373602"},"reference-count":71,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":4070,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["The Journal of Logic and Algebraic Programming"],"published-print":{"date-parts":[[2002,7]]},"DOI":"10.1016\/s1567-8326(02)00025-5","type":"journal-article","created":{"date-parts":[[2002,10,8]],"date-time":"2002-10-08T16:46:42Z","timestamp":1034095602000},"page":"109-127","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":12,"special_numbering":"C","title":["Iterating transducers"],"prefix":"10.1016","volume":"52-53","author":[{"given":"Dennis","family":"Dams","sequence":"first","affiliation":[]},{"given":"Yassine","family":"Lakhnech","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Steffen","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1567-8326(02)00025-5_BIB1","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, A. Bouajjani, B. Jonsson, On-the-fly analysis of systems with unbounded lossy Fifo-channels, in: Ref. [45], pp. 305\u2013318","DOI":"10.1007\/BFb0028754"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB2","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, A. Bouajjani, B. Jonsson, M. Nilsson, Handling global conditions in parameterized system verification, in: Ref. [43], pp. 134\u2013145","DOI":"10.1007\/3-540-48683-6_14"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB3","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, P. Mahata, J. d\u2019Orso, Regular tree model checking, in: Proc. 14th Int. Conf. on Computer-aided Verification, 2002, to appear","DOI":"10.1007\/3-540-45657-0_47"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB4","unstructured":"ACM, 27th Annual Symposium on Principles of Programming Languages (POPL) Boston, MA, January 2000"},{"volume":"vol. 1102","year":"1996","series-title":"Proceedings of the 8th International Conference on Computer-Aided Verification, CAV\u201996 New Brunswick, NJ","key":"10.1016\/S1567-8326(02)00025-5_BIB5"},{"volume":"vol. 431","year":"1990","series-title":"Trees in Algebra and Programming (CAAP\u201990)","key":"10.1016\/S1567-8326(02)00025-5_BIB6"},{"year":"1998","series-title":"Term Rewriting and All That","author":"Baader","key":"10.1016\/S1567-8326(02)00025-5_BIB7"},{"year":"1979","series-title":"Transductions and Context-Free Languages","author":"Berstel","key":"10.1016\/S1567-8326(02)00025-5_BIB8"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB9","unstructured":"B. Boigelot, Symbolic methods for exploring infinite state spaces, Ph.D. Thesis, Universit\u00e9 de Li\u00e8ge, 1998"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB10","doi-asserted-by":"crossref","unstructured":"B. Boigelot, P. Godefroid, Symbolic verification of communication protocols with infinite state spaces using QDDs, in: Ref. [5], pp. 1\u201312","DOI":"10.1007\/3-540-61474-5_53"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB11","unstructured":"B. Boigelot, P. Godefroid, B. Willems, P. Wolper, The power of QDDs, in: Ref. [68], pp. 172\u2013186"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB12","doi-asserted-by":"crossref","unstructured":"B. Boigelot, P. Wolper, Symbolic verification with periodic sets, in: Ref. [28], pp. 55\u201367","DOI":"10.1007\/3-540-58179-0_43"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB13","doi-asserted-by":"crossref","unstructured":"R. Book, F. Otto, String rewriting systems, in: Monographs in Computer Science, Springer, Berlin, 1993","DOI":"10.1007\/978-1-4613-9771-7"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB14","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, Languages, rewriting systems, and verification of infinite-state systems, in: Ref. [46], pp. 24\u201339","DOI":"10.1007\/3-540-48224-5_3"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB15","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, T. Touili, Regular model checking, in: Ref. [32], pp. 135\u2013145"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB16","unstructured":"A. Bouajjani, A. Muscholl, T. Touili, Permutation rewriting and algorithmic verification, in: Ref. [47]"},{"volume":"vol. 1450","year":"1998","series-title":"International Symposium on Mathmatical Foundations of Computer Science (MFCS)","key":"10.1016\/S1567-8326(02)00025-5_BIB17"},{"issue":"2","key":"10.1016\/S1567-8326(02)00025-5_BIB18","article-title":"Graph-based algorithms for boolean function manipulation","volume":"40","author":"Bryant","year":"1986","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"10.1016\/S1567-8326(02)00025-5_BIB19","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Inf. Comput."},{"key":"10.1016\/S1567-8326(02)00025-5_BIB20","doi-asserted-by":"crossref","unstructured":"O. Burkhart, Model checking rationally restricted right closures of recognizable graphs, in: Methods and Tools for the Verification of Infinite State Systems, Grenoble, 1997","DOI":"10.1016\/S1571-0661(05)80424-4"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB21","doi-asserted-by":"crossref","unstructured":"D. Caucal, On the regular structures of prefix rewriting, in: Ref. [6], pp. 87\u2013102","DOI":"10.1007\/3-540-52590-4_42"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB22","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1090\/S0002-9947-1936-1501858-0","article-title":"Some properties of conversion","volume":"39","author":"Church","year":"1936","journal-title":"Trans. Am. Math. Soc."},{"volume":"vol. 531","year":"1991","series-title":"Computer Aided Verification 1990","key":"10.1016\/S1567-8326(02)00025-5_BIB23"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB24","unstructured":"D. Dams, Y. Lakhnech, M. Steffen, Iterating transducers. Technical Report TR-ST-01-03, Lehrstuhl f\u00fcr Software-Technologie, Institut f\u00fcr Informatik und praktische Mathematik, Christian-Albrechts-Universit\u00e4t Kiel, January 2001. A preliminary version is available on-line at http:\/\/radon.ics.ele.tue.nl\/\u223cvires\/public\/results.htm (reports section)"},{"volume":"vol. 600","year":"1991","series-title":"Real-time: Theory in Practice (REX Workshop)","key":"10.1016\/S1567-8326(02)00025-5_BIB25"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB26","unstructured":"N. Dershowitz, J.-P. Jouannaud, Rewrite systems, in: Ref. [69], Also as research report 478, LRI pp. 244\u2013320"},{"volume":"vol. 104","year":"1981","series-title":"Fifth GI Conference on Theoretical Computer Science","key":"10.1016\/S1567-8326(02)00025-5_BIB27"},{"volume":"vol. 818","year":"1994","series-title":"Computer Aided Verification (Proc. of CAV\u201994)","key":"10.1016\/S1567-8326(02)00025-5_BIB28"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB29","unstructured":"M. Duflot, L. Fribourg, U. Nilsson, Unavoidable configurations of parametrized rings of processes, Research Report LSV-00-10, Laboratoire Sp\u00e9cification et V\u00e9rification, Ecole Normale Sup\u00e9rieure de Cachan, November 2000"},{"year":"1974","series-title":"Automata, Languages and Machines, vol. A","author":"Eilenberg","key":"10.1016\/S1567-8326(02)00025-5_BIB30"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB31","first-page":"47","article-title":"On relations defined by generalized finite automata","volume":"9","author":"Elgot","year":"1965","journal-title":"J. Res. Dev."},{"volume":"vol. 1855","year":"2000","series-title":"Proceedings of the 12th International Conference on Computer-Aided Verification CAV\u201900, Chicago IL","key":"10.1016\/S1567-8326(02)00025-5_BIB32"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB33","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Podelski, Efficient algorithms for pre\u2217 and post\u2217 on interprocedural parallel flow graphs, in: Ref. [4], pp. 1\u201311","DOI":"10.1145\/325694.325697"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB34","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/0167-6423(90)90071-K","article-title":"An implementation of an efficient algorithm for bisimulation equivalence","volume":"13","author":"Fernandez","year":"1989","journal-title":"Sci. Comput. Prog."},{"key":"10.1016\/S1567-8326(02)00025-5_BIB35","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, P. Wolper, A direct symbolic approach to model checking pushdown systems, in: Electronic Notes in Theoretical Computer Science, August 1997, Presented at Infinity \u201997","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB36","doi-asserted-by":"crossref","unstructured":"D. Fisman, A. Pnueli, Beyond regular model checking, in: Procedings of the 21th Conference on the Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, vol. 2245, Springer, Berlin, 2001, pp. 156\u2013170","DOI":"10.1007\/3-540-45294-X_14"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB37","doi-asserted-by":"crossref","unstructured":"L. Fribourg, H. Ols\u00e9n, Reachability sets of parametrized rings as regular languages, in: Electronic Notes in Theoretical Computer Science, vol. 9, 2000. Also published as part of the Proceedings of the 2nd International Workshop on Verification of Infinite State Systems (INFINITY\u201997), Bologna, Italy, July 1997","DOI":"10.1016\/S1571-0661(05)80427-X"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB38","first-page":"157","article-title":"Regular tree languages and rewrite systems","volume":"24","author":"Gilleron","year":"1995","journal-title":"Fund. Inf."},{"year":"1966","series-title":"The Mathematical Theory of Context-Free Languages","author":"Ginsburg","key":"10.1016\/S1567-8326(02)00025-5_BIB39"},{"volume":"vol. 1785","year":"2000","series-title":"Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000)","key":"10.1016\/S1567-8326(02)00025-5_BIB40"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB41","unstructured":"S. Graf, B. Steffen, Compositional minimization of finite state systems, in: Ref. [23]"},{"volume":"vol. 1254","year":"1997","series-title":"Proceedings of the 9th International Conference on Computer-Aided Verification CAV\u201997, Haifa. Israel","key":"10.1016\/S1567-8326(02)00025-5_BIB42"},{"volume":"vol. 1633","year":"1999","series-title":"CAV\u201999: Computer Aided Verification","key":"10.1016\/S1567-8326(02)00025-5_BIB43"},{"year":"1979","series-title":"Introduction to Automata Theory, Languages, and Computation","author":"Hopcroft","key":"10.1016\/S1567-8326(02)00025-5_BIB44"},{"volume":"vol. 1427","year":"1998","series-title":"Computer-Aided Verification, CAV\u201998, Proceedings of the 10th International Conference, Vancouver, BC, Canada","key":"10.1016\/S1567-8326(02)00025-5_BIB45"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB46","unstructured":"28th Colloquium on Automata, Languages and Programming (ICALP), Lecture Notes in Computer Science, vol. 2076, Springer, Berlin, July 2001"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB47","unstructured":"IEEE, Sixteenth Annual Symposium on Logic in Computer Science (LICS), Boston, MA, Computer Society Press, June 2001"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB48","unstructured":"B. Jonsson, M. Nilsson, Transitive closures of regular relations for verifying infinite-state systems, in: Ref. [40]"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB49","doi-asserted-by":"crossref","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar, Symbolic model checking with rich assertional languages, Theoret. Comput. Sci. 256 (2001) 93\u2013112 (a conference version appeared in [42])","DOI":"10.1016\/S0304-3975(00)00103-1"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB50","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebra","author":"Knuth","year":"1970"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB51","doi-asserted-by":"crossref","unstructured":"M. Latteux, D. Simplot, A. Terlutte, Iterated length-preserving rational transductions, in: Ref. [17], pp. 286\u2013295","DOI":"10.1007\/BFb0055778"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB52","doi-asserted-by":"crossref","unstructured":"D. Lugiez, P. Schnoebelen, The regular viewpoint on PA-processes, in: Ref. [65], A longer version appeared as INRIA Rapport de Recherche, No. 3403, April 1998, pp. 50\u201366","DOI":"10.1007\/BFb0055615"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB53","doi-asserted-by":"crossref","unstructured":"N. Lynch, F. Vaandrager, Forward and backward simulations for timed-based systems, in: Ref. [25], pp. 397\u2013446","DOI":"10.1007\/BFb0032002"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB54","doi-asserted-by":"crossref","unstructured":"V. Manca, C. Martin-V\u0131\u0301de, G. P\u0103un, Iterated GSM mappings: a collapsing hierarchy, TUCS Report 206, Turku Centre for Computer Science, 1998","DOI":"10.1007\/978-3-642-60207-8_16"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB55","unstructured":"K. L. McMillan, Symbolic model checking: an approach to the state space explosion problem, Ph.D. Thesis, Carnegie Mellon University, 1992"},{"issue":"5","key":"10.1016\/S1567-8326(02)00025-5_BIB56","doi-asserted-by":"crossref","first-page":"1045","DOI":"10.1002\/j.1538-7305.1955.tb03788.x","article-title":"A method for synthesizing sequential circuits","volume":"34","author":"Mealy","year":"1955","journal-title":"Bell System Tech. J."},{"year":"1989","series-title":"Communication and Concurrency","author":"Milner","key":"10.1016\/S1567-8326(02)00025-5_BIB57"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB58","first-page":"129","article-title":"Gedanken experiments on sequential machines","author":"Moore","year":"1956","journal-title":"Automat. Stud."},{"issue":"2","key":"10.1016\/S1567-8326(02)00025-5_BIB59","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","article-title":"On theories with a combinatorial definition of equivalence","volume":"43","author":"Newman","year":"1942","journal-title":"Ann. Math."},{"key":"10.1016\/S1567-8326(02)00025-5_BIB60","unstructured":"M. Nilsson, Regular model checking, Licenciate Thesis of Uppsala University, Department of Information Technology, 2000"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB61","doi-asserted-by":"crossref","first-page":"339","DOI":"10.5802\/aif.287","article-title":"Transductions des languages de Chomsky","volume":"18","author":"Nivat","year":"1968","journal-title":"Ann. de 1\u2019Inst. Fourier"},{"issue":"6","key":"10.1016\/S1567-8326(02)00025-5_BIB62","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1137\/0216062","article-title":"Three partition refinement algorithms","volume":"16","author":"Paige","year":"1987","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S1567-8326(02)00025-5_BIB63","doi-asserted-by":"crossref","unstructured":"D. Park, Concurrency and automata on infinite sequences, in: Ref. [27], pp. 167\u2013183","DOI":"10.1007\/BFb0017309"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB64","doi-asserted-by":"crossref","unstructured":"A. Pnueli, E. Shahar, Liveness and acceleration in parameterized verification, in: Ref. [32], pp. 328\u2013343","DOI":"10.1007\/10722167_26"},{"volume":"vol. 1466","year":"1998","series-title":"CONCUR\u201998: Concurrency Theory (9th International Conference, Nice, France)","key":"10.1016\/S1567-8326(02)00025-5_BIB65"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB66","first-page":"234","article-title":"Sur les relations rationelles entre mono\u0131\u0308des libres","author":"Sch\u00fctzenberger","year":"1976","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S1567-8326(02)00025-5_BIB67","doi-asserted-by":"crossref","unstructured":"T. Touili, Regular model checking using widening techniques, in: Proceedings on the Workshop on Verification of Parametrized Systems (VEPAS\u201901), Crete, Electronic Notes in Theoretical Computer Science, vol. 50, Elsevier, Amsterdam, 2001","DOI":"10.1016\/S1571-0661(04)00187-2"},{"volume":"vol. 1302","year":"1997","series-title":"Proceedings of the Fourth International Static Analysis Symposium (SAS\u201997, Paris, France)","key":"10.1016\/S1567-8326(02)00025-5_BIB68"},{"year":"1990","series-title":"Handbook of Theoretical Computer Science, vol. B, Formal Models and Semantics","key":"10.1016\/S1567-8326(02)00025-5_BIB69"},{"key":"10.1016\/S1567-8326(02)00025-5_BIB70","doi-asserted-by":"crossref","unstructured":"P. Wolper, B. Boigelot, Verifying systems with infinite but regular state spaces, in: Ref. [45], pp. 88\u201397","DOI":"10.1007\/BFb0028736"},{"issue":"1","key":"10.1016\/S1567-8326(02)00025-5_BIB71","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0019-9958(76)90074-7","article-title":"Iterated a-NGSM maps and \u0393 systems","volume":"32","author":"Wood","year":"1976","journal-title":"Inf. Control"}],"container-title":["The Journal of Logic and Algebraic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1567832602000255?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1567832602000255?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T18:34:41Z","timestamp":1761590081000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1567832602000255"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,7]]},"references-count":71,"alternative-id":["S1567832602000255"],"URL":"https:\/\/doi.org\/10.1016\/s1567-8326(02)00025-5","relation":{},"ISSN":["1567-8326"],"issn-type":[{"type":"print","value":"1567-8326"}],"subject":[],"published":{"date-parts":[[2002,7]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Iterating transducers","name":"articletitle","label":"Article Title"},{"value":"The Journal of Logic and Algebraic Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1567-8326(02)00025-5","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Elsevier Science Inc. All rights reserved.","name":"copyright","label":"Copyright"}]}}