We study decidability and undecidability results for parameterized verification of a formal model of timed Ad Hoc network protocols. The communication topology is represented by a graph and the behavior of each node is represented by a timed automaton communicating with its neighbors via broadcast messages. We consider verification problems formulated in terms of reachability, starting from initial configurations of arbitrary size, of a configuration that contain at least one occurrence of a node in a certain state. We study the problem for dense and discrete time and compare the results with those obtained for (fully connected) networks of timed automata. © 2011 Springer-Verlag.
CITATION STYLE
Abdulla, P. A., Delzanno, G., Rezine, O., Sangnier, A., & Traverso, R. (2011). On the verification of timed ad hoc networks. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6919 LNCS, pp. 256–270). https://doi.org/10.1007/978-3-642-24310-3_18
Mendeley helps you to discover research relevant for your work.