{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:29:50Z","timestamp":1772836190830,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662494974","type":"print"},{"value":"9783662494981","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-49498-1_5","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T13:36:06Z","timestamp":1458567366000},"page":"95-122","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A Timed Process Algebra for Wireless Networks with an Application in Routing"],"prefix":"10.1007","author":[{"given":"Emile","family":"Bres","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rob","family":"van Glabbeek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"H\u00f6fner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"5_CR1","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/BF01214556","volume":"8","author":"J Baeten","year":"1996","unstructured":"Baeten, J., Bergstra, J.: Discrete time process algebra. Formal Aspects Comput. 8(2), 188\u2013208 (1996). doi:\n                    10.1007\/BF01214556","journal-title":"Formal Aspects Comput."},{"key":"5_CR2","unstructured":"Bergstra, J.A., Klop, J.W.: Observation of strains: algebra of communicating processes. In: de Bakker, J.W., Hazewinkel, M., Lenstra, J.K. (eds) Mathematics and Computer Science, CWI Monograpph 1, pp. 89\u2013138. North-Holland (2011)"},{"issue":"4","key":"5_CR3","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1145\/581771.581775","volume":"49","author":"K Bhargavan","year":"2002","unstructured":"Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM 49(4), 538\u2013576 (2002). doi:\n                    10.1145\/581771.581775","journal-title":"J. ACM"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T Bolognesi","year":"1987","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Comput. Netw. 14, 25\u201359 (1987). doi:\n                    10.1016\/0169-7552(87)90085-7","journal-title":"Comput. Netw."},{"key":"5_CR5","unstructured":"Bres, E., van Glabbeek, R.J., H\u00f6fner, P.: A Timed Process Algebra for Wireless Networks with an Application in Routing. Technical Report 9145, NICTA (2016). \n                    http:\/\/nicta.com.au\/pub?id=9145"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/11494881_20","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"S Chiyangwa","year":"2005","unstructured":"Chiyangwa, S., Kwiatkowska, M.: A timing analysis of AODV. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 306\u2013321. Springer, Heidelberg (2005). doi:\n                    10.1007\/11494881_20"},{"key":"5_CR7","unstructured":"Clausen, T., Jacquet, P.: Optimized Link State Routing Protocol (OLSR). RFC 3626 (Experimental), Network Working Group (2003). \n                    http:\/\/www.ietf.org\/rfc\/rfc3626.txt"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-540-85361-9_35","volume-title":"Concurrency Theory","author":"S Cranen","year":"2008","unstructured":"Cranen, S., Mousavi, M.R., Reniers, M.A.: A rule format for associativity. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 447\u2013461. Springer, Heidelberg (2008). doi:\n                    10.1007\/978-3-540-85361-9_35"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Edenhofer, S., H\u00f6fner, P.: Towards a rigorous analysis of AODVv2 (DYMO). In: Rigorous Protocol Engineering (WRiPE 2012). IEEE (2012). doi:\n                    10.1109\/ICNP.2012.6459942","DOI":"10.1109\/ICNP.2012.6459942"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-28869-2_15","volume-title":"Programming Languages and Systems","author":"A Fehnker","year":"2012","unstructured":"Fehnker, A., van Glabbeek, R., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 295\u2013315. Springer, Heidelberg (2012). doi:\n                    10.1007\/978-3-642-28869-2_15"},{"key":"5_CR11","unstructured":"Fehnker, A., van Glabbeek, R.J., H\u00f6fner, P., McIver, A.K., Portmann, M., Tan, W.L.: A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV. Technical report 5513, NICTA (2013). \n                    http:\/\/arxiv.org\/abs\/1312.7645"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Garcia-Luna-Aceves, J.J.: A unified approach to loop-free routing using distance vectors or link states. In: SIGCOMM 1989, SIGCOMM Computer Communication Review 19(4), pp. 212\u2013223. ACM Press (1989). doi:\n                    10.1145\/75246.75268","DOI":"10.1145\/75246.75268"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Garcia-Luna-Aceves, J.J., Rangarajan, H.: A new framework for loop-free on-demand routing using destination sequence numbers. In: MASS 2004, pp. 426\u2013435. IEEE (2004). doi:\n                    10.1109\/MAHSS.2004.1392182","DOI":"10.1109\/MAHSS.2004.1392182"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-57208-2_6","volume-title":"CONCUR\u201993","author":"RJ Glabbeek van","year":"1993","unstructured":"van Glabbeek, R.J.: The linear time - branching time spectrum II; the semantics of sequential systems with silent moves. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66\u201381. Springer, Heidelberg (1993). doi:\n                    10.1007\/3-540-57208-2_6"},{"key":"5_CR15","unstructured":"Glabbeek, R.J., H\u00f6fner, P., Portmann, M., Tan, W.L.: Modelling and Verifying the AODV Routing Protocol. Distributed Computing (2016) (to appear)"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.J., H\u00f6fner, P., Tan, W.L., Portmann, M.: Sequence numbers do not guarantee loop freedom \u2013AODV can yield routing loops\u2013. In: MSWiM 2013, pp. 91\u2013100. ACM Press (2013). doi:\n                    10.1145\/2507924.2507943","DOI":"10.1145\/2507924.2507943"},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1006\/inco.1995.1041","volume":"117","author":"M Hennessy","year":"1995","unstructured":"Hennessy, M., Regan, T.: A process algebra for timed systems. Inf. Comput. 117(2), 221\u2013239 (1995). doi:\n                    10.1006\/inco.1995.1041","journal-title":"Inf. Comput."},{"key":"5_CR18","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"H\u00f6fner, P., van Glabbeek, R.J., Tan, W.L., Portmann, M., McIver, A.K., Fehnker, A.: A Rigorous analysis of AODV and its variants. In: MSWiM 2012, pp. 203\u2013212. ACM Press (2012). doi:\n                    10.1145\/2387238.2387274","DOI":"10.1145\/2387238.2387274"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"IEEE: IEEE Standard for Information Technology\u2014Telecommunications and information exchange between systems\u2014Local and metropolitan area networks \u2014Specific requirements Part 11: Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) specifications Amendment 10: Mesh Networking (2011). doi:\n                    10.1109\/IEEESTD.2011.6018236","DOI":"10.1109\/IEEESTD.2011.6018236"},{"issue":"3","key":"5_CR21","first-page":"219","volume":"2","author":"N Lynch","year":"1989","unstructured":"Lynch, N., Tuttle, M.: An introduction to input\/output automata. CWI-Q. 2(3), 219\u2013246 (1989). Centrum voor Wiskunde en Informatica, Amsterdam","journal-title":"CWI-Q."},{"key":"5_CR22","unstructured":"McCune, W.W.: Prover9 and Mace4. \n                    http:\/\/www.cs.unm.edu\/ mccune\/prover9\n                    \n                  . Accessed 10 October 2015"},{"key":"5_CR23","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/BFb0039073","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"F Moller","year":"1990","unstructured":"Moller, F., Tofts, C.: A temporal calculus of communicating systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 401\u2013415. Springer, Heidelberg (1990). doi:\n                    10.1007\/BFb0039073"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-19195-9_7","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"KS Namjoshi","year":"2015","unstructured":"Namjoshi, K.S., Trefler, R.J.: Loop freedom in AODVv2. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 98\u2013112. Springer, Heidelberg (2015). doi:\n                    10.1007\/978-3-319-19195-9_7"},{"key":"5_CR26","unstructured":"Neumann, A., Aichele, M., Lindner, C., Wunderlich, S.: Better Approach To Mobile Ad-hoc Networking (B.A.T.M.A.N.). Internet-Draft (Experimental), Network Working Group (2008). \n                    http:\/\/tools.ietf.org\/html\/draft-openmesh-b-a-t-m-a-n-00"},{"issue":"1","key":"5_CR27","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1006\/inco.1994.1083","volume":"114","author":"X Nicollin","year":"1994","unstructured":"Nicollin, X., Sifakis, J.: The algebra of timed processes, ATP: theory and application. Inf. Comput. 114(1), 131\u2013178 (1994). doi:\n                    10.1006\/inco.1994.1083","journal-title":"Inf. Comput."},{"key":"5_CR28","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.entcs.2005.12.093","volume":"162","author":"J Ouaknine","year":"2006","unstructured":"Ouaknine, J., Schneider, S.: Timed CSP: a retrospective. Electronic Notes Theor. Comput. Sci. 162, 273\u2013276 (2006). doi:\n                    10.1016\/j.entcs.2005.12.093","journal-title":"Electronic Notes Theor. Comput. Sci."},{"key":"5_CR29","unstructured":"Perkins, C.E., Belding-Royer, E.M., Das, S.: Ad hoc On-Demand Distance Vector (AODV) Routing. RFC 3561 (Experimental), Network Working Group (2003). \n                    http:\/\/www.ietf.org\/rfc\/rfc3561.txt"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Perkins, C.E., Royer, E.M.: Ad-hoc on-demand distance vector routing. In: Mobile Computing Systems and Applications (WMCSA 1999), pp. 90\u2013100. IEEE (1999). doi:\n                    10.1109\/MCSA.1999.749281","DOI":"10.1109\/MCSA.1999.749281"},{"key":"5_CR31","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.jlap.2004.05.001","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Logic Algebraic Program. 60\u201361, 17\u2013139 (2004). doi:\n                    10.1016\/j.jlap.2004.05.001\n                    \n                  . Originally appeared in (1981)","journal-title":"J. Logic Algebraic Program."},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-16761-7_81","volume-title":"Automata, Languages and Programming","author":"G Reed","year":"1986","unstructured":"Reed, G., Roscoe, A.: A timed model for communicating sequential processes. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 314\u2013323. Springer, Heidelberg (1986). doi:\n                    10.1007\/3-540-16761-7_81"},{"key":"5_CR33","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/0304-3975(85)90093-3","volume":"37","author":"R Simone de","year":"1985","unstructured":"de Simone, R.: Higher-level synchronising devices in meije-SCCS. Theor. Comput. Sci. 37, 245\u2013267 (1985). doi:\n                    10.1016\/0304-3975(85)90093-3","journal-title":"Theor. Comput. Sci."},{"key":"5_CR34","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1016\/j.scico.2009.07.008","volume":"75","author":"A Singh","year":"2010","unstructured":"Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for Mobile Ad Hoc Networks. Sci. Comput. Program. 75, 440\u2013469 (2010). doi:\n                    10.1016\/j.scico.2009.07.008","journal-title":"Sci. Comput. Program."},{"key":"5_CR35","doi-asserted-by":"publisher","unstructured":"Zhou, M., Yang, H., Zhang, X., Wang, J.: The proof of AODV loop freedom. In: Wireless Communications & Signal Processing (WCSP 2009), IEEE (2009). doi:\n                    10.1109\/WCSP.2009.5371479","DOI":"10.1109\/WCSP.2009.5371479"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49498-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T01:03:58Z","timestamp":1584925438000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49498-1_5"}},"subtitle":["(Extended Abstract)"],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662494974","9783662494981"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49498-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}