{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,25]],"date-time":"2026-09-25T01:08:58Z","timestamp":1790298538752,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540646082","type":"print"},{"value":"9783540693390","type":"electronic"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"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":[[1998]]},"DOI":"10.1007\/bfb0028754","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"305-318","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":68,"title":["On-the-fly analysis of systems with unbounded, lossy FIFO channels"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","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,6,18]]},"reference":[{"issue":"1","key":"29_CR1","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1006\/inco.1996.0083","volume":"130","author":"P. A. Abdulla","year":"1996","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Undecidable verification problems for programs with unreliable channels. Inform. and Comput., 130(1):71\u201390, 1996.","journal-title":"Inform. and Comput."},{"issue":"2","key":"29_CR2","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. Inform. and Comput., 127(2):91\u2013101, 1996.","journal-title":"Inform. and Comput."},{"key":"29_CR3","unstructured":"B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In CAV'96, LNCS 1102."},{"key":"29_CR4","unstructured":"B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. Available at http:\/\/www.montefiore.ulg.ac.be\/~biogelot\/research\/BGWW97.ps."},{"key":"29_CR5","unstructured":"B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In SAS'97, LNCS 1997."},{"key":"29_CR6","unstructured":"A. Bouajjani and P. Habermehl. Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations. http:\/\/www.imag.fr\/VERIMAG\/PEOPLE\/Peter.Habermehl."},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"A. Bouajjani and P. Habermehl. Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations. In ICALP '97, LNCS 1256. 1997.","DOI":"10.1007\/3-540-63165-8_211"},{"key":"29_CR8","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":"29_CR9","doi-asserted-by":"crossref","unstructured":"B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In CAV'94, LNCS 818. 1994.","DOI":"10.1007\/3-540-58179-0_43"},{"issue":"5","key":"29_CR10","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":"29_CR11","unstructured":"A. Choquet and A. Finkel. Simulation of linear FIFO nets having a structured set of terminal markings. In Proc. 8\nth\nEuropean Workshop on Applications and Theory of Petri Nets, 1987."},{"issue":"1","key":"29_CR12","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1006\/inco.1996.0003","volume":"124","author":"G. C\u00e9\u00e9","year":"1996","unstructured":"G\u00e9rard C\u00e9\u00e9, Alain Finkel, and S. Purushothaman Iyer. Unreliable channels are easier to verify than perfect channels. Inform. and Comput., 124(1):20\u201331, 10 January 1996.","journal-title":"Inform. and Comput."},{"key":"29_CR13","unstructured":"C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In CAV'90."},{"key":"29_CR14","unstructured":"A. Finkel and O. Marc\u00e9. Verification of infinite regular communicating automata. Technical report, LIFAC, ENS de Cachan, 1996. Tech. Rep."},{"issue":"3","key":"29_CR15","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"},{"key":"29_CR16","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"2","author":"G. Higman","year":"1952","unstructured":"G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc., 2:326\u2013336, 1952.","journal-title":"Proc. London Math. Soc."},{"key":"29_CR17","unstructured":"G.J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"29_CR18","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":"29_CR19","doi-asserted-by":"publisher","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":"29_CR20","unstructured":"A.P. Sistla and L.D. Zuck. Automatic temporal verification of buffer systems. In Larsen and Skou, editors, CAV'91, LNCS 575. 1991."},{"key":"29_CR21","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS'86, IEEE, 1986."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028754","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:00:26Z","timestamp":1558270826000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028754"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0028754","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"18 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}