{'fraction_non_alphanumeric': 0.03751567904519366, 'fraction_numerical': 0.007411912273366529, 'mean_word_length': 4.205777601899485, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 10, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Parameterized Verification of Safety Properties in Ad Hoc Network Protocols

We summarize the main results proved in recent work on the parameterized verification of safety properties for ad hoc network protocols. We consider a model in which the communication topology of a network is represented as a graph. Nodes represent states of individual processes. Adjacent nodes represent single-hop neighbors. Processes are finite state automata that communicate via selective broadcast messages. Reception of a broadcast is restricted to single-hop neighbors. For this model we consider a decision problem that can be expressed as the verification of the existence of an initial topology in which the execution of the protocol can lead to a configuration with at least one node in a certain state. The decision problem is parametric both on the size and on the form of the communication topology of the initial configurations. We draw a complete picture of the decidability and complexity boundaries of this problem according to various assumptions on the possible topologies.


Introduction
Ad hoc networks consist of wireless hosts that, in the absence of a fixed infrastructure, communicate sending broadcast messages. In this context protocols are typically supposed to work independently from the communication topology and from the size (number of nodes) of the network. As suggested in [3,4], the control state reachability problem (or coverability problem) seems a particularly adequate formalization of parameterized verification problems for ad hoc networks. A network is represented as a graph in which nodes are individual processes and edges represent communication links. Each node executes an instance of the same protocol. A protocol is described by a finite state communicating automaton. The control state reachability problem consists in checking whether there exists an initial graph (with unknown size and topology) that can evolve into a configuration in which at least one node is in a given error state. Since the size of the initial configuration is not fixed a priori, the state-space to be explored is in general infinite.
In this paper we summarize the main results that we have proved in two recent publications [3,4]. The first result is negative: control state reachability is undecidable if we do not fix any restriction on the possible topologies. As for other communication models [16,25], finding interesting classes of network topologies for which verification is, at least theoretically, possible is an important research problem. As a first positive result, we have proved in [3] that control state reachability turns out to be decidable for the class of bounded path graphs. Graphs have bounded path if there exists a value k such that all simple paths in the considered graph have length smaller than k. Although for a fixed k this class of graphs is infinite, it appears of limited interest as it does not include clique graphs. Cliques are appealing for at least two reasons. First, they represent the best possible scenario for optimizing broadcast communication (one broadcast to reach all nodes). Second, when restricting configurations only to cliques, control state reachability can be reduced to coverability in a Broadcast Protocol, i.e., in a model in which configurations are multisets of processes defined by communicating automata [6]. Coverability is decidable in Broadcast Protocols in [8].
For these reasons, in [4] we have decided to investigate classes of graphs that at least include the clique graphs. More precisely, we have considered networks in which the underlying topology is in between the class of cliques and the strictly larger class of bounded diameter graphs. Graphs have bounded diameter if there exists a value k such that the minimal path between every pair of nodes of the same graph has length smaller than k. Graphs with bounded diameter (also called clusters) are particularly relevant for the domain of ad hoc networks. They are often used to partition a network in order to increase the efficiency of broadcast communication [10].
The restriction to bounded diameter follows the approach taken for point-to-point communication in [16,25]. Differently from [16,25] we have proved that for our model of selective broadcast control state reachability is undecidable when restricting the topologies to graphs whose diameter is bounded by k (for a fixed k > 0). Then, we have investigated further restrictions having in mind the constraint that they must allow at least cliques of arbitrary order. By using an original well-quasi ordering result, we have proved that control state reachability becomes decidable when considering a class of graphs in which the corresponding maximal cliques are connected by paths of bounded length. Furthermore, by exploiting a recent result of Schnoebelen [21] and a reduction to coverability in reset nets, we have shown that the resulting decision procedure is Ackermann-hard. Interestingly, the same complexity result already holds in the subclass of clique topologies.
Related Work Ethernet-like broadcast communication has been analyzed by Prasad [18] using the Calculus of Broadcasting Systems, in which all processes receive a broadcast message at once. A similar type of broadcast mechanism is used in the Broadcast Protocols of Emerson and Namjoshi [6]. In our setting, this is similar to the case in which all nodes share a common group (the underlying graph is a clique). Ene and Muntean presented the bπ-calculus [7], an extension of the π-calculus [19] with a broadcast such that only nodes listening on the right channel can receive emitted messages. Wireless broadcast communication has been investigated in the context of process calculi by Nanz and Hankin [17], Singh, Ramakrishnan and Smolka [22,23], Lanese and Sangiorgi [14], Godskesen [12], and Merro [15]. In particular Nanz and Hankin [17] consider a graph representation of node localities to determine the receivers of a message, while Godskesen [12] makes use of a neighbour relation. On the contrary, Lanese and Sangiorgi [14] and Merro [15] associate physical locations to processes so that the receivers depend on the location of the emitter and its transmission range. As already mentioned, we have been directly inspired by the ω-calculus of Singh, Ramakrishnan and Smolka [22,23]. The ω-calculus is based on the π-calculus. The π-calculus [19] intermixes the communication and mobility of processes by expressing mobility as change of interconnection structure among processes through communication. In the ω-calculus mobility of processes is abstracted from their communication actions, i.e., mobility is spontaneous and it does not involve any communication. In [24] the same authors define a constraint-based analysis for configurations with fixed topologies and a fixed number of nodes. The authors also mention that checking reachability of a configuration from an initial one is decidable for the fragment without restriction. This property is an immediate consequence of the fact that there is no dynamic generation or deletion of processes (i.e. it boils down to a finite-state reachability problem). The symbolic approach in [24] seems to improve verification results obtained with more standard model checking techniques. For instance, in [9] model checking is used for automatic verification of finite-state and timed models of Ad Hoc Networks. In these works the number of nodes in the initial configurations is known and fixed a priori. In order to detect protocol vulnerabilities tools like Uppaal are executed on all possible topologies (modulo symmetries) for a given number of nodes. In [20] Saksena et al. define a symbolic procedure based on graph-transformations to analyze routing protocol for Ad Hoc Networks. The symbolic representation is based on upward closed sets of graphs ordered w.r.t. subgraph inclusion. Their procedure is not guaranteed to terminate. In our paper we consider a non trivial class of graphs (bounded path configurations) for which backward analysis with a similar symbolic representation (upward closure of graphs w.r.t. induced subgraph ordering) is guaranteed to terminate for finite-state descriptions of individual nodes.
Structure of the paper In Section 2 we formally introduce our model for ad hoc network protocols, we define the parametric version of the control state reachability problem, and we recall the result from [3], i.e. that control state reachability is undecidable if we do not impose any restriction on the class of possible topologies, while it turns out to be decidable when restricting to bounded path topologies. In Sections 3 and 4 we consider other restricted classes that include clique graphs: bounded diameter and bounded path on the maximal clique graph, respectively. For these classes we report the results proved in [4]: control state reachability is undecidable when restricted to graphs with a bounded diameter (but it turns out to be decidable if we additionally assume bounded degree), while for the class of graphs having a corresponding maximal clique graph with bounded path, the problem is decidable. Section 5 contains concluding remarks and directions for future work.

Preliminaries on Graphs
In this section we assume that Q is a finite set of elements. A Q-labeled undirected graph (shortly Qgraph or graph) is a tuple G = (V, E, L), where V is a finite set of vertices (sometimes called nodes), and E ⊆ V × V is a finite set of edges, and L : V → Q is a labeling function. We consider here undirected graphs, i.e., such that u, v ∈ E iff v, u ∈ E. We denote by G Q the set of Q-graphs. For an edge u, v ∈ E, u and v are called its endpoints and we say that u and v are adjacent vertices. For a node u we call vicinity the set of its adjacent nodes (neighbors). Given a vertex v ∈ V , the degree of v is the size of the set {u ∈ V | v, u ∈ E}. The degree of a graph is the maximum degree of its vertices. We will sometimes denote L(G) the set L(V ) (which is a subset of Q). A path π in a graph is a finite sequence v 1 , v 2 , . . . , v m of vertices such that for 1 ≤ i ≤ m − 1, v i , v i+1 ∈ E and the integer m − 1 (i.e. its number of edges) is called the length of the path π, denoted by |π|.
. The diameter of a graph G = V, E, L is the length of the longest shortest simple path between any two vertices of G. Hence, the diameter of a clique graph is always one. We also need to define some graph orderings. Given two graphs G = V, E, L and As an example, a path with three nodes is a subgraph, but not an induced subgraph, of a ring of the same order. Finally, we recall the notion of well-quasi-ordering (wqo for short). A quasi order (A, ≤) is a wqo if for every infinite sequence of elements a 1 , a 2 , . . . , a i , . . . in A, there exist two indices i < j s.t. a i ≤ a j . Examples of wqo's are the sub-multiset relation, and both the subgraph and the induced subgraph relation over graphs with simple paths of bounded length [5].

Ad Hoc Networks
In our model of ad hoc networks a configuration is simply a graph and we assume that each node of the graph is a process that runs a common predefined protocol. A protocol is defined by a communicating automaton with a finite set Q of control states. Communication is achieved via selective broadcast. The effect of a broadcast is in fact local to the vicinity of the sender. The initial configuration is any graph in which all the nodes are in an initial control state. Remark that even if Q is finite, there are infinitely many possible initial configurations. We next formalize the above intuition. Individual Behavior The protocol run by each node is defined via a process P = Q, Σ, R, Q 0 , where Q is a finite set of control states, Σ is a finite alphabet, R ⊆ Q × ({τ} ∪ {!!a, ??a | a ∈ Σ}) × Q is the transition relation, and Q 0 ⊆ Q is a set of initial control states. The label τ represents the capability of performing an internal action, and the label !!a (??a) represents the capability of broadcasting (receiving) a message a ∈ Σ. Network Semantics An AHN associated to P = Q, Σ, R, Q 0 is defined via a transition system A P = C , ⇒, C 0 , where C = G Q (undirected graphs with labels in Q) is the set of configurations, C 0 = G Q 0 (undirected graphs with labels in Q 0 ) is the subset of initial configurations, and ⇒⊆ C × C is the transition relation defined next. For q ∈ Q and a ∈ Σ, we define the set R a (q) = {q ′ ∈ Q | q, ??a, q ′ ∈ R} that contains states that can be reached from the state q upon reception of message a. For G = V, E, L and G ′ = V ′ , E ′ , L ′ , G ⇒ G ′ holds iff G and G ′ have the same underlying structure, i.e., V = V ′ and E = E ′ , and one of the following conditions on L and L ′ holds: • ∃v ∈ V s.t. (L(v), τ, L ′ (v)) ∈ R, and L(u) = L ′ (u) for all u in V \ {v}; • ∃v ∈ V s.t. (L(v), !!a, L ′ (v)) ∈ R and for every u ∈ V \ {v} -if v, u ∈ E and R a (L(u)) = / 0 (reception of a in u is enabled), then L ′ (u) ∈ R a (L(u)).
An execution is a sequence G 0 G 1 . . . such that G 0 ∈ G Q 0 and G i ⇒ G i+1 for i ≥ 0. We use ⇒ * to denote the reflexive and transitive closure of ⇒.
Observe that a broadcast message a sent by v is delivered only to the subset of neighbors interested in it. Such a neighbor u updates its state with a new state taken from R(L(u)). All the other nodes (including neighbors not interested in a) simply ignore the message. Also notice that the topology is static, i.e., the set of nodes and edges remain unchanged during a run.
Finally, for a set of Q-graphs T ⊆ G Q , the AHN A T P restricted to T is defined by the transition system C ∩ T , ⇒ T , C 0 ∩ T where the relation ⇒ T is the restriction of ⇒ to (C ∩ T ) × (C ∩ T ).

Example of Ad Hoc Network Protocol
As an example of an ad hoc network protocol and of its semantics, consider a protocol consisting of the following rules: (A, τ,C), (C, !!m, D), (B, ??m,C), and (A, ??m,C). As shown in Fig. 1, starting from Figure 1: Example of execution configuration with only A and B nodes, an A node first moves to C and then send m to his/her neighbors. In turn, they forward the message m to their neighbors, and so on.

Decision problem
We define the decision problem of control state reachability (COVER) as follows: Input: A process P = Q, Σ, R, Q 0 with A P = C , ⇒, C 0 and a control state q ∈ Q; Output: Yes, if there exists G ∈ C 0 and G ′ ∈ C such that q ∈ L(G ′ ) and G ⇒ * G ′ , no otherwise.
Control state reachability is strictly related to parameterized verification of safety properties. The input control state q can in fact be seen as an error state for the execution of the protocol in some node of the network. If the answer to COVER is yes, then there exists a sufficient number of processes, all executing the same protocol, and an initial topology from which we can generate a configuration in which the error is exposed. Under this perspective, COVER can be viewed as instance of a parameterized verification problem.
In [3] we have proved that COVER is undecidable. The proof is by reduction from the halting problem for two-counter Minsky machines. A Minsky machine manipulates two integer variables c 1 and c 2 , which are called counters, and it is composed of a finite set of instructions. Each of the instuction is either of the form (1) L : c i := c i + 1; goto L ′ or (2) L : if c i = 0 then goto L ′ else c i := c i − 1; goto L ′′ where i ∈ {1, 2} and L, L ′ , L ′′ are labels preceding each instruction. Furthermore there is a special label L F from which nothing can be done. The halting problem consists then in deciding whether or not the execution that starts from L 0 with counters equal to 0 reaches L F .
The intuition behind the reduction is as follows. In a first phase we exploit an exploration protocol to impose a logical topology on top of the actual physical node connections. This logical topology is composed by a control node which is connected to two distinct lists of nodes used to simulate the content of the counters. Each node in the list associated to counter c i is either in state Z i or NZ i . The current value of the counter c i equals the number of NZ i nodes in the list. The length of each list is guessed non-deterministically during the execution of the first phase (i.e. before starting the simulation) and it corresponds to the maximum value store in a counter for the simulation to succeed. Initially, all nodes must encode zero (state Z i ).
In the second phase the control node starts the simulation of the instructions. It operates by sending requests that are propagated back and forth a list by using broadcast sent by a node to its (unique) singlehop successor/predecessor node. The effect of these requests is to change the state of one node in zero state Z i to the non-zero state NZ i in case of increment, or the vice versa in the case of decrement. The test-for-zero instruction on the counter c i is simply simulated by checking whether there are no nodes in the zero state Z i in the i-th list.

Configurations with Bounded Path
In [3] we have proved that COVER turns out to be decidable if we restrict the possible topologies to the class of graphs whose path is bounded by k (for a fixed k > 0). The proof is based on the theory of Well Structured Transition Systems [1,2,11] (WSTS). A WSTS is a transition system equipped with a wellquasi ordering on states and a monotonicity property: if a configuration c 1 smaller than a configuration c 2 has a transition to a configuration c ′ 1 , then also c 2 has a transition to a configuration c ′ 2 which is greater than c ′ 1 . Coverability turns out to be decidable in WSTSs by using backward analysis, if it is possible to compute the predecessors of a given state.
In [3] we have observed that ad hoc network protocols are monotonic with respect to the induced subgraph ordering relation, while this is not the case for the subgraph ordering relation. This is already an interesting observation that distinguishes selective broadcast from point-to-point communication, which is monotonic with respect to the usual subgraph ordering. The proof of decidability is completed by defining how to compute the predecessors, and by observing that the induced subgraph ordering is a wqo for the class of graphs for which the length of simple paths is bounded by a constant (i.e. bounded path graphs). This result is known as Ding's Theorem [5].

Configurations with Bounded Diameter
As mentioned in the introduction, restricting protocol analysis to configurations with bounded path seems to have a limited application in a communication model with selective broadcast. For these reasons, in [4] we have investige COVER for restricted classes of graphs that at least include the class of clique graphs. The first class we have consider is that of graphs with bounded diameter. Fixed k > 0, a graph G has a k-bounded diameter if and only if its diameter is smaller than or equal to k. Observe that for every k > 0, clique graphs belong to the class of graphs with a diameter bounded by k. Furthermore, given k > 0 the class of graphs with path bounded by k is included in the class of graphs with a diameter bounded by k. Graphs with k-bounded diameter coincide with the so called k-clusters used in partitioning algorithm for ad hoc networks [10]. Thus, this class is of particular relevance for the analysis of selective broadcast communication. Intuitively, the diameter corresponds to the minimal number of broadcasts (hops) needed to send a message to all nodes connected by a path with the sender.
The COVER problem restricted to configurations with k-bounded diameter turns out to be undecidable for k > 1. The proof is similar to the proof of undecidability for the general case reported in [3]: by reduction from the halting problem for two-counter Minsky machines.
The main difference is that the logical topology to be imposed in the first phase of the simulation of the Minsky machines should be with bounded diameter (namely, diameter 2). The topology that we have considered is a sort of butterfly (see Figure 2) consisting of two lists (to represent the counters) and in which all nodes in the lists are connected to a monitor node (to represent the program counter). The second phase of the simulation, i.e. the actual execution of the instructions, proceeds similarly to the protocol described above. The unique difference is that we use a distinct f irstZ i node to distinguish the initial node of each list (this is needed as now all the list nodes are connected to the program counter node).
Note that if we restrict our attention to graphs with a diameter bounded by 1, the above encoding does not work anymore. The class of graphs with diameter 1 corresponds to the set of clique graphs and, as said above, COVER turns out to be decidable when restricting to clique topologies.

Bounded diameter and bounded degree.
From a non trivial result on bounded diameter graphs [13], we have obtained in [4] an interesting decidable subclass. Indeed, in [13] the authors show that, given two integers k, d > 0, the number of graphs whose diameter is smaller than k and whose degree is smaller than d is finite. The Moore bound is an upper bound for the size of the largest undirected graph in such a class. It follows that, for k, d > 0, and an ad hoc protocol with n states, if we restrict to configurations with a diameter bounded by k and a degree bounded by d, the state space is bounded by n M(k,d) , thus it is polynomial in the size of the protocol. Consequently we can conclude that COVER restricted to configurations with k-bounded diameter and d-bounded degree is in PSPACE.

Maximal Clique Graphs with Bounded Paths
In this section we describe classes of graphs that strictly increases both the classes of clique graphs and the classes of bounded path graphs, for which we have proved in [4] that COVER is decidable. We have called these classes of graphs BPC n (n-Bounded Path maximal Cliques graphs). Namely, for n > 0 BPC n contains both n-bounded path graphs and any clique graph, while being strictly contained in the class of graphs with 2n-bounded diameter. These classes are defined on top of the notion of maximal clique graphs associated to a configuration. • W ⊆ 2 V is the set of maximal cliques of G; Note that for each connected graph G there exists a unique maximal clique graph K G . An example of construction is given by Figure 3. One can also easily prove that if G is a clique graph then in K G there is no path of length strictly greater than 3. Furthermore, from the maximality of the cliques in W if two G K G Figure 3: A graph G and its associated clique graph K G .
nodes v 1 , v 2 ∈ V are connected both to w 1 and w 2 ∈ W , then w 1 and w 2 are distinct cliques. We use the notation v 1 ∼ w v 2 to denote that v 1 , v 2 belong to the same clique w.

Definition 4.2
For n ≥ 1, the class BPC n consists of the set of configurations whose associate maximal clique graph has n-bounded paths (i.e. the length of the simple paths of K G is at most n).
The proof of decidability of COVER for BPC n graphs is based on an ordering defined on maximal clique graphs that corresponds to the induced subgraph ordering defined on the corresponding graphs. Such a new ordering is defined as follows.

Definition 4.3 Assume
with G 1 and G 2 both connected graphs. Then, G 1 ⊑ G 2 iff there exist two injective functions f : X 1 → X 2 and g : W 1 → W 2 , such that ). The first condition ensures that (dis)connected nodes remain (dis)connected inside the image of g. Indeed, from point (i) it follows that, for every v 1 , v 2 ∈ X 1 , and The second condition ensures that disconnected nodes remain disconnected outside the image of g.
By condition (i) in the definition of ⊑, we also have that G 1 ⊑ G 2 (via f and g) implies that K G 1 is in the induced subgraph relation with K G 2 (via f ∪ g). The relation between this new relation and the induced subgraph ordering is even stronger, in fact we have proved in [4] that the two coincide: G 1 ⊑ G 2 iff G 1 is an induced subgraph of G 2 .
The main theorem in [4] states that for any n ≥ 1, (BPC n , ⊑) is a well-quasi ordering. In the light of the correspondance result between ⊑ and the induced subgraph ordering, and the monotonicity of ad hoc network protocol with respect to the induced subgraph ordering relation (and the computability of the predecessors) discussed the previous section, we have been able to prove in [4] the decidability of COVER for topologies restricted to graphs in BPC n (for a fixed n > 0).
In [4] we have investigated also the complexity of the decision procedure for COVER restricted to topologies in BPC n . We have found that this problem is not primitive recursive. The proof is by reduction from the coverability problem for reset nets, which is known to be an Ackermann-hard problem [21].

Conclusions
In this paper we have reported the main result that we have recently proved in [3,4] about the decidability and complexity boundaries for the decidability and the complexity of the parametric verification of safety properties in ad hoc networks. Namely, given an ad hoc network protocol expressed as a finite state communicating automaton, we are interested in checking the existence of an initial network configuration that can generate a computation leading to a configuration in which at least one node is in a given (error) state.
The problem is undecidable if no restrictions are imposed to the possible initial configurations, but it turns out to be decidable for interesting classes of graphs in which the corresponding maximal cliques are connected by paths of bounded length. These graphs include both cliques and bounded path graphs. The problem returns to be undecidable for bounded diameter graphs.
As a future work, we plan to study decidability and complexity issues in presence of communication and node failures. In particular, an interesting case of communication failure in the context of ad hoc networks is due to conflicts deriving form the contemporaneous emission of signals from two distinct nodes that share some neighbors. We plan to move to a truly concurrent semantics for ad hoc network protocols in order to faithfully represent this specific phenomenon.