{"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":1781172313018,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540672821","type":"print"},{"value":"9783540464198","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_16","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T23:17:25Z","timestamp":1186615045000},"page":"220-235","source":"Crossref","is-referenced-by-count":46,"title":["Transitive Closures of Regular Relations for Verifying Infinite-State Systems"],"prefix":"10.1007","author":[{"given":"Bengt","family":"Jonsson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marcus","family":"Nilsson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"16_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/BFb0028754","volume-title":"Proc. 10th CAV","author":"P. A. Abdulla","year":"1998","unstructured":"Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson. On-the-fly analysis of systems with unbounded, lossy fifo channels. In Proc. 10th CAV, volume 1427 of LNCS, pages 305\u2013318, 1998. 223"},{"key":"16_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"Proc. 11th CAV","author":"P. A. Abdulla","year":"1999","unstructured":"Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, and Marcus Nilsson. Handling global conditions in parameterized system verification. In Proc. 11th CAV, volume 1633 of LNCS, pages 134\u2013145, 1999. 220, 222, 224, 226, 231, 233"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5th LICS, pages 414\u2013425, Philadelphia, 1990. 220","DOI":"10.1109\/LICS.1990.113766"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Karlis \u010cer\u0101ns, Bengt Jonsson, and Tsay Yih-Kuen. General decidability theorems for infinite-state systems. In Proc. 11th LICS, pages 313\u2013321, 1996. 222","DOI":"10.1109\/LICS.1996.561359"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"R. Alur and T. Henzinger. A really temporal logic. In Proc. 30th Annual Symp. Foundations of Computer Science, pages 164\u2013169, 1989. 220","DOI":"10.1109\/SFCS.1989.63473"},{"issue":"2","key":"16_CR6","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P. A. Abdulla","year":"1996","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91\u2013101, 1996. 220, 222, 232","journal-title":"Information and Computation"},{"key":"16_CR7","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th LICS, 1990. 220"},{"key":"16_CR8","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proc. 8th CAV","author":"B. Boigelot","year":"1996","unstructured":"B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In Alur and Henzinger, editors, Proc. 8th CAV, volume 1102 of Lecture Notes in Computer Science, pages 1\u201312. Springer Verlag, 1996. 223, 229, 230, 233"},{"key":"16_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the Fourth International Static Analysis Symposium","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. 223, 229"},{"key":"16_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Proc. ICALP\u2019 97","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani and P. Habermehl. Symbolic reachability analysis of fifochannel systems with nonregular sets of configurations. In Proc. ICALP\u2019 97, volume 1256 of Lecture Notes in Computer Science, 1997. 223"},{"issue":"8","key":"16_CR11","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35(8):677\u2013691, Aug. 1986. 231","journal-title":"IEEE Trans. on Computers"},{"issue":"2","key":"16_CR12","first-page":"89","volume":"2","author":"O. Burkart","year":"1995","unstructured":"O. Burkart and B. Steffen. Composition, decomposition, and model checking of pushdown processes. Nordic Journal of Computing, 2(2):89\u2013125, 1995. 220","journal-title":"Nordic Journal of Computing"},{"key":"16_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"Proc. 6th CAV","author":"B. Boigelot","year":"1994","unstructured":"B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Proc. 6th CAV, volume 818 of LNCS, pages 55\u201367. Springer Verlag, 1994. 223"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM Symp. on Principles of Programming Languages, pages 238\u2013252, 1977. 223","DOI":"10.1145\/512950.512973"},{"issue":"5","key":"16_CR15","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0020-0190(83)90092-3","volume":"16","author":"E.W. Dijkstra","year":"1983","unstructured":"E.W. Dijkstra, W.H.J. Feijen, and A.J.M. van Gasteren. Derivation of a termination detection algorithm for distributed somputations. Information Processing Letters, 16(5):217\u2013219, 1983. 224, 232","journal-title":"Information Processing Letters"},{"issue":"3","key":"16_CR16","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/BF02277857","volume":"7","author":"A. Finkel","year":"1994","unstructured":"A. Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7(3), 1994. 220","journal-title":"Distributed Computing"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"L. Fribourg and H. Ols\u00e9n. Reachability sets of parametrized rings as regular languages. In Proc. 2nd Int. Workshop on Verification of Infinite State Systems (INFINITY\u201997), volume 9 of Electronical Notes in Theoretical Computer Science. Elsevier Science Publishers, July 1997. 222","DOI":"10.1016\/S1571-0661(05)80427-X"},{"issue":"3","key":"16_CR18","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S. M. German","year":"1992","unstructured":"S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675\u2013735, 1992. 220","journal-title":"Journal of the ACM"},{"key":"16_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Proc. TACAS\u2019 95, 1th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems","author":"J.G. Henriksen","year":"1996","unstructured":"J.G. Henriksen, J. Jensen, M. J\u00f8rgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Proc. TACAS\u2019 95, 1th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of LNCS, 1996. 222"},{"key":"16_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS\u2019 95","author":"J.G. Henriksen","year":"1996","unstructured":"J.G. Henriksen, J. Jensen, M. J\u00f8rgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS\u2019 95, LNCS 1019, 1996. Also available through http:\/\/www.brics.dk\/~klarlund\/Mona\/main.html . 231"},{"key":"16_CR21","unstructured":"N. Klarlund and A. M\u00f8ller. MONA Version 1.3 User Manual. BRICS Notes Series NS-98-3 (2.revision), Department of Computer Science, University of Aarhus, October 1998. 231"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In O. Grumberg, editor, Proc. 9th CAV, volume 1254, pages 424\u2013435, Haifa, Israel, 1997. Springer Verlag. 220, 221, 222, 226","DOI":"10.1007\/3-540-63166-6_41"},{"key":"16_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BFb0035388","volume-title":"Proc. of the Int. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201997), Enschede (NL)","author":"P. Kelb","year":"1997","unstructured":"P. Kelb, T. Margaria, M. Mendler, and C. Gsottberger. Mosel: A flexible toolset for monadic second-order logic. In Proc. of the Int. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201997), Enschede (NL), volume 1217 of LNCS, pages 183\u2013202, Heidelberg, Germany, March 1997. Springer-Verlag. 222"},{"key":"16_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1007\/3-540-63166-6_40","volume-title":"Proc. 9th CAV","author":"A. P. Sistla","year":"1997","unstructured":"A. Prasad Sistla. Parametrized verification of linear networks using automata as invariants. In O. Grumberg, editor, Proc. 9th CAV, volume 1254 of LNCS, pages 412\u2013423, Haifa, Israel, 1997. Springer Verlag. 222"},{"key":"16_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/3-540-61604-7_57","volume-title":"Proc. CONCUR\u2019 96, 7th Int. Conf. on Concurrency Theory","author":"C. Stirling","year":"1996","unstructured":"C. Stirling. Decidability of bisimulation equivalence for normed pushdown processes. In Proc. CONCUR\u2019 96, 7th Int. Conf. on Concurrency Theory, volume 1119 of LNCS, pages 217\u2013232. Springer Verlag, 1996. 220"},{"key":"16_CR26","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st LICS, pages 332\u2013344, June 1986. 226"},{"key":"16_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Proc. 10th CAV","author":"P. Wolper","year":"1998","unstructured":"Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. In Proc. 10th CAV, volume 1427 of LNCS, pages 88\u201397, Vancouver, July 1998. Springer Verlag. 222"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T05:59:58Z","timestamp":1737352798000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}