{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:41:16Z","timestamp":1778298076153,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540600459","type":"print"},{"value":"9783540494133","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_39","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:37:11Z","timestamp":1330259831000},"page":"42-53","source":"Crossref","is-referenced-by-count":6,"title":["Verifying safety properties of a class of infinite-state distributed algorithms"],"prefix":"10.1007","author":[{"given":"Bengt","family":"Jonsson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Kempe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In Proc. 8 th IEEE Int. Symp. on Logic in Computer Science, 1993. Accepted for Publication in Information and Computation.","DOI":"10.1109\/LICS.1993.287591"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla and B. Jonsson. Undecidable verification problems for programs with unreliable channels. In Abiteboul and Shamir, editors, Proc. ICALP '94, volume 820 of Lecture Notes in Computer Science, pages 316\u2013327. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58201-0_78"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5 th IEEE Int. Symp. on Logic in Computer Science, pages 414\u2013425, Philadelphia, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur, T. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. In Proc. 14 th IEEE Real-Time Systems Symposium, pages 2\u201311, 1993.","DOI":"10.1109\/REAL.1993.393520"},{"key":"5_CR5","unstructured":"M. Ben-Ari. Mathematical Logic for Computer Science. Prentice Hall, 1993."},{"key":"5_CR6","unstructured":"J. Blom, B. Jonsson, and L. Kempe. Using temporal logic for modular specification of telephone services. In Feature Interactions in Telecommunications Systems, Amsterdam, Holland, May 1994."},{"key":"5_CR7","unstructured":"T. Bowen, F. Dworack, C. Chow, N. Griffeth, G. Herman, and Y.-J. Lin. The feature interaction problem in telecommunications system. SETS, 1989."},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"O. Burkart and B. Steffen. Model checking for context-free processes. In Cleaveland, editor, Proc. CONCUR '92, Theories of Concurrency: Unification and Extension, number 630 in Lecture Notes in Computer Science, pages 123\u2013137. Springer Verlag, 1992.","DOI":"10.1007\/BFb0084787"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"S. Christensen, Y. Hirshfeld, and F. Moller. Bisimulation equivalence is decidable for basic parallel processes. In Proc. CONCUR '93, Theories of Concurrency: Unification and Extension, pages 143\u2013157, 1993.","DOI":"10.1007\/3-540-57208-2_11"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"S. Christensen, H. H\u00fcttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. In W. R. Cleaveland, editor, Proc. CONCUR '92, Theories of Concurrency: Unification and Extension, pages 138\u2013147, 1992.","DOI":"10.1007\/BFb0084788"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"E. M. Clarke and O. Grumberg. Avoiding the state explosion problem in temporal logic model checking algorithms. In Proc. 6 th ACM Symp. on Principles of Distributed Computing, Vancouver, Canada, pages 294\u2013303, 1987.","DOI":"10.1145\/41840.41865"},{"key":"5_CR12","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. Fischer","year":"1979","unstructured":"M. Fischer and R. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and Systems Sciences, 18:194\u2013211, 1979.","journal-title":"Journal of Computer and Systems Sciences"},{"issue":"3","key":"5_CR13","doi-asserted-by":"crossref","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.","journal-title":"Journal of the ACM"},{"key":"5_CR14","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0304-3975(90)90006-4","volume":"74","author":"P. Jan\u010dar","year":"1990","unstructured":"P. Jan\u010dar. Decidability of a temporal logic problem for petri nets. Theoretical Computer Science, 74:71\u201393, 1990.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"5_CR15","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1006\/inco.1993.1069","volume":"107","author":"B. Jonsson","year":"1993","unstructured":"B. Jonsson and J. Parrow. Deciding bisimulation equivalences for a class of nonfinite-state programs. Information and Computation, 107(2):272\u2013302, Dec. 1993.","journal-title":"Information and Computation"},{"key":"5_CR16","unstructured":"F. J. Lin and Y.-J. Lin. A building block approach to detecting and resolving feature interactions. In L. Bouma and H. Velthuijsen, editors, Feature Interactions in Telecommuniactions Systems, pages 86\u2013119. IOS Press, 1994."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Z. Shtadler and O. Grumberg. Network grammars, communication behaviours and automatic verification. In Sifakis, editor, Proc. Workshop on Computer Aided Verification, volume 407 of Lecture Notes in Computer Science, pages 151\u2013165. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52148-8_13"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"K. \u010cer\u0101ns. Decidability of bisimulation equivalence for parallel timer processes. In Proc. Workshop on Computer Aided Verification, volume 663 of Lecture Notes in Computer Science, pages 302\u2013315, 1992.","DOI":"10.1007\/3-540-56496-9_24"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing interesting properties of programs in propositional temporal logic (extended abstract). In Proc. 13 th ACM Symp. on Principles of Programming Languages, pages 184\u2013193, Jan. 1986.","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:28:48Z","timestamp":1605630528000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}