Abstract
We study decision problems for parameterized verification of protocols for ad hoc networks. The problem we consider is control state reachability for networks of arbitrary size. We restrict our analysis to topologies that approximate the notion of bounded diameter often used in ad hoc networks for optimizing broadcast communication. We show that restricting to graphs with bounded diameter is not sufficient to make control state reachability decidable, but the problem turns out to be decidable when considering an additionally restricted class of graphs that still includes cliques. Although decidable, the problem is already Ackermann-hard over clique graphs.
Chapter PDF
Similar content being viewed by others
References
Abdulla, P.A., Čerāns, C., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313–321. IEEE Computer Society, Los Alamitos (1996)
Abdulla, P.A., Čerāns, C., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1-2), 109–127 (2000)
Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized Verification of Ad Hoc Networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313–327. Springer, Heidelberg (2010)
Delzanno, G., Sangnier, A., Zavattaro, G.: On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks. Technical Report DISI-TR-11-01, DISI-University of Genova (2011)
Ding, G.: Subgraphs and well quasi ordering. J. of Graph Theory 16(5), 489–502 (1992)
Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: LICS 1998, pp. 70–80. IEEE Computer Society, Los Alamitos (1998)
Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352–359. IEEE Computer Society, Los Alamitos (1999)
Fehnker, A., van Hoesel, L., Mader, A.: Modelling and verification of the LMAC protocol for wireless sensor networks. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 253–272. Springer, Heidelberg (2007)
Fernandess, Y., Malkhi, D.: K-clustering in wireless ad hoc networks. In: POMC 2002, pp. 31–37. ACM, New York (2002)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoret. Comp. Sci. 256(1-2), 63–92 (2001)
Hoffman, A., Singleton, R.: On Moore graphs with diameter 2 and 3. IBM J. Res. Develop. 4, 497–504 (1960)
Meyer, R.: On boundedness in depth in the pi-calculus. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds.) IFIP TCS 2008. IFIP, vol. 273, pp. 477–489. Springer, Heidelberg (2008)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Minsky, M.: Computation: finite and infinite machines. Prentice-Hall, Englewood Cliffs (1967)
Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoret. Comp. Sci. 6, 223–231 (1978)
Rosa-Velardo, F.: Depth boundedness in multiset rewriting systems with name binding. In: Kučera, A., Potapov, I. (eds.) RP 2010. LNCS, vol. 6227, pp. 161–175. Springer, Heidelberg (2010)
Saksena, M., Wibling, O., Jonsson, B.: Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 18–32. Springer, Heidelberg (2008)
Schnoebelen, P.: Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)
Singh, A., Ramakrishnan, C.R., Smolka, S.A.: Query-Based Model Checking of Ad Hoc Network Protocols. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 603–619. Springer, Heidelberg (2009)
Wies, T., Zufferey, D., Henzinger, T.A.: Forward analysis of depth-bounded processes. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 94–108. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delzanno, G., Sangnier, A., Zavattaro, G. (2011). On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks. In: Hofmann, M. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2011. Lecture Notes in Computer Science, vol 6604. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19805-2_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-19805-2_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19804-5
Online ISBN: 978-3-642-19805-2
eBook Packages: Computer ScienceComputer Science (R0)