{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:06:44Z","timestamp":1725746804376},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642402128"},{"type":"electronic","value":"9783642402135"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40213-5_14","type":"book-chapter","created":{"date-parts":[[2013,8,29]],"date-time":"2013-08-29T09:26:23Z","timestamp":1377768383000},"page":"217-232","source":"Crossref","is-referenced-by-count":6,"title":["Model Checking MANETs with Arbitrary Mobility"],"prefix":"10.1007","author":[{"given":"Fatemeh","family":"Ghassemi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saeide","family":"Ahmadi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wan","family":"Fokkink","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ali","family":"Movaghar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,8,30]]},"reference":[{"issue":"4","key":"14_CR1","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1145\/581771.581775","volume":"49","author":"K Bhargavan","year":"2002","unstructured":"Bhargavan, K., Obradovid, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. Journal of the ACM 49(4), 538\u2013576 (2002)","journal-title":"Journal of the ACM"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982)","DOI":"10.1007\/BFb0025774"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407\u2013419. Springer, Heidelberg (1990)","DOI":"10.1007\/3-540-53479-2_17"},{"issue":"2","key":"14_CR4","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R Nicola De","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. Journal of the ACM 42(2), 458\u2013487 (1995)","journal-title":"Journal of the ACM"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"De Renesse, R., Aghvami, A.H.: Formal verification of ad-hoc routing protocols using SPIN model checker. In: MELECON, pp. 1177\u20131182. IEEE (2004)","DOI":"10.1109\/MELCON.2004.1348275"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"14_CR7","doi-asserted-by":"crossref","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.) ESOP 2012. LNCS, vol. 7211, pp. 295\u2013315. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28869-2_15"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Fehnker, A., van Glabbeek, R., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using Uppaal. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 173\u2013187. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28756-5_13"},{"key":"14_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/FI-2010-316","volume":"103","author":"F Ghassemi","year":"2010","unstructured":"Ghassemi, F., Fokkink, W., Movaghar, A.: Equational reasoning on mobile ad hoc networks. Fundamenta Informaticae 103, 1\u201341 (2010)","journal-title":"Fundamenta Informaticae"},{"issue":"28","key":"14_CR10","doi-asserted-by":"publisher","first-page":"3262","DOI":"10.1016\/j.tcs.2011.03.017","volume":"412","author":"F Ghassemi","year":"2011","unstructured":"Ghassemi, F., Fokkink, W., Movaghar, A.: Verification of mobile ad hoc networks: An algebraic approach. Theoretical Computer Science 412(28), 3262\u20133282 (2011)","journal-title":"Theoretical Computer Science"},{"key":"14_CR11","unstructured":"Ghassemi, F., Ahmadi, S., Fokkink, W., Movaghar, A.: Model Checking MANETs with Arbitrary Mobility. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 214\u2013228. Springer, Heidelberg (2013)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Godskesen, J.C.: Observables for mobile and wireless broadcasting systems. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol. 6116, pp. 1\u201315. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-13414-2_1"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Godskesen, J.C.: A calculus for mobile ad hoc networks. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 132\u2013150. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-72794-1_8"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Kouzapas, D., Philippou, A.: A process calculus for dynamic networks. In: Bruni, R., Dingel, J. (eds.) FMOODS\/FORTE 2011. LNCS, vol. 6722, pp. 213\u2013227. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-21461-5_14"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"McIver, A., Fehnker, A.: Formal Techniques for Analysis of Wireless Network. In: ISoLA. LNCS vol. 6722, pp. 263\u2013270. IEEE (2006)","DOI":"10.1109\/ISoLA.2006.51"},{"issue":"6","key":"14_CR16","doi-asserted-by":"publisher","first-page":"1542","DOI":"10.1016\/j.ins.2007.10.023","volume":"178","author":"R Meolic","year":"2008","unstructured":"Meolic, R., Kapus, T., Brezocnik, Z.: ACTLW - An action-based computation tree logic with unless operator. Information Sciences 178(6), 1542\u20131557 (2008)","journal-title":"Information Sciences"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Merro, M.: An observational theory for mobile ad hoc networks. In: MFPS XXIII. ENTCS, vol. 173, pp. 275\u2013293. Elsevier (2007)","DOI":"10.1016\/j.entcs.2007.02.039"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Mezzetti, N., Sangiorgi, D.: Towards a calculus for wireless systems. In: MFPS XXII. ENTCS, vol. 158, pp. 331\u2013353. Elsevier (2006)","DOI":"10.1016\/j.entcs.2006.04.017"},{"key":"14_CR19","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall (1989)"},{"issue":"1","key":"14_CR20","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.tcs.2006.08.036","volume":"367","author":"S Nanz","year":"2006","unstructured":"Nanz, S., Hankin, C.: A framework for security analysis of mobile wireless networks. Theoretical Computer Science 367(1), 203\u2013227 (2006)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"14_CR21","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.ic.2009.10.003","volume":"208","author":"S Nanz","year":"2010","unstructured":"Nanz, S., Nielson, F., Nielson, H.: Static analysis of topology-dependent broadcast networks. Information and Computation 208(2), 117\u2013139 (2010)","journal-title":"Information and Computation"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Perkins, C.E., Belding-Royer, E.M.: Ad-hoc on-demand distance vector routing. In: WMCSA, pp. 90\u2013100. IEEE (1999)","DOI":"10.1109\/MCSA.1999.749281"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for mobile ad hoc networks. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 296\u2013314. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-68265-3_19"},{"issue":"3","key":"14_CR24","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R Glabbeek van","year":"1996","unstructured":"van Glabbeek, R., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), 555\u2013600 (1996)","journal-title":"Journal of the ACM"},{"key":"14_CR25","unstructured":"Vasudevan, S., Kurose, J., Towsley, D.: Design and analysis of a leader election algorithm for mobile ad hoc networks. In: ICNP, pp. 350\u2013360. IEEE Computer Society (2004)"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Wibling, O., Parrow, J., Pears, A.: Automatized verification of ad hoc routing protocols. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 343\u2013358. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-30232-2_22"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Wibling, O., Parrow, J., Pears, A.: Ad hoc routing protocol verification through broadcast abstraction. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 128\u2013142. Springer, Heidelberg (2005)","DOI":"10.1007\/11562436_11"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40213-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T19:51:40Z","timestamp":1596397900000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40213-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642402128","9783642402135"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40213-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}