{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:42:33Z","timestamp":1746006153513,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602187"},{"type":"electronic","value":"9783540447382"}],"license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60218-6_25","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:51:21Z","timestamp":1330278681000},"page":"333-347","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Decidability of simulation and bisimulation between lossy channel systems and finite state systems"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Mats","family":"Kindahl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5th IEEE Int. Symp. on Logic in Computer Science, pages 414\u2013425, Philadelphia, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"25_CR2","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In Proc. 8th IEEE Int. Symp. on Logic in Computer Science, 1993. Accepted for Publication in Information and Computation."},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla and Bengt 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":"25_CR4","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1016\/0376-5075(78)90015-6","volume":"2","author":"G. V. Bochman","year":"1978","unstructured":"G. V. Bochman. Finite state description of communicating protocols. Computer Networks, 2:361\u2013371, 1978.","journal-title":"Computer Networks"},{"key":"25_CR5","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"},{"issue":"5","key":"25_CR6","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1145\/362946.362970","volume":"2","author":"K. Bartlett","year":"1969","unstructured":"K. Bartlett, R. Scantlebury, and P. Wilkinson. A note on reliable full-duplex transmissions over half duplex lines. Communications of the ACM, 2(5):260\u2013261, 1969.","journal-title":"Communications of the ACM"},{"issue":"5","key":"25_CR7","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"2","author":"D. Brand","year":"1983","unstructured":"D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 2(5):323\u2013342, April 1983.","journal-title":"Journal of the ACM"},{"key":"25_CR8","first-page":"302","volume":"663","author":"K. \u010cer\u0101ns","year":"1992","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.","journal-title":"Proc. Workshop on Computer Aided Verification"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"K. \u010cer\u0101ns. Deciding properties of integral relational automata. In Abiteboul and Shamir, editors, Proc. ICALP '94, volume 820 of Lecture Notes in Computer Science, pages 35\u201346. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58201-0_56"},{"key":"25_CR10","unstructured":"A. Choquet and A. Finkel. Simulation of linear FIFO nets having a structured set of terminal markings. In Proc. 8th European Workshop on Applications and Theory of Petri Nets, 1987."},{"key":"25_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. 6th ACM Symp. on Principles of Distributed Computing, Vancouver, Canada, pages 294\u2013303, 1987.","DOI":"10.1145\/41840.41865"},{"key":"25_CR12","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":"25_CR13","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":"25_CR14","first-page":"1","volume-title":"Protocol Specification, Testing, and Verification VIII","author":"A. Finkel","year":"1988","unstructured":"A. Finkel. A new class of analyzable CFSMs with unbounded FIFO channels. In Protocol Specification, Testing, and Verification VIII, pages 1\u201312, Atlantic City, USA, 1988. IFIP WG 6.1, North-Holland."},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"A. Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7(3), 1994.","DOI":"10.1007\/BF02277857"},{"issue":"3","key":"25_CR16","first-page":"209","volume":"6","author":"M.G. Gouda","year":"1987","unstructured":"M.G. Gouda, E.M. Gurari, T.-H. Lai, and L.E. Rosier. On deadlock detection in systems of communicating finite state machines. Computers and Artificial Intelligence, 6(3):209\u2013228, 1987.","journal-title":"Computers and Artificial Intelligence"},{"issue":"3","key":"25_CR17","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.","journal-title":"Journal of the ACM"},{"key":"25_CR18","volume-title":"Technical Report ISO 4335","author":"ISO","year":"1979","unstructured":"ISO. Data communications \u2014 HDLC procedures \u2014 elements of procedures. Technical Report ISO 4335, International Standards Organization, Geneva, Switzerland, 1979."},{"key":"25_CR19","doi-asserted-by":"publisher","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"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Bengt Jonsson and Lars Kempe. Verifying safety properties of a class of infinite-state distributed algorithms, 1995. To appear in: Proc. CAV '95.","DOI":"10.1007\/3-540-60045-0_39"},{"issue":"2","key":"25_CR21","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 non-finite-state programs. Information and Computation, 107(2):272\u2013302, Dec. 1993.","journal-title":"Information and Computation"},{"issue":"2","key":"25_CR22","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"R.M. Karp","year":"1969","unstructured":"R.M. Karp and R.E. Miller. Parallel program schemata. Journal of Computer and Systems Sciences, 3(2):147\u2013195, May 1969.","journal-title":"Journal of Computer and Systems Sciences"},{"key":"25_CR23","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, 1989."},{"issue":"3","key":"25_CR24","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1145\/117009.117015","volume":"13","author":"W. Peng","year":"1991","unstructured":"W. Peng and S. Purushothaman. Data flow analysis of communicating finite state machines. ACM Trans. on Programming Languages and Systems, 13(3):399\u2013442, July 1991.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"25_CR25","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(86)90110-6","volume":"44","author":"L.E. Rosier","year":"1986","unstructured":"L.E. Rosier and H-C. Yen. Boundedness, empty channel detection and synchronization for communicating finite automata. Theoretical Computer Science, 44:69\u2013105, 1986.","journal-title":"Theoretical Computer Science"},{"key":"25_CR26","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":"25_CR27","doi-asserted-by":"crossref","unstructured":"A.P. Sistla and L.D. Zuck. Automatic temporal verification of buffer systems. In Larsen and Skou, editors, Proc. Workshop on Computer Aided Verification, volume 575 of Lecture Notes in Computer Science. Springer Verlag, 1991.","DOI":"10.1007\/3-540-55179-4_7"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic (extended abstract). In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 184\u2013193, Jan. 1986.","DOI":"10.1145\/512644.512661"},{"key":"25_CR29","unstructured":"Wang Yi. CCS + Time = an interleaving model for real time systems. In Leach Albert, Monien, and Rodriguez Artalejo, editors, Proc. ICALP '91, volume 510 of Lecture Notes in Computer Science. Springer Verlag, 1991."}],"container-title":["Lecture Notes in Computer Science","CONCUR '95: Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60218-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:55:41Z","timestamp":1742597741000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60218-6_25"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602187","9783540447382"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-60218-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"3 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}