{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:59:02Z","timestamp":1773655142305,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642385919","type":"print"},{"value":"9783642385926","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38592-6_15","type":"book-chapter","created":{"date-parts":[[2013,5,29]],"date-time":"2013-05-29T04:56:11Z","timestamp":1369803371000},"page":"209-224","source":"Crossref","is-referenced-by-count":4,"title":["Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels"],"prefix":"10.1007","author":[{"given":"Jay","family":"Thakkar","sequence":"first","affiliation":[]},{"given":"Aditya","family":"Kanade","sequence":"additional","affiliation":[]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"http:\/\/www.tinyos.net\/tinyos-2.x\/doc\/html\/tep113.html"},{"key":"15_CR2","unstructured":"http:\/\/www.ietf.org\/rfc\/rfc793.txt"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-49059-0_15","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"P.A. Abdulla","year":"1999","unstructured":"Abdulla, P.A., Annichini, A., Bouajjani, A.: Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 208\u2013222. Springer, Heidelberg (1999)"},{"issue":"2","key":"15_CR4","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying Programs with Unreliable Channels. Inf. Comput.\u00a0127(2), 91\u2013101 (1996)","journal-title":"Inf. Comput."},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Cern\u00fd, P.: Expressiveness of streaming string transducers. In: FSTTCS, pp. 1\u201312 (2010)","DOI":"10.1007\/978-3-642-22012-8_1"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Cern\u00fd, P.: Streaming Transducers for Algorithmic Verification of Single-pass List-processing Programs. In: POPL, pp. 599\u2013610 (2011)","DOI":"10.1145\/1925844.1926454"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-22012-8_1","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"2011","unstructured":"Alur, R., Deshmukh, J.V.: Nondeterministic Streaming String Transducers. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol.\u00a06756, pp. 1\u201320. Springer, Heidelberg (2011)"},{"issue":"1","key":"15_CR8","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1109\/COMST.2002.5341329","volume":"4","author":"F. Babich","year":"2002","unstructured":"Babich, F., Deotto, L.: Formal Methods for Specification and Analysis of Communication Protocols. IEEE Comm. Surveys and Tutorials\u00a04(1), 2\u201320 (2002)","journal-title":"IEEE Comm. Surveys and Tutorials"},{"issue":"3","key":"15_CR9","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/s00165-005-0070-0","volume":"17","author":"B. Badban","year":"2005","unstructured":"Badban, B., Fokkink, W., Groote, J., Pang, J., Pol, J.: Verification of a Sliding Window Protocol in \u03bcCRL and PVS. Formal Asp. Comput.\u00a017(3), 342\u2013388 (2005)","journal-title":"Formal Asp. Comput."},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-39979-7_14","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2003","author":"J. Billington","year":"2003","unstructured":"Billington, J., Gallasch, G.E.: How Stop and Wait Protocols Can Fail over the Internet. In: K\u00f6nig, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol.\u00a02767, pp. 209\u2013223. Springer, Heidelberg (2003)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 403\u2013418. Springer, Heidelberg (2000)"},{"issue":"2","key":"15_CR12","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On Communicating Finite-State Machines. J. ACM\u00a030(2), 323\u2013342 (1983)","journal-title":"J. ACM"},{"issue":"9","key":"15_CR13","doi-asserted-by":"publisher","first-page":"1217","DOI":"10.1109\/TC.2011.147","volume":"61","author":"Y. Cao","year":"2012","unstructured":"Cao, Y.: Reliability of Mobile Processes with Noisy Channels. IEEE Trans. Computers\u00a061(9), 1217\u20131230 (2012)","journal-title":"IEEE Trans. Computers"},{"issue":"5","key":"15_CR14","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1109\/TCOM.1974.1092259","volume":"22","author":"V. Cerf","year":"1974","unstructured":"Cerf, V., Kahn, R.: A Protocol for Packet Network Intercommunication. IEEE Transactions on Communications\u00a022(5), 637\u2013648 (1974)","journal-title":"IEEE Transactions on Communications"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-36577-X_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Chkliaev","year":"2003","unstructured":"Chkliaev, D., Hooman, J., de Vink, E.P.: Verification and Improvement of the Sliding Window Protocol. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 113\u2013127. Springer, Heidelberg (2003)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-08342-1_11","volume-title":"Automata, Languages and Programming","author":"M. Chytil","year":"1977","unstructured":"Chytil, M., J\u00e1kl, V.: Serial composition of 2-way finite-state transducers and simple programs on strings. In: Salomaa, A., Steinby, M. (eds.) ICALP 1977. LNCS, vol.\u00a052, pp. 135\u2013147. Springer, Heidelberg (1977)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/BFb0035403","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.R. D\u2019Argenio","year":"1997","unstructured":"D\u2019Argenio, P.R., Katoen, J.P., Ruys, T.C., Tretmans, G.J.: The Bounded Retransmission Protocol must be on time! In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 416\u2013431. Springer, Heidelberg (1997)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-30793-5_15","volume-title":"Formal Techniques for Distributed Systems","author":"G. Delzanno","year":"2012","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: Verification of Ad Hoc Networks with Node and Communication Failures. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol.\u00a07273, pp. 235\u2013250. Springer, Heidelberg (2012)"},{"issue":"3","key":"15_CR19","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BF02277857","volume":"7","author":"A. Finkel","year":"1994","unstructured":"Finkel, A.: Decidability of the termination problem for completely specified protocols. Distrib. Comput.\u00a07(3), 129\u2013135 (1994)","journal-title":"Distrib. Comput."},{"key":"15_CR20","unstructured":"Forouzan, B.: Data Communications and Networking. McGraw-Hill Companies (2012)"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1007\/BFb0014338","volume-title":"Algebraic Methodology and Software Technology","author":"J. Groote","year":"1996","unstructured":"Groote, J., Pol, J.: A Bounded Retransmission Protocol for Large Data Packets. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol.\u00a01101, pp. 536\u2013550. Springer, Heidelberg (1996)"},{"issue":"3","key":"15_CR22","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1137\/0211035","volume":"11","author":"E. Gurari","year":"1982","unstructured":"Gurari, E.: The equivalence problem for deterministic two-way sequential transducers is decidable. SIAM J. Comput.\u00a011(3), 448\u2013452 (1982)","journal-title":"SIAM J. Comput."},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods","author":"K. Havelund","year":"1996","unstructured":"Havelund, K., Shankar, N.: Experiments in Theorem Proving and Model Checking for Protocol Verification. In: Gaudel, M.-C., Wing, J.M. (eds.) FME 1996. LNCS, vol.\u00a01051, pp. 662\u2013681. Springer, Heidelberg (1996)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-58085-9_75","volume-title":"Types for Proofs and Programs","author":"L. Helmink","year":"1994","unstructured":"Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-Checking a Data Link Protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806, pp. 127\u2013165. Springer, Heidelberg (1994)"},{"issue":"5","key":"15_CR25","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. Software Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"15_CR26","unstructured":"ISO. Data Communication - HDLC Procedures - Elements of Procedure. Technical Report ISO 4335, International Organization for Standardization (1979)"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/3-540-63166-6_41","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1997","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic Model Checking with Rich Assertional Languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 424\u2013435. Springer, Heidelberg (1997)"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Madelaine, E., Vergamini, D.: Specification and Verification of a Sliding Window Protocol in LOTOS. In: FORTE, pp. 495\u2013510 (1991)","DOI":"10.1016\/B978-0-444-89402-1.50045-X"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Peterson, W.W., Brown, D.T.: Cyclic Codes for Error Detection. In: IRE, pp. 228\u2013235 (1961)","DOI":"10.1109\/JRPROC.1961.287814"},{"key":"15_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2007)"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Rusu, V.: Verifying a Sliding Window Protocol using PVS. In: FORTE, pp. 251\u2013268 (2001)","DOI":"10.1007\/0-306-47003-9_16"},{"key":"15_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/3-540-55179-4_7","volume-title":"Computer Aided Verification","author":"A.P. Sistla","year":"1992","unstructured":"Sistla, A.P., Zuck, L.D.: Automatic Temporal Verification of Buffer Systems. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol.\u00a0575, pp. 59\u201369. Springer, Heidelberg (1992)"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"Smith, M.A., Klarlund, N.: Verification of a Sliding Window Protocol Using IOA and MONA. In: FORTE, pp. 19\u201334 (2000)","DOI":"10.1007\/978-0-387-35533-7_2"},{"key":"15_CR34","first-page":"99","volume":"1","author":"V. Stenning","year":"1976","unstructured":"Stenning, V.: A Data Transfer Protocol. Computer Networks\u00a01, 99\u2013110 (1976)","journal-title":"Computer Networks"},{"key":"15_CR35","unstructured":"Tanenbaum, A.S., Wetherall, D.: Computer Networks. Pearson (2010)"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bj\u00f8rner, N.: Symbolic Finite State Transducers: Algorithms and Applications. In: POPL, pp. 137\u2013150 (2012)","DOI":"10.1145\/2103621.2103674"},{"key":"15_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying Systems with Infinite but Regular State Spaces. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"},{"issue":"9","key":"15_CR38","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/s00236-005-0168-0","volume":"41","author":"M. Ying","year":"2005","unstructured":"Ying, M.: \u03c0-calculus with noisy channels. Acta Inf\u00a041(9), 525\u2013593 (2005)","journal-title":"Acta Inf"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38592-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T12:02:53Z","timestamp":1557748973000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38592-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385919","9783642385926"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38592-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}