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 cluster (graphs with bounded diameter) often used in ad hoc networks for optimizing broadcast communication. In particular we are interested in classes of graphs that include at least cliques of arbitrary order. We show that, although decidable, control state reachability over cliques is already Ackermann-hard and study more sophisticated topologies for which the problem remains decidable.
On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks / G. Delzanno; A. Sangnier; G. Zavattaro. - STAMPA. - LNCS 6604:(2011), pp. 441-455. (Intervento presentato al convegno Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 tenutosi a Saarbrucken, Germany nel March 26-April 3, 2011) [10.1007/978-3-642-19805-2_30].
On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks
ZAVATTARO, GIANLUIGI
2011
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 cluster (graphs with bounded diameter) often used in ad hoc networks for optimizing broadcast communication. In particular we are interested in classes of graphs that include at least cliques of arbitrary order. We show that, although decidable, control state reachability over cliques is already Ackermann-hard and study more sophisticated topologies for which the problem remains decidable.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
