{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214731,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540424970"},{"type":"electronic","value":"9783540446859"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44685-0_1","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:16:21Z","timestamp":1186740981000},"page":"1-15","source":"Crossref","is-referenced-by-count":6,"title":["Channel Representations in Protocol Verification"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,8,22]]},"reference":[{"key":"1_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Proc. TACAS\u2019 99","author":"P. A. Abdulla","year":"1999","unstructured":"Parosh Aziz Abdulla, Aurore Annichini, and Ahmed Bouajjani. Algorithmic verification of lossy channel systems: An application to the bounded retransmission protocol. In Proc. TACAS\u2019 99, volume 1579 of LNCS, 1999."},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Luc Boasson, and Ahmed Bouajjani. Effective lossy queue languages, 2001. To appear in Proc. ICALP\u2019 2001: 28th International Colloquium on Automata, Lnaguages, and Programming.","DOI":"10.1007\/3-540-48224-5_53"},{"key":"1_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/BFb0028754","volume-title":"Proc. 10thInt. Conf. on Computer Aided Verification","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 Int. Conf. on Computer Aided Verification, volume 1427 of LNCS, pages 305\u2013318, 1998."},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Karlis Cer\u21ads, Bengt Jonsson, and Tsay Yih-Kuen. General decidability theorems for infinite-state systems. In Proc. LICS\u2019 96 11 th IEEE Int. Symp. on Logic in Computer Science, pages 313\u2013321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"issue":"2","key":"1_CR5","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.","journal-title":"Information and Computation"},{"key":"1_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/BFb0054179","volume-title":"Proc. TACAS\u2019 98","author":"P. A. Abdulla","year":"1998","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Verifying networks of timed processes. In Bernhard Steffen, editor, Proc. TACAS\u2019 98, volume 1384 of LNCS, pages 298\u2013312, 1998."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla and Aletta Nyl\u2019en. Timed Petri nets and BQOs, 2001. To appear in Proc. ICATPN\u20192001: 22nd Int. Conf. on application and theory of Petri nets.","DOI":"10.1007\/3-540-45740-2_5"},{"issue":"8","key":"1_CR8","doi-asserted-by":"crossref","first-page":"827","DOI":"10.1109\/TSE.1986.6312985","volume":"SE-12","author":"T.P. Blumer","year":"1986","unstructured":"T.P. Blumer and D.P. Sidhu. Mechanical verification of communication protocols. IEEE Trans. on Software Engineering, SE-12(8):827\u2013843, Aug. 1986.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"1_CR9","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proc. 8th Int. Conf. on Computer Aided Verification","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. 8 th Int. Conf. on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 1\u201312. Springer Verlag, 1996."},{"key":"1_CR10","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."},{"key":"1_CR11","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 fifo-channel systems with nonregular sets of configurations. In Proc. ICALP\u2019 97, volume 1256 of Lecture Notes in Computer Science, 1997."},{"issue":"5","key":"1_CR12","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":"1_CR13","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. LICS\u2019 90, 5 th IEEE Int. Symp. on Logic in Computer Science, 1990."},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"G\u2019erard C\u2019ec\u2019e, Alain Finkel, and S. Purushothaman Iyer. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(1):20\u201331, 10 January 1996.","DOI":"10.1006\/inco.1996.0003"},{"key":"1_CR15","unstructured":"A. Choquet and A. Finkel. Simulation of linear FIFO nets having a structured set of terminal markings. In Proc. 8 th European Workshop on Applications and Theory of Petri Nets, 1987."},{"issue":"2","key":"1_CR16","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":"1_CR17","doi-asserted-by":"crossref","unstructured":"G. Delzanno, J. Esparza, and A. Podelski. Constraint-based analysis of broadcast protocols. In Proc. CSL\u201999, 1999.","DOI":"10.1007\/3-540-48168-0_5"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and K.S. Namjoshi. On model checking for non-deterministic infinite-state systems. In Proc. LICS\u2019 98 13 th IEEE Int. Symp. on Logic in Computer Science, pages 70\u201380, 1998.","DOI":"10.1109\/LICS.1998.705644"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In Proc. LICS\u2019 99 14 th IEEE Int. Symp. on Logic in Computer Science, 1999.","DOI":"10.1109\/LICS.1999.782630"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/0890-5401(90)90009-7","volume":"89","author":"A. Finkel","year":"1990","unstructured":"A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89:144\u2013179, 1990.","journal-title":"Information and Computation"},{"key":"1_CR21","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"},{"key":"1_CR22","unstructured":"A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere. Technical Report LSV-98-4, Ecole Normale Sup\u2019erieure de Cachan, April 1998."},{"issue":"6","key":"1_CR23","doi-asserted-by":"crossref","first-page":"846","DOI":"10.1109\/TSE.1984.5010313","volume":"SE-10","author":"M. Gouda","year":"1984","unstructured":"M. Gouda. Closed covers: to verify progress for communicating finite state machines. IEEE Trans. on Software Engineering, SE-10(6):846\u2013855, Nov. 1984.","journal-title":"IEEE Trans. on Software Engineering"},{"issue":"3","key":"1_CR24","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":"5","key":"1_CR25","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, SE-23(5):279\u2013295, May 1997.","journal-title":"IEEE Trans. on Software Engineering"},{"issue":"2","key":"1_CR26","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":"1_CR27","doi-asserted-by":"crossref","unstructured":"K.G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Software Tools for Technology Transfer, 1(1\u20132), 1997.","DOI":"10.1007\/s100090050010"},{"key":"1_CR28","unstructured":"G. LeLann. Distributed systems-towards a formal approach. In B. Gilchrist, editor, IFIP77, pages 155\u2013160. North-Holland, 1977."},{"key":"1_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/10719839_37","volume-title":"Theoretical Informatics (LATIN\u20192000)","author":"R. Mayr","year":"2000","unstructured":"R. Mayr. Undecidable problems in unreliable computations. In Theoretical Informatics (LATIN\u20192000), number 1776 in Lecture Notes in Computer Science, 2000."},{"key":"1_CR30","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":"1_CR31","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":"1_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"5th International Symposium on Programming, Turin","author":"J.P. Queille","year":"1982","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in cesar. In 5th International Symposium on Programming, Turin, volume 137 of LNCS, pages 337\u2013352. Springer Verlag, 1982."},{"key":"1_CR33","unstructured":"H. Rudin, West, and P. Zafiropulo. Automated protocol validation-one chain of development. In Proc. Computer Network Protocols Symposium Liege, 1978."},{"key":"1_CR34","series-title":"Lect Notes Comput Sci","volume-title":"Proc. Workshop on Computer Aided Verification","author":"A.P. Sistla","year":"1991","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 LNCS. Springer Verlag, 1991."},{"key":"1_CR35","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. LICS\u2019 86, 1st IEEE Int. Symp. on Logic in Computer Science, pages 332\u2013344, June 1986."},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"C.H. West. Automated validation of a communications protocol: the ccitt x.21 recommendation. IBM Journal on Research and Development, 22(1), Jan. 1978.","DOI":"10.1147\/rd.221.0060"},{"key":"1_CR37","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":"1_CR38","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Proc. 10th Int. Conf. on Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. In Proc. 10th Int. Conf. on Computer Aided Verification, volume 1427 of LNCS, pages 88\u201397, Vancouver, July 1998. Springer Verlag."}],"container-title":["Lecture Notes in Computer Science","CONCUR 2001 \u2014 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44685-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T07:25:02Z","timestamp":1737357902000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44685-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540424970","9783540446859"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-44685-0_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}