{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T10:56:29Z","timestamp":1790938589128,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540582014","type":"print"},{"value":"9783540485667","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58201-0_78","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:33:15Z","timestamp":1330270395000},"page":"316-327","source":"Crossref","is-referenced-by-count":15,"title":["Undecidable verification problems for programs with unreliable channels"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"key":"26_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":"26_CR2","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In Proc. 8th IEEE Int. Symp. on Logic in Computer Science, 1993.","DOI":"10.1109\/LICS.1993.287591"},{"key":"26_CR3","volume-title":"Technical Report 94\/47","author":"P. A. Abdulla","year":"1994","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Undecidable verification problems for programs with unreliable channels. Technical Report 94\/47, Dept. of Computer Systems, Uppsala University, Sweden, 1994."},{"key":"26_CR4","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 IEEE Int. Symp. on Logic in Computer Science, 1990."},{"issue":"5","key":"26_CR5","doi-asserted-by":"crossref","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":"26_CR6","doi-asserted-by":"crossref","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":"26_CR7","doi-asserted-by":"crossref","unstructured":"K. Cerans. 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"},{"issue":"2","key":"26_CR8","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"26_CR9","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":"26_CR10","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":"26_CR11","series-title":"IFIP WG 6.1","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":"26_CR12","unstructured":"A. Finkel. Decidability of the termination problem for completely specified protocols. Technical Report 463, LRI, University Paris-Sud, 1989. Also accepted for publication in the Distributed Computing Journal."},{"issue":"3","key":"26_CR13","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":"26_CR14","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":"26_CR15","unstructured":"G.J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"26_CR16","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":"26_CR17","doi-asserted-by":"crossref","unstructured":"B. Jonsson and J. Parrow. Deciding bisimulation equivalences for a class of non-finite-state programs. In Monien and Cori, editors, Proc. 6th Symposium on Theoretical Aspects of Computer Science, volume 349 of Lecture Notes in Computer Science, pages 421\u2013433. Springer Verlag, 1989. Revised version to appear in Information and Computation.","DOI":"10.1007\/BFb0029004"},{"issue":"2","key":"26_CR18","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":"26_CR19","unstructured":"J.K. Pachl. Protocol description and analysis based on a state transition model with channel expressions. In Protocol Specification, Testing, and Verification VII, May 1987."},{"issue":"3","key":"26_CR20","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":"26_CR21","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/BF00290732","volume":"19","author":"K. Ruohonen","year":"1983","unstructured":"K. Ruohonen. On some variants of Post's correspondence problem. Acta Informatica, (19):357\u2013367, 1983.","journal-title":"Acta Informatica"},{"key":"26_CR22","doi-asserted-by":"crossref","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":"26_CR23","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":"26_CR24","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":"26_CR25","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st IEEE Int. Symp. on Logic in Computer Science, pages 332\u2013344, June 1986."},{"key":"26_CR26","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":"26_CR27","doi-asserted-by":"crossref","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.","DOI":"10.1007\/3-540-54233-7_136"}],"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-58201-0_78.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:18:30Z","timestamp":1605647910000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58201-0_78"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540582014","9783540485667"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-58201-0_78","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}