Aziz Parosh

Mohamed Faouzi Abdulla

Othmane Atig

Rezine

Verification of Directed Acyclic Ad Hoc Networks

We study decision problems for parameterized verification of a formal model of ad hoc networks. We consider a model in which the network is composed of a set of processes connected to each other through a directed acyclic graph. Vertices of the graph represent states of individual processes. Adjacent vertices represent single-hop neighbors. The processes are finite-state machines with local and synchronized broadcast transitions. Reception of a broadcast is restricted to the immediate neighbors of the sender process. The underlying connectivity graph constrains communication pattern to only one direction. This allows to model typical communication patterns where data is propagated from a set of central nodes to the rest of the network, or alternatively collected in the other direction. For this model, we consider decidability of the control state reachability (coverability) problem, defined over two classes of architectures, namely the class of all acyclic networks (for which we show undecidability) and that of acyclic networks with a bounded depth (for which we show decidability). The decision problems are parameterized both by the size and by the topology of the underlying network.

Introduction

The analysis and verification of models for wireless ad hoc networks have attracted much interest in recent years [START_REF] Fehnker | Modelling and verification of the LMAC protocol for wireless sensor networks[END_REF][START_REF] Saksena | Graph grammar modeling and verification of Ad Hoc Routing Protocols[END_REF][START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF][START_REF] Delzanno | On the power of cliques in the parameterized verification of ad hoc networks[END_REF][START_REF] Nanz | A framework for security analysis of mobile wireless networks[END_REF][START_REF] Merro | A timed calculus for wireless systems[END_REF][START_REF] Singh | Query-based model checking of ad hoc network protocols[END_REF][START_REF] Singh | A process calculus for mobile ad hoc networks[END_REF][START_REF] Prasad | A calculus of broadcasting systems[END_REF]. Such networks usually consist of arbitrary numbers of nodes that communicate wirelessly in arbitrarily configured networks. Several features in their behaviors make them both attractive and difficult from the point of view of verification. First, the network infrastructure can be static or dynamic but is usually not a priori defined. Also, the communication between nodes occurs via broadcast over the shared radio channel medium. Messages broadcasted by a given node are only received by nodes in its proximity, in contrast to classical broadcast communication in which all processes of the system are able to receive the sent messages. Furthermore, since the systems may contain unbounded numbers of processes, and since the protocols are supposed to work independently from specific configurations of the network, we need to perform parameterized verification where we prove correctness of the system regardless of the number of nodes or the topology of the network.

Using a model similar to that proposed in [START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF], we view the network as a graph of nodes, where each node runs an instance of a given finite-state process. The graph defines the underlying connectivity of the network, while a process models the code of a given fixed protocol that runs on the node. For such networks, the behavior of a node can in general be specified in terms of a sequence of states with transitions corresponding to local or to broadcast operations. Local transitions are internal to a node and do not affect the states of the other nodes in the network. Broadcast transitions on the other hand may have an impact on other nodes in the network. More precisely, we consider selective broadcast transitions that involve a sender (the broadcasting node), together with a set of receivers composed of the nodes that are in the topological vicinity of the sender, and that are willing to receive the broadcasted message. The vicinity of a node is defined by the underlying communication graph of the network. The broadcasting and the reception of the message happens synchronously for all involved nodes, i.e., the sender and all potential receivers in its vicinity. The interleaving semantics of our formalism does not take into account problems that could arise at the physical and link layer, such us message collision for example. We are here more interested in network and application layer protocols where these type of problems are abstracted away.

As argued in [START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF][START_REF] Delzanno | On the power of cliques in the parameterized verification of ad hoc networks[END_REF], the control state reachability problem or the coverability problem seems to be adequate for capturing several interesting properties that arise in parameterized verification of ad hoc networks. The problem consists in checking whether the system can start from a given initial configuration and evolve to reach a configuration in which at least one of the processes is in a given state. Since we are performing parameterized verification, the number of nodes that has to be handled in the analysis is not a priori bounded. In other words, we are dealing with the verification of an infinite-state system. Indeed, it is shown in [START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF] that the coverability problem is undecidable in the general case. Therefore, an important line of work has been done to identify classes of network topologies for which algorithmic verification is at least theoretically possible [START_REF] Delzanno | On the power of cliques in the parameterized verification of ad hoc networks[END_REF]. This paper proposes one such a class of topologies where the underlying graph is acyclic, and hence the communication from a node to another goes only through one direction. Such patterns arise, for instance, in the context of Wireless Sensor Networks (Wsn), where small wireless devices are distributed over an area in order to perform different types of measurements (temperature, humidity, etc.). In Wsn, it is common that the topology is static over time. Furthermore, it is also common in Wsn that communication follows a specific direction; for instance this is the case for flooding protocols at the network layer [START_REF] Levis | Trickle: A self-regulating algorithm for code propagation and maintenance in wireless sensor networks[END_REF], and for the optimized directed diffusion protocol [START_REF] Intanagonwiwat | Directed diffusion for wireless sensor networking[END_REF].

From the verification point of view, we show that the coverability problem is undecidable even in the case where the network topology is acyclic (section 5). We show the undecidability result through a reduction from an undecidable problem for finite-state transducers (section 4). Then, we consider a restricted version of the problem where we assume that the depth of the acyclic graph is bounded by a given natural number k. In fact, we are still dealing with an infinite state-system since we may have an unbounded number of nodes, and an unbounded in-and out-degrees for the nodes of the graph. For this case we show decidability of the coverability problem. The proof is carried out in several steps. First we reduce the problem from the case of general acyclic graphs to that of inverted forests (forests with all edges reversed) and then to the case of inverted trees (section 6). For the case of inverted trees, we propose a novel symbolic representation of infinite sets of configurations. This symbolic representation amounts to having "higher-order multisets" in which a multiset of a certain order contains multisets of lower orders (section 7). We show that this allows to define a symbolic backward reachability analysis based on a non-trivial instantiation of the the framework of well quasi-ordered transition systems [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF].

Preliminaries

In this section, we introduce some basic definitions and notations that we will use in the rest of the paper.

We use N and N ą0 to denote the sets of natural numbers and positive natural numbers, respectively. Given a finite set A, we use |A| to denote the number of elements in A. We use A b to denote the set of finite multisets over A; and use A to denote the set of finite words over A. For words w 1 , w 2 P A ˚we use w 1 ¨w2 to denote the concatenation of w 1 and w 2 . Sometimes, we write multisets as lists, e.g., ra, a, b, b, bs is a multiset with two occurrences of a and three occurrences of b. A quasi-ordering (ordering for short) Ď on a set A is a reflexive and transitive binary relation over A (i.e. ĎĎ A ˆA, a Ď a and a Ď b, b Ď c ñ a Ď c for any a, b, c P A). We extend the ordering Ď on A to an ordering Ď b on the set A b of multisets over A such that ra 1 , . . . , a m sĎ b rb 1 , . . . , b n s if there is an injection h : t1, . . . , mu Þ Ñ t1, . . . , nu with a i Ď b hpiq for all i : 1 ď i ď m. Given a function f : A Þ Ñ N, we define maxpf q :" max tf peq|e P Au to be the largest value taken by f over A. For a function f : A Þ Ñ B, we use f ra Ð bs to denote the function f 1 such that f 1 paq " b and f 1 pa 1 q " f pa 1 q if a 1 ‰ a.

A (directed) graph is a pair G " xV, Ey where V is a finite set of vertices and E Ď V ˆV is the set of edges. Two graphs G 1 " xV 1 , E 1 y and G 2 " xV 2 , E 2 y are said to be disjoint iff V 1 X V 2 " H. For vertices u, v P V , we use u ; G v to denote that xu, vy P E, use ;G to denote the reflexive transitive closure of ; G , and use ;G to denote the transitive closure of ; G . A path in G is a finite sequence π " v 1 v 2 ¨¨¨v k where v i ; G v i`1 for all i : 1 ď i ă k. We define first pπq :" v 1 and last pπq :" v k . Notice that u ;G v iff there is a finite path in G with first pπq " u and last pπq " v. For a vertex v P V , we define succ G pvq :" tu| v ; G uu to be its set of successor vertices, and define pred G pvq :" tu| u ; G vu to be its set of predecessor vertices. For a graph G " xV, Ey, we define its transpose G Transp :" @ V, E Transp D , where E Transp :" txv, uy| xu, vy P Eu. In other words G Transp is G with all edges reversed. We say that G is a Dag if there are no cycles in G, i.e., there are no vertices v P V with v ;G v. Fix a Dag G " xV, Ey. We define #G :"

| tv P V | |succ G pvq | ą 1u |.
In other words, it is the number of vertices in the graph whose set of successors contains more than one element. For a vertex v P V , we define height G pvq :" 0 if succ G pvq " H, and define height G pvq :" 1 `max uPsucc Gp vq pheight G puqq otherwise. We define height pGq :" max vPV height G pvq, i.e., it is the length of a longest path in G. We define depth G pvq :" 0 if pred G pvq " H, and define depth G pvq :" 1 `max uPpred G pvq pdepth G puqq otherwise. We define depth pGq :" max vPV depth G pvq. A leaf of G is a vertex v P V with height zero, i.e., succ G pvq " H. We use leaves pGq to denote the set of leaves of G. A forest is a Dag such that for all distinct pairs of vertices v, u P V we have succ G pvq X succ G puq " H. A tree is a forest such that | tv| pred G pvq " Hu | " 1. We say that G is an inverted forest/tree if G Transp is a forest/tree. The root of an inverted tree G is the unique vertex v with succ G pvq " H. Notice that a Dag G is an inverted forest iff #G " 0, i.e., it does not contain any vertices with multiple successors.

Directed Acyclic Ad-Hoc Networks

A Directed Acyclic Ad-Hoc Network (Daahn) contains a finite (but arbitrary) number of nodes that are organized in a Dag. The vertices of the Dag represent individual processes, while the Dag models the topology of the network. The processes are modeled as finite-state automata that can perform both local and synchronized broadcast transitions. The successors of a vertex are the set of processes that are able to "hear" broadcast messages issued by the vertex. Depending on its local state, a successor may participate in the broadcast transition or not. Below, we describe the syntax and the operational semantics of a Daahn, and then define two decision problems for the model related to reachability properties.

Syntax. An Ad-Hoc Network (Ahn) consists of a pair N " xP, Gy where P is a finite-state automaton describing the behavior of each process, and G " xV, Ey is the communication graph between the processes. A process P is a tuple xQ, Σ, ∆, q init y where Q is a finite set of states, Σ is a finite message alphabet, q init P Q is the initial state, and ∆ Ď Q ptτ u Y tb pmq| m P Σu Y tr pmq| m P Σuq ˆQ is the transition relation. Intuitively, τ represents a local (internal) transition of the process. The operation b pmq corresponds to broadcasting a message m, while r pmq corresponds to receiving the message m. We say that N is a Daahn if G is a Dag.

Operational Semantics. We give the operational semantics by defining the transition system induced by N . A configuration c of N is a function c : V Þ Ñ Q that defines, for each vertex v P V (i.e., a process position), a state q P Q. We use q P c to denote that there exists a vertex v P V such that cpvq " q. We use C to denote the set of configurations of N , and define the initial configuration c init such that c init pvq " q init for all v P V . We define a transition relation ÑN on the set C by ÑN :"

Ť tP∆ t
Ñ, where t Ñ describes the effect of performing the transition t. Given two configurations c, c 1 P C, we have c t ÑN c 1 if one of the following conditions holds:

-Local transition. There is a v P V such that t " xcpvq, τ, c 1 pvqy P ∆ and for every v 1 P V z tvu, we have that c 1 pv 1 q " cpv 1 q. A local transition modifies only the state of the involved process. -Broadcast. There are v P V and m P Σ such that t " xcpvq, b pmq , c 1 pvqy P ∆, and for every v 1 P V ztvu one of the following conditions holds: ' v ; G v 1 and xcpv 1 q, r pmq , c 1 pv 1 qy P ∆. ' v ; G v 1 , xcpv 1 q, r pmq , qy R ∆ for any q P Q, and c 1 pv 1 q " cpv 1 q. ' v ; G v 1 and c 1 pv 1 q " cpv 1 q. In a broadcast transition, any successor of the sender process that can receive the message m is obliged to participate in the transition.

For both types of transitions, the topology of the system is not affected. We use ÑN to denote the reflexive transitive closure of ÑN . A (finite) run ρ of N is a sequence c 0 c 1 . . . c n of configurations such that c 0 " c init and c i ÑN c i`1 for i : 0 ď i ă n. We use last pρq to denote c n . A configuration c is said to be reachable in N if there is a run ρ of N such that last pρq " c (notice that this is equivalent to c init ÑN c). A state q P Q is said to be reachable in N if q P c for some reachable configuration c.

Decision Problems. The state reachability problem or coverability problem

Cover is defined by a process P " xQ, Σ, ∆, q init y and a state target P Q. The task is to check whether there is a Dag G such that target is reachable in the Daahn N " xP, Gy. The bounded state reachability problem Bounded-Cover is defined by a process P " xQ, Σ, ∆, q init y, a state target P Q, and a natural number k P N. The task is to check whether there is a Dag G with height pGq ď k such that target is reachable in the Daahn N " xP, Gy.

Transducers

We recall the standard definition of transducers and an undecidable problem for them. A (finite-state) automaton is a tuple A " xQ, Σ, ∆, q init , Q final y where Q is a finite set of states, Σ is a finite alphabet, q init P Q is the initial state, Q final Ď Q is the set of final states, and ∆ Ď Q ˆΣ ˆQ is the transition relation. We define the language L pAq of A as usual. A (finite-state) transducer T " xQ, Σ, ∆, q init , Q final y is of the same form as a finite-state automaton except that ∆ Ď Q ˆΣ ˆΣ ˆQ. Thus, a member of L pT q is a word of pairs over Σ, i.e., a member of `Σ2 ˘˚. A transducer T induces a binary relation R pT q on the set Σ ˚such that xa 1 ¨¨¨a n , b 1 ¨¨¨b n y P R pT q if xa 1 , b 1 y ¨¨¨xa n , b n y P L pT q. For a word w P Σ ˚, we define T pwq :" tv| xw, vy P R pT qu. For a set W of words, we define T pW q :" Y wPW T pwq. Given an automaton A and a transducer T (with identical alphabets Σ) we define T pAq :" T pL pAqq. For a natural number i P N and a word w P Σ ˚, we define T i pwq inductively by T 0 pwq :" twu and T i`1 pwq :" T pT i pwqq. In other words, it is the result of i applications of the relation induced by T on w. We extend the definition of T i to sets of words in the expected manner. For an automaton A, we define T i pAq :" T i pL pAqq.

An instance of the problem Transd consists of two automata A and B, and a transducer T , all with identical alphabets Σ. The task is to check whether there is an i P N such that T i pAq X L pBq ‰ H. It is straightforward to show undecidability of Transd through a reduction from a certain non-trivial problem for Turing machines, namely whether a given Turing machine M will eventually print a given symbol a on its tape. More precisely, we use L pAq to describe an appropriate encoding of (i) an empty tape of M , and (ii) the initial position of its head on the tape. The transducer T encodes one move of M , by nondeterministically guessing the position of the head, and then (i) moving the head, (ii) changing one symbol on the tape, and (iii) changing its state, according to the transition relation of M . Finally, the automaton B accepts all words that contains the symbol a.

Undecidability of Cover

In this section, we prove the following theorem.

Theorem 1. Cover is undecidable.

We show undecidability through a reduction from Transd to Cover. Consider an instance of Transd defined by automata A "

A Q A , Σ A , ∆ A , q A init , Q A final E and B " A Q B , Σ B , ∆ B , q B init , Q B final E
, and transducer T "

A Q T , Σ T , ∆ T , q T init , Q T final E (with Σ A " Σ B " Σ T ).
We define a process P " xQ, Σ, ∆, q init y and a state q accept P Q such that there is a Dag G with q accept reachable in the Daahn N " xP, Gy iff there is an i P N such that T i pAq X L pBq ‰ H. The manner in which we define process P (see below) will allow it to simulate both automata A and B and transducer T . The set Q of states of P is defined to be the union of four disjoint sets Q :" tq init , q error , q accept u Y S A Y S B Y S T described below. The idea of the simulation is that a group of processes in N tries to build a "chain" (of some size, say i), where the root of the chain simulates A, the pi ´2q processes in the middle of the chain simulate T , and the last process simulates B. We will refer to such a chain as transduction chain below.

Simulating A. The states in S A are used by P to simulate the automaton A. Each state q P Q A in A has a copy rqs A in S A . At state q init , the process P may decide to simulate the automaton A (Figure 1), thus becoming the first vertex in a potential transduction chain. It does this by performing the transition @ q init , b pA start q , " q A init ‰ A D P ∆ in which it moves to (the copy of) of the initial state of A. At the same time, it issues a broadcast message b pA start q to notify its successor processes in G that it has started the simulation of A. For each transition xq 1 , a, q 2 y P ∆ A in A there is a transition xrq 1 s A , b paq , rq 2 s A y P ∆ in which P simulates changing of states in A and broadcasts the symbol a to its successors. Finally, for each final state q P Q A final , there is a transition @ rqs A , b pm end q , q A end D P ∆ in which P declares that it has ended the simulation of A (by broadcasting the message m end ), after which P stops (there are no outgoing transition from q A end ). Thus, in this mode, the process P broadcasts a sequence of messages corresponding to a word in L pAq followed by the end-marker m end .

qinit qtmp Original: Encoding:

" q T init ı T " q A init ı A " q B init ı B . . . . . . . . . b pAstart q r pAstart q , r pTstart q r pAstart q , r pTstart q b pTstart q SA ST SB
q1 q2 a rq1s A rq2s A q A end b paq b pmend q q1 q2 a rq1s B rq2s B qaccept r paq r pmend q q1 q2 t : a1{a2 rq1s T rq1s t T rq2s T rq2s end T q T end r pa1q b pa2q r pmend q b pmend q Fig. 2

. Transition and accepting state encoding

Simulating T . The states in S T are used by P to simulate the transducer T . Each state q P Q T in T has several corresponding states in S T . More precisely, it has one copy rqs T (as in the case of A above); together with one temporary state rqs t T for each transition t " xq, a 1 , a 2 , q 1 y P ∆ T , i.e., for each transition whose source state is q. At state q init , if the process P receives a message A start or T start from one of its predecessors, then it may decide to simulate the transducer T (Figure 1). It does so by (i) first performing one of the transitions xq init , r pA start q , q tmp y P ∆ and xq init , r pT start q , q tmp y P ∆, where q tmp P S T is a temporary state, followed by (ii) performing the transition @ q tmp , b pT start q , " q T init ‰ T D P ∆ in which it moves to the first copy of the initial state of T . At the same time, it issues a broadcast message b pT start q to its successors declaring that it has started the simulation of T . Intuitively, if P has received A start , it will be the second process in a transduction chain (its predecessor will be the first since it simulates A), while if it has received T start , it will be the pk `1q-th process in the chain (its predecessor will be the k-th process and the predecessor also simulates T ). For each transition t " xq 1 , a 1 , a 2 , q 2 y P ∆ T in T there are two transitions

A rq 1 s T , r pa 1 q , rq 1 s t T E P ∆ and A rq 1 s t T , b pa 2 q , rq 2 s T E P ∆.
Here, P receives the message a 1 from its predecessor (in the chain), and sends a 2 to its successors. Although, a node may have several predecessors, only one of them is allowed to act as the predecessor of the current node in the chain. This is ensured by transitions xq, r pA start q , q error y P ∆ and xq, r pT start q , q error y P ∆ for each q P S T . In other words, if the current process has already received a message from one predecessor (and thus moved to a state in S T ) then it moves to the state q error if it later receives messages from any of its other predecessors. The process P then immediately suspends the simulation (there are no outgoing transition from q error ). Also, the process is not allowed to be "disturbed" by its predecessor while it is in the temporary state q tmp or in one of the temporary states of the form rqs t T . This is due to the fact that the process in such a temporary state has not yet had time to perform the next broadcast, and therefore it is not yet ready to receive the next message form the predecessor (if this is not done, such a message will be lost in the simulation). To encode this, we add extra transitions xq, r paq , q error y for each temporary state q and each message a. Also, in order to discard any sequence of received messages that do not correspond to a valid T input word, we add in ∆ the transition xrqs T , r paq , q error y for every state q of Q T and for every message a P Σ T such that there is no q 1 P Q T such that xq, a, q 1 y P ∆ T . Finally, for each final state q P Q T final , there is a transition is a temporary state). If the process happens to be in a final state, and it receives the end-marker from its predecessor in the chain, then it ends its simulation by notifying its successor and moving to the state q T end . Thus, in this mode, the process P receives a word w from its predecessor and sends a word in T pwq to its successor.

A rqs T ,
Simulating B. The states in S B are used by P to simulate the automaton B. Each state q P Q B in B has a copy rqs B in S B . At state q init , if the process P receives a message A start or T start from one of its predecessors, then it may decide to simulate the automaton B (Figure 1). It does so by performing one of the transitions @ q init , r pA start q , " q B init ‰ B D P ∆ and @ q init , r pT start q , " q B init ‰ B D P ∆. In either case, it moves to the (copy of) the initial state of B. For each transition xq 1 , a, q 2 y P ∆ B in B there is a transition xrq 1 s B , r paq , rq 2 s B y in which P simulates the changing of states in B and receives the symbol a from its predecessor. In a similar manner to the case of T , we also add transitions xq, r pA start q , q error y P ∆ and xq, r pT start q , q error y P ∆ for each q P S B , and xrqs B , r paq , q error y P ∆ for every state q of B and for every message a P Σ B such that there is no q 1 P Q B such that xq, a, q 1 y P ∆ B . Finally, for each final state q P Q B final , there is a transition xrqs B , r pm end q , q accept y P ∆ in which P ends the simulation of B. Thus, in this mode, the process P receives a sequence of messages corresponding to a word in L pBq followed by the end-marker m end . In such a case, the process moves to the state q accept which means that the given instance of Cover has a positive solution.

Correctness. We show correctness of our reduction. Suppose that the given instance of Transd has a positive answer, i.e., there is an i P N and a word w P L pAq such that T i pwq P L pBq. We show that there is a Dag G such that q accept is reachable in the Daahn N " xG, P y, where P is defined as described above. We define G :" xtv 1 , v 2 , . . . , v i`2 u , Ey, where v j ; G v k iff 1 ď j ď i `1 and k " j `1. In other words, the graph forms a chain with i `2 nodes. The process at node 1 starts simulating A eventually broadcasting the word w followed by m end . The process at node 2 starts simulating T receiving the word w symbol by symbol, and eventually broadcasting the word T pwq followed by m end . In general, the process at node j for j : 2 ď j ď i `1 starts simulating T receiving the word T j´2 pwq symbol by symbol, and eventually broadcasting the word T j´1 pwq followed by m end . Finally, the process at node i `2 starts simulating B receiving the word T i pwq symbol by symbol, and eventually moving to the state q accept . Suppose that the given instance of Cover has a positive answer, i.e., there is a Dag G such that q accept is reachable in the Daahn N " xG, P y. We show that there is an i P N and a word w P L pAq such that T i pwq P L pBq. We do this by extracting a transduction chain. We extract the chain vertex by vertex starting by identifying the process that simulates B, then identifying the ones that simulate T , and finally identifying the one that simulates A. Recall that q accept can only be reached in a process that is simulating B. Recall also that such a process can reach q accept if it receives the end-marker from a predecessor process. On the other hand, it cannot receive start messages from two different predecessors before it reaches q accept since this would mean that it would move to the error state q error from which it cannot reach q accept . This implies that the current process has a unique predecessor. Recall that the predecessor, a sending process, must be either a process simulating A or T . If the predecessor is simulating A then we can close the chain, otherwise we have found the next transducer. In the latter case, we repeat the reasoning and find the predecessor again. Let j be the length of the chain obtained in this manner (j ě 2 since it contains at least two vertices simulating A resp. B). Define i in the instance of Transd to be j ´2.

Forest Bounded Coverability

In this section, we show that the bounded coverability problem can be reduced from the general case of Dags to the case where we assume the Dag to be an inverted tree. We do that in two steps, namely by first reducing the problem to the case of inverted forests and then to trees.

Forests. A Daahn N is said to be an inverted forest if the underlying graph is an inverted forest. We consider a restricted version of Bounded-Cover, which we call Forest-Bounded-Cover. In Forest-Bounded-Cover, we require that the given Daahn is an inverted forest. We show the following theorem.

Theorem 2. Bounded-Cover is reducible to Forest-Bounded-Cover.

In order to prove this theorem, we first introduce a split operator over Dags. We define an inverted forest G ' :" xV ' , E ' y as follows. Each vertex v P V induces a set v ' in V ' . A member of v ' is an inverted path π in G with first pπq P leaves pGq and last pπq " v.

The set v ' is defined using induction on the height of v as follows. If height G pvq " 0 (i.e., v is a leaf) then v ' :" tvu. Otherwise, v ' :" tπ ¨v| Du. v ; G u ^π P u ' u.

In other words, we split v into a number of copies, each corresponding to a path starting from a successor of v and ending in a leaf in G. We define E ' :" txπ 1 , π 2 y| π 1 " π 2 ¨vu. Notice that height G ' puq " height G pvq for every v P V and u P v ' . Therefore, height pG ' q " height pGq. Furthermore, by definition, any vertex in G ' has at most one successor (no successors if it is of the form v P V , or the unique successor π if is of the form π ¨v). This means that G ' is an inverted forest.

Consider an instance of Bounded-Cover defined by P " xQ, Σ, ∆, q init y, a state target P Q, and a natural number k P N. We claim that the instance of Forest-Bounded-Cover defined by P " xQ, Σ, ∆, q init y, target, and k is equivalent. For a configuration c in N " xP, Gy, we define c ' to be the configuration of N ' " xP, G ' y such that c ' pπ ¨vq " cpvq. The following lemma shows that reachability is preserved by splitting.

Lemma 3. If c 1 ÑN c 2 then c ' 1 ÑN ' c ' 2 .
From Lemma 3 and the fact that c init ' pπ ¨vq " c init pvq " q init , we conclude the following:

Lemma 4. If c is reachable in N then c ' is reachable in N ' .
Now, we are ready to prove Theorem 2. If the given instance of Forest-Bounded-Cover has a positive answer, then the instance of Bounded-Cover has trivially a positive answer (each inverted forest is a Daahn). For the opposite direction, suppose that the instance of Bounded-Cover has a positive answer, i.e., there is a Dag G with height pGq ď k such that target is reachable in the Daahn N " xP, Gy. By Lemma 4, we know that target is reachable in xP, G ' y. The result then follows since G ' is an inverted forest and since height pG ' q " height pGq ď k.

Trees. We consider a yet more restricted version of Bounded-Cover, which we call Tree-Bounded-Cover. In Tree-Bounded-Cover, we require that the given Daahn is an inverted tree.

Theorem 5. Forest-Bounded-Cover is reducible to Tree-Bounded-Cover.

The proof of Theorem 5 is straightforward. Since the nodes inside the tree of a forest do not affect transitions of the nodes inside the other trees, we can solve Tree-Bounded-Cover for each tree separately. The given instance of Forest-Bounded-Cover has a positive answer iff Tree-Bounded-Cover has a positive answer for any of the component trees.

Tree Bounded Coverability

In this section, we prove the following theorem. Theorem 6. Tree-Bounded-Cover is decidable.

We devote the section to the proof of Theorem 6. To do that, we instantiate the framework of well quasi-ordered transition systems introduced in [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF]. The main ingredient of this framework is to show that the transition relation induced by the system is monotonic wrt. a well quasi-ordering (wqo) on the set of configurations. We define an ordering that we denote by Ď on configurations that are inverted trees and show monotonicity of the system behavior wrt. this ordering. Unfortunately, it is not possible to apply existing frameworks (such as the one in [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF]) to directly prove the wqo of Ď on inverted trees. Therefore, we introduce a new ordering that we denote by Ď 2 on a set of "higher-order multisets". We show that the ordering on higher-order multisets Ď 2 is indeed a wqo and that it is equivalent to the original ordering Ď on inverted trees, which proves that Ď is itself a wqo. Then, we recall the basic concepts of the framework of well quasi-ordered systems, and show how the framework can be instantiated to prove Theorem 6.

Ordering

Assume a process P " xQ, Σ, ∆, q init y. An extended configuration is a pair e " xG, cy where G is an inverted tree, and c is a configuration of the Daahn xG, P y.

We use E to denote the set of extended configurations, and, for k ě 1, we use E k to denote the set of extended configurations xG, cy where the inverted tree G is of height at most k. We define an ordering on E as follows. Consider extended configurations e " xG, cy with G " xV, Ey and e 1 " xG 1 , c 1 y with G 1 " xV 1 , E 1 y. For an injection α : V Þ Ñ V 1 , we use e Ď α e 1 to denote that the following two conditions hold for all v P V : (i) cpvq " c 1 pαpvqq, and (ii) If u ; G v then αpuq ; G 1 αpvq. We write e 1 Ď e 2 if e Ď α e 1 for some α. Intuitively, we can view an extended configuration as an inverted tree that is unranked (a node may have any number of predecessors) and unordered (the order in which the predecessors occur is not relevant). The ordering e 1 Ď e 2 then means that the inverted tree corresponding to e 1 has a copy (an image) inside the inverted tree corresponding to e 2 . In Figure 3, three extended configurations are depicted as inverted trees e 1 , e 2 , e 3 . Here e 1 Ď e 2 Ď e 3 .

Monotonicity

Given a process P , we define a transition relation ÝÑ on E where xG, cy ÝÑ xG 1 , c 1 y if G 1 " G, N " xP, Gy, and c ÑN c 1 . The following lemma shows monotonicity of ÝÑ wrt. Ď. Assume that e 1 , e 2 , e 3 are extended configurations. Lemma 7. If e 1 ÝÑ e 2 and e 1 Ď e 3 then there is an e 4 such that e 3 ÝÑ e 4 and e 2 Ď e 4 .

Higher-Order Multisets

For a finite set A and k ě 0, we define the set A bk inductively as follows: (i) A b0 :" A; and (ii) A bk`1 :" A bk Y ´A ˆ`A bk ˘b¯.

In other words, a higher-order multiset of order 0 is an element in A, while a multiset of order k `1 is either a multiset of order k, or a pair consisting of an element in A together with a multiset of multisets of order k. Intuitively, a higher-order multiset defines an inverted tree (corresponding to an extended configuration). More precisely, a higher-order multiset of the form a represents an inverted tree consisting of a single node (labeled by a), while the higher-order multiset xa, rB 1 , . . . , B k sy represents an inverted tree with a root labeled a, and where predecessors of the root are themselves the roots of the inverted subtrees represented by B 1 , . . . , B k respectively (see Figure 3). We define an ordering Ď 2 on A bk in two steps. First, we define an ordering Ď 1 on A bk such that a Ď 1 a 1 if a " a 1 ; and a Ď 1 xa 1 , By if a " a 1 .

xa, rB 1 , . . . , B k sy Ď 1 xa 1 , rB 1 1 , . . . , B 1 sy if a " a 1 and there is an injection h : t1, . . . , ku Þ Ñ t1, . . . , u with B i Ď 1 B 1 hpiq for all i : 1 ď i ď k. Notice that the second condition is equivalent to rB 1 , . . . , B k sĎ b 1 rB 1 1 , . . . , B 1 s. Intuitively, B 1 Ď 1 B 2 means that a copy of the inverted tree corresponding to B 1 occurs in the inverted tree corresponding to B 2 starting from the root. For instance, consider B 1 , B 2 , B 3 in Figure 3. According to the definition of Ď 1 , we have B 1 Ď 1 B 2 while B 1 Ď 1 B 3 . This is reflected in the inverted trees corresponding to the extended configurations e 1 , e 2 , e 3 . Although copies of e 1 occurs both in e 2 and e 3 , the copy of e 1 does not start from the root of e 3 . Now, we define Ď 2 as follows.

a Ď 2 a 1 if a " a 1 ; and a Ď 2 xa 1 , By if a " a 1 or a Ď 2 B.

xa, rB 1 , . . . , B k sy Ď 2 xa 1 , rB 1 1 , . . . , B 1 sy if one of the following two cases is satisfied:

' a " a 1 and there is an injection h : t1, . . . , ku Þ Ñ t1, . . . , u with

B i Ď 1 B 1 hpiq for all i : 1 ď i ď k. ' xa, rB 1 , . . . , B k sy Ď 2 B 1 i for some i : 1 ď i ď . Notice that Ď 1 ĎĎ 2 . Intuitively, B 1 Ď 2 B 2
means that a copy of the inverted tree corresponding to e 1 occur somewhere in the inverted tree corresponding to B 2 (not necessarily starting from the root). In Figure 3, B 1 Ď 2 B 3 (and a copy of e 1 occurs in e 3 ).

Encoding

We define an encoding function # that translates each extended configuration to a higher-order multiset. Formally, consider an extended configuration xG, cy with G " xV, Ey. First, we define # pv, cq, for v P V , by induction on depth G pvq as follows:

-If depth G pvq " 0 then # pv, cq :" cpvq. In this case, the encoding is of order 0 (given by the state of the vertex).

-If depth G pvq ą 0 then let pred G pvq " tv 1 , . . . , v n u. Then, # pv, cq :" xcpvq, r# pv 1 , cq , . . . , # pv n , cqsy. The encoding is of the same order as the depth of the vertex; it consists of the state of the vertex itself together with the multiset of the encodings of its predecessors.

We define #e :" # pv, cq where v is the root of G. Notice that the order of #e is identical to the height of the inverted tree G. As an example, in Figure 3, if we view an inverted tree e i , i " 1, 2, 3, as an extended configuration then its encoding is given by B i . The following lemma shows that the orderings on extended configurations and higher-order multisets coincide. Let e 1 and e 2 be two extended configurations.

Lemma 8. e 1 Ď e 2 iff #e 1 Ď 2 #e 2 .

Well Quasi-Orderings

Let A be a set and let Ď be a quasi-ordering on A. We say that Ď is well quasiordering (wqo) if it satisfies the following property: for any infinite sequence a 0 , a 1 , a 2 , . . . of elements in A, there are i ă j with a i Ď a j . We will use the following variant of Higman's Lemma [START_REF] Higman | Ordering by divisibility in abstract algebras[END_REF] for our purposes:

Lemma 9. If Ď is wqo on A then Ď b is a wqo on A b .
Now, we show that the ordering Ď 2 is a wqo on A bk for any given k ě 0. To show Ď 2 is a wqo, we first show that Ď 1 is a wqo on A bk for any given k ě 0. We use induction on k. The base case is trivial since it amounts to equality being a wqo on a finite alphabet. Consider an infinite sequence xa 0 , D 0 y , xa 1 , D 1 y , xa 2 , D 2 y , . . . of elements in A bk`1 (notice that D i P `Abk ˘b). Since a 0 , a 1 , a 2 , . . . all belong to the finite set A, there is an a P A and an infinite sequence i 0 ă i 1 ă ¨¨s uch that a ij " a for all j ě 0. Since Ď 1 is a wqo on A bk by the induction hypothesis, it follows by Lemma 9 that Ď b 1 is a wqo on `Abk ˘b. By definition of wqo, there are i m ă i n with D im Ď b 1 D in . By definition of Ď 1 we have that xa im , D im y Ď 1 xa in , D in y.

We are now ready to show that Ď 2 is a wqo. Consider an infinite sequence as the one above. Since xa im , D im y Ď 1 xa in , D in y and Ď 1 ĎĎ 2 it follows that xa im , D im y Ď 2 xa in , D in y which completes the proof for wqo of Ď 2 .

Lemma 8 implies that, for extended configurations e 1 , e 2 , we have that e 1 Ď e 2 iff #e 1 Ď 2 #e 2 . Also, recall that, for e " xG, cy the height of G is equal to the order of #e. From this and the fact that Ď 2 is a wqo on A bk for any given k ě 1, we get the following lemma. Lemma 10. For any k ě 1, the ordering Ď is a wqo on E k .

Monotonic Transition Systems

A monotonic transition system (MTS) is a tuple xΓ, Γ init , Ď, ÝÑ, U y, where -Γ is a (potentially infinite) set of configurations.

-Γ init Ď Γ is a set of initial configurations.

-Ď is a computable ordering on Γ , i.e., for each γ 1 , γ 2 P Γ , we can check whether γ 1 Ď γ 2 . Furthermore, Ď is a wqo. -ÝÑ is a binary transition relation on Γ . Furthermore, ÝÑ is monotonic with respect to Ď, i.e., given configurations γ 1 , γ 2 , γ 3 such that γ 1 ÝÑ γ 2 and γ 1 Ď γ 3 , there is a configuration γ 4 such that γ 3 ÝÑ γ 4 and γ

2 Ď γ 4 . -U is defined as the upward closure Γ 1 Ò of a finite set Γ 1 Ď Γ , where Γ 1 Ò" tγ 1 P Γ | Dγ P Γ 1 . γ Ď γ 1 u.
We use Ñ to denote the reflexive transitive closure of ÝÑ. For sets Γ 1 , Γ 2 Ď Γ , we say that Γ 2 is reachable from Γ 1 if there are γ 1 P Γ 1 and γ 2 P Γ 2 such that γ 1 Ñ γ 2 . In the reachability problem MTS-Reach we are given an MTS xΓ, Γ init , Ď, ÝÑ, U y and are asked the question whether U is reachable from Γ init . The paper [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF] gives sufficient conditions for decidability of MTS-Reach as follows. For Γ 1 Ď Γ , we define PrepΓ 1 q :" tγ| Dγ

1 P Γ 1 . γ ÝÑ γ 1 u. For Γ 1 Ď Γ , we say that M Ď Γ 1 is a minor set of Γ 1 if -For each γ 1 P Γ 1 there is γ 2 P M such that γ 2 Ď γ 1 . -If γ 1 , γ 2 P M and γ 1 Ď γ 2 then γ 1 " γ 2 .
Since Ď is a wqo, it follows that each minor set is finite. However, in general, the same set may have several minor sets. We use min to denote a function which, given Γ 1 Ď Γ , returns an arbitrary (but unique) minor set of Γ 1 . We use minprepγq to denote the set minpPreptγu Òqq.

It is shown in [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF] that the following conditions are sufficient for decidability of MTS-Reach.

Theorem 11. MTS-Reach is decidable if for each γ P Γ we can check whether γ P Γ init .

the set minprepγq is finite and computable.

From Tree-Bounded-Cover to MTS-Reach

For a natural number k ě 1, a process P " xQ, Σ, ∆, q init y, and a state target P Q, we derive an MTS xΓ, Γ init , Ď, ÝÑ, U y such that Γ init Ñ U iff there is a Dag G which is an inverted tree with height pGq ď k such that target is reachable in the Daahn N " xP, Gy.

-Γ is the set E k . -Γ init is the set of pairs xG, c init y P E k and c init is the initial configuration of the Daahn xG, P y. -Ď is defined on E k as described above. The ordering Ď is obviously computable. Well quasi-ordering of Ď on Γ is shown in Lemma 10.

-The transition relation ÝÑ on E k is defined as described above. Monotonicity is shown in Lemma 7. -U is defined as the upward closure of the singleton txG 1 , c 1 yu, where G 1 " xtvu , Hy i.e., G 1 contains a single vertex v and no edges, and furthermore c 1 pvq " target. Notice that U characterizes all inverted trees that contain at least one vertex labeled with target.

It is trivial to check whether a given configuration is initial (check whether all vertices are labeled with q init ). The following lemma states that the induced transition system also satisfies the second sufficient condition for decidability (see Theorem 11).

Lemma 12. Consider the MTS defined above. Then, for each extended configuration e we can compute minprepeq as a finite set of extended configurations.

Lemma 12, together with Theorem 11, proves Theorem 6.

Related Work

A fixed, generally small, number of processes has been considered when model checking techniques have been applied to verify ad hoc network protocols [START_REF] Fehnker | Modelling and verification of the LMAC protocol for wireless sensor networks[END_REF][START_REF] Singh | Query-based model checking of ad hoc network protocols[END_REF]. In [START_REF] Saksena | Graph grammar modeling and verification of Ad Hoc Routing Protocols[END_REF] Saksena et al. define a possibly non-terminating symbolic procedure based on graph transformations to verify routing protocols for Ad Hoc Networks. Delzanno et al. showed in [START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF] that the coverability problem is undecidable in the general case of unbounded, possibly cyclic and directed graphs. In particular, the same authors considered in [START_REF] Delzanno | On the power of cliques in the parameterized verification of ad hoc networks[END_REF] the boundeddepth subclass of Ad Hoc Networks. Using the induced sub-graph relation on bounded-depth graphs as a symbolic representation within the well quasiordered transition systems framework, they proved the decidability of the coverability problem. However, this result cannot be used in the context of directed acyclic ad hoc networks because the induced sub-graph relation is not a well quasi-order in the case of the bounded depth acyclic graphs. . . .

In fact, as shown in the figure, the list of directed acyclic labeled graphs of depth 2, g 1 , g 2 , g 3 , . . . is an infinite sequence of extended configurations of incomparable elements.

Conclusions

We have considered parameterized verification of ad hoc networks where the network topology is defined by an acyclic graph. We have considered the coverability problem which, for a given process definition, asks whether there is a graph and a reachable configuration where a process is in a given state. The coverability problem is used to find violations generated by a fixed set of processes independently from the global configuration. The problem turns out to be undecidable in the general case, but decidable under the restriction that the graph is of bounded depth (where the depth is bounded by a given k). Among possible directions for future work is the study of the impact of richer broadcast mechanisms such as those that allow processes to have local (unbounded) mailboxes, and to consider models augmented by timed and probabilistic transitions in order to allow quantitative reasoning about network behaviors.

Fig. 1 .

 1 Fig. 1. Process P : initial choices

r pm end q , rqs

  end q , q T end E P ∆ (where rqs end T

  Dag G " xV, Ey. The split operator splits the nodes of G, transforming it into an inverted forest.

Fig. 3 .

 3 Fig.3. The extended configurations e 1 , e 2 , and e 3 correspond to the higher order multisets B 1 " xa, rb, csy, B 2 " xa, rxb, rasy , d, csy, and B 3 " xd, rxa, rxb, rasy , d, csy , dsy respectively.


Tobias Isenberg
email: isenberg@mail.upb.de

Dominik Steenken
email: dominik@mail.upb.de

Heike Wehrheim
email: wehrheim@mail.upb.de

Bounded Model Checking of Graph Transformation Systems via SMT Solving

Keywords: verification, graph transformation systems, bounded model checking, satisfiablility modulo theories

Bounded model checking (BMC) complements classical model checking by an efficient technique for checking error-freedom of bounded system paths. Usually, BMC approaches reduce the verification problem to propositional satisfiability. With the recent advances in SAT solving, this has proven to be a fast analysis. In this paper we develop a bounded model checking technique for graph transformation systems. Graph transformation systems (GTSs) provide an intuitive, visual way of specifying system models and their structural changes. An analysis of such models -however -remains difficult since GTSs often give rise to infinite state spaces. In our BMC technique we use first-order instead of propositional logic for encoding complex graph structures and rules. Today's off-the-shelf SMT solvers can then readily be employed for satisfiability solving. The encoding heavily employs the concept of uninterpreted function symbols for representing edge labels. We have proven soundness of the encoding and report on experiments with different case studies.

Introduction

Graph transformation systems (GTSs) are an intuitive and powerful way of modeling dynamic systems. They describe the states of a system as graphs and state changes as graph transformation rules. This makes them particularly suitable for modeling structural aspects of systems. GTSs have been applied in diverse areas, such as model transformation and refactorings [START_REF] Bisztray | Verification of architectural refactorings by rule extraction[END_REF], the modeling of dynamic self-adaptive systems [START_REF] Becker | Symbolic invariant verification for systems with dynamic structural adaptation[END_REF] or web services [START_REF] Engels | Assuring consistency of business process models and web services using visual contracts[END_REF]. Some of these application areas are safety critical, raising the need for formal verification of such systems. When modeling these systems using GTSs, the analysis often suffers from the state space explosion problem. A number of approaches aim at fighting this problem, most often using abstraction techniques [START_REF] Rensink | Pattern-based graph abstraction[END_REF][START_REF] Baldan | Summary 2: Graph grammar verification through abstraction[END_REF].

Bounded model checking [START_REF] Biere | Symbolic model checking without BDDs[END_REF] is a technique avoiding the state space explosion problem by focusing on bounded paths. This technique is incomplete, and thus primarily used for finding errors, not for correctness proofs. This idea has been adapted for the verification of GTSs [START_REF] Kastenberg | Graph-based software specification and verification[END_REF][START_REF] Baresi | On the use of Alloy to analyze graph transformation systems[END_REF], however, few of the existing solutions directly utilizes the progress of SAT/SMT solvers seen in the last years. In particular, none of the verification techniques for GTSs have proposed to reduce the complete analysis directly to satisfiability checking. An encoding of GTS in logical formulae is only used in [START_REF] Kreowski | Graph Transformation Units Guided by a SAT Solver[END_REF], which however gives a SAT encoding and uses the result to guide the state space exploration of a (non-SAT) analysis tool for GTS.

In this paper we present a bounded model checking (BMC) technique for GTSs using satisfiability checking of quantifier-free first-order logic with uninterpreted functions (QF UF). We transform the BMC instance over GTSs into a satisfiability modulo theories (SMT) instance encoding only the initial graph and the transformation rules, as well as the property to be checked.

In the present paper, the property will -for simplicity -always be a (forbidden) graph; thus we just aim at checking reachability of error states. Our approach, detailed in [START_REF] Isenberg | Bounded Model Checking für Graphtransformationssysteme als SMT-Problem[END_REF], does however cover more general properties specified in LTL. The generated SMT formula describes bounded-length paths of the GTS that exhibit the forbidden graph. The formula is given to an off-the-shelf SMT solver which checks for satisfiability. A satisfying interpretation represents a violating path and is used to display it.

We have implemented our approach and tested it with a number of SMT solvers (MathSAT [START_REF] Cimatti | The MathSAT5 SMT Solver[END_REF], SMTInterpol [START_REF] Christ | SMTInterpol: An Interpolating SMT Solver[END_REF], veriT [START_REF] Bouton | veriT: An open, trustable and efficient smt-solver[END_REF], Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF]). The performance of the approach heavily depends on the structure of rules (e.g., number of nodes, NACs), and only to a minor extent on the solver. We exemplify our technique on the car platooning case study of the Transformation Tool Contest 2010 [START_REF] Backes | A graph transformation case study for the topology analysis of dynamic communication system[END_REF].

Background

We start by defining Graph Transformation Systems (GTSs) and the reachability problem of a forbidden pattern in this context, while introducing the running example. The definitions are similar to those in [START_REF] Ehrig | Algebraic Approaches to Graph Transformation -Part II: Single Pushout Approach and Comparison with Double Pushout Approach[END_REF][START_REF] Habel | Graph grammars with negative application conditions[END_REF][START_REF] Rensink | The joys of graph transformation[END_REF].

Definition 1 (Graph).

Let L E be a set of edge labels and L N be a set of node labels.

A graph G = (N G , E G , U G ) over L E and L N consists of a set N G of nodes, a set E G ⊆ N G × L E × N G of labeled edges and a set U G ⊆ L N × N G of unary edges labeling the nodes.
A graph is a set of nodes with edges between pairs of them and on individual nodes. These edges are labeled over L E and L N respectively.

For illustration purposes, consider the car platooning GTS specified by Backes and Reineke [START_REF] Backes | A graph transformation case study for the topology analysis of dynamic communication system[END_REF], modeling a protocol for cars to build a platoon, i.e., a connected entity. Initially the cars are unconnected and in the state free agent(fa). During the process of connecting there are several intermediate states, as described by the protocol. However, the final states of a car are leader (ld ) and follower (flw ). A platoon is structured such that there are a number of follower s following one leader . In our example this protocol is modeled as a GTS with an initial graph containing four nodes labeled fa, modeling cars in state free agent(see Figure 1a). Note that we model node labels as "unary" edges, i.e., edges with a target but without a source. Additionally, a GTS has rules that describe possible changes and under which conditions these can be applied. For these transformation rules and their applicability consider the following definitions.

Definition 2. A total graph morphism f : G → G from graph G to graph G is a tuple f = f N , f E , f U of total functions f N : N G → N G , f E : E G → E G and f U : U G → U G satisfying the following conditions: f E (n 1 , l, n 2 ) = (f N (n 1 ) , l, f N (n 2 )) ∀ (n 1 , l, n 2 ) ∈ E G f U (l, n 1 ) = (l, f N (n 1 )) ∀ (l, n 1 ) ∈ U G
A partial graph morphism from graph G to graph G is a total graph morphism of a subgraph S of G to G . A total graph morphism specifies a mapping that maintains the structure. Intuitively speaking, such a morphism exists, if a subgraph similar to G can be found in G . This construct is fundamental for applying graph transformation rules. Such a rule consists of a left hand side graph L and a right hand side graph R, related by a partial graph morphism.

Definition 3 (Transformation Rule and Match).

Let G be a graph, called host graph. A graph transformation rule r = L, R , described by a partial graph morphism r : L → R, is applicable to G, if and only if there exists a total, injective graph morphism m : L → G, called a match.

For simplicity, in the following we assume r = id L∩R (i.e., L and R need not be disjoint, e.g., see the nodes in Figure 2). Intuitively speaking, a match specifies at which location in the graph a rule can be applied. This application itself is done obeying the well known SPO-semantics [START_REF] Ehrig | Algebraic Approaches to Graph Transformation -Part II: Single Pushout Approach and Comparison with Double Pushout Approach[END_REF] explained below.

Let G, r and m be as in Def. 3. We define N del := N L \ N R and N add as a disjoint copy of N R \ N L . By setting m N := m ∪ id N add we extend m onto N add .

The following sets are useful in defining the effect of a rule application.

E del := {(m N (n 1 ) , l, m N (n 2 )) | (n 1 , l, n 2 ) ∈ E L \ E R ∨ n 1 ∈ N del ∨ n 2 ∈ N del } E add := {(m N (n 1 ) , l, m N (n 2 )) | (n 1 , l, n 2 ) ∈ E R \ E L }
Corresponding sets U del and U add for unary edges are defined analogously. Each of these sets contains the objects deleted / added through the rule application. Fig. 2: Rule 1 of the car platooning GTS [START_REF] Backes | A graph transformation case study for the topology analysis of dynamic communication system[END_REF] This gives rise to the following definition.

Definition 4 (Rule Application). Given a host graph G, a graph transformation rule r = L, R and a match m : L → G. The application of r to graph G via the match m, written G r,m =⇒ H, creates a result graph H specified by

N H := N G \m N (N del )∪N add , E H := E G \E del ∪E add , and U H := U G \U del ∪U add .
The resulting graph is constructed such that the images (w.r.t. the match) of the nodes and edges of the LHS, which are not part of the RHS have to be deleted. Afterwards, new nodes and edges are added for the ones contained in the RHS and not in the LHS. All dangling edges, i.e., edges that are left without a source-or target node after application, are deleted. Definition 5 (GTS). A graph transformation system G = (S, P ) consists of a start graph S and a set P = {r 1 , ..., r n } of graph transformation rules.

The car platooning GTS [START_REF] Backes | A graph transformation case study for the topology analysis of dynamic communication system[END_REF] consists of 14 rules. For simplicity we will only present the encoding of two of them (Rules 1 and 13 ) illustrated in the next section (see Figures 2,3). The LHS of Rule 1 requires two distinct nodes in the host graph, one of which is labeled fa(free agent) and changes its state to hon(hand over nothing). Additionally, two edges are added as shown in Fig. 2. This rule models the initialization of a connection started by a free agent car.

For Rule 13, we will need an extension of the above formalism. We need to allow Negative Application Conditions (NACs) within the rules [START_REF] Habel | Graph grammars with negative application conditions[END_REF]. A NAC constrains the application of a rule, s.t. it is only applicable if the structures described by the NAC are not present in the host graph. Fig. 3: Rule 13 of the car platooning GTS [START_REF] Backes | A graph transformation case study for the topology analysis of dynamic communication system[END_REF] l : L → L be such a morphism and let m be a match of r to G. The application of r with match m to the host graph G is allowed w.r.t. l, if and only if no match n : L → G exists with n • l = m (concatenation operator •). A NAC allows the application of r with match m to the host graph G, if and only if the application is allowed w.r.t. all total graph morphisms of the NAC.

For simplicity, in the following we assume l to be an embedding, i.e., L ⊂ L. Rule 13 (Figure 3) contains a NAC. It states that the match of the node n 1 must not have a flws-labeled edge to any other node. When two platoons join, one leader hands over all his followers to the other leader. While having at least one follower left, he is not allowed to proceed to the next step of the protocol, but must finish the handover first. This is modeled by the NAC in Rule 13. Thus, car n 1 must not have a follower, when changing its state from hand over back to hand over done. With this understanding of the application of rules, we define the paths of a GTS and the reachability problem. Definition 7. Given a GTS G = (S, P ). A state of the GTS is a graph. Thus, a path G 0 , G 1 , ... of G is a finite or infinite sequence of graphs starting with the initial graph (G 0 = S) such that we have G i ri,mi =⇒ G i+1 for all consecutive graphs G i ,G i+1 . The state space of a GTS is the union of all of its paths, joined at isomorphic graphs.

While usually, GTSs do not distinguish between isomorphic graphs, our encoding does not have that capability. Thus, each isomorphic instance of a graph is explored separately. In the following we state the reachability problem. Definition 8. Given a GTS G and a graph F , called the forbidden pattern. The pattern is reachable, if there exists a finite path G 0 , ..., G k of G, such that F matches G k .

Intuitively speaking, reachability means the existence of a path containing a graph in which the forbidden pattern can be found. Within the car platooning protocol [START_REF] Backes | A graph transformation case study for the topology analysis of dynamic communication system[END_REF], no follower should ever follow a follower. This can be expressed as a forbidden pattern (see Figure 1b). If that pattern would be reachable, the model of the protocol would not meet the desired behavior.

We propose a BMC technique to check reachability of such a forbidden graph. Our approach directly encodes the initial graph, the transformation rules and the forbidden pattern as a satisfiability modulo theories (SMT) instance. SMT describes the problem of searching for a satisfying interpretation of a first-order logic formula with a background theory. Intuitively, a theory can be seen as constraints on the possible interpretations, as it describes a priori interpretations of functions. Our formulae use the theory of uninterpreted functions with equality, i.e., only the equality sign has an a priori interpretation. This approach relocates the computational complexity of exploring the bounded state space into solving an SMT formula, which can be a reasonable trade-off, as current research continuously improves efficiency of SMT solvers (SMT-COMP [START_REF] Barrett | 6 Years of SMT-COMP[END_REF]).

The technique presented here is subject to several restrictions, which we summarize here for clarity.

1. we only allow simple, labeled graphs (no multigraphs, no hypergraphs) 2. we disallow node merging 3. we disallow non-injective matches 4. we only support reachability analysis Restrictions 3 and 4 are removed in our full technique, detailed in [START_REF] Isenberg | Bounded Model Checking für Graphtransformationssysteme als SMT-Problem[END_REF]. In the following, we will only give the definitions required for the restricted version.

Encoding of GTSs in first-order logic

In the following we describe our BMC technique, which encodes bounded paths of a GTS (S, P ) as an SMT formula to check the reachability of a forbidden pattern in the bounded state space. The concept of BMC via SAT-solving was originally introduced in 1999 [START_REF] Biere | Symbolic model checking without BDDs[END_REF]. In hardware verification it is a natural choice to represent circuits as boolean formulas. This idea was then extended to check error freedom of a bounded subset of the state space. The state space is only examined up to a predefined number k of steps, called the bound. The initial state, k transitions and the error are encoded as a boolean formula, that is satisfiable if the error exists within the bounded state space.

Our approach likewise encodes the start graph, k transitions and a forbidden pattern (or LTL formula). A transition in this context denotes the application of one of the graph transformation rules of the GTS.

Let S be the encoding of the initial graph S = G 0 and T 1 to T k be the encodings of the k transition steps. The complete formula is defined as S ∧ T 1 ∧...∧ T k ∧ F with F being the encoding of the forbidden pattern.

Below we describe the process in detail. Let L E be the set of all edge labels occurring in the initial graph, the rules or the forbidden pattern and let L N be the set of all node labels, respectively. For representing all edges with label l ∈ L E of a graph G i (i ∈ {0, ..., k}) along the path G 0 , ..., G k we use binary predicates l i . For tagging the nodes with label l ∈ L N we use unary predicates, respectively. Let U be the universe consisting of the nodes of the initial graph. Unary predicates have domain U, binary ones have domain U × U.

Definition 9. Let L E,i = {l i |l ∈ L E } and L N,i = {l i |l ∈ L N }
be the sets of binary and unary predicates with index i. An i-interpretation I i assigns a total function with image true or f alse to every such predicate. Formally, I i :

-L E,i → {U × U → {true, f alse}} -L N,i → {U → {true, f alse}}. An i-interpretation I i represents a graph G i (written I i (G i )), iff: -∀l ∈ L E ∀n 1 , n 2 ∈ N Gi : I i (l i )(n 1 , n 2 ) = true ⇔ (n 1 , l, n 2 ) ∈ E Gi -∀l ∈ L N ∀n ∈ N Gi : I i (l i )(n) = true ⇔ (l, n) ∈ U Gi .
This idea of how a satisfying interpretation represents a graph is used throughout the complete encoding process.

Encoding of the initial graph. Given the initial graph S = G 0 = (N G0 , E G0 , U G0 ), we encode each edge (n 1 , l, n 2 ) ∈ E G0 with a positive literal l 0 (n 1 , n 2 ) and each nonexistent edge (n 1 , l, n 2 ) ∈ (U × L E × U) \ E G0 with a negated literal ¬l 0 (n 1 , n 2 ). Unary edges are handled analogously. Furthermore, we include literals ¬ (n i = n j ) for all pairings of distinct nodes n i , n j . This ensures that the graph itself and not a smaller graph it would be homomorphic to is encoded, and provides support for isolated nodes. These literals are combined via conjunction. Example 1. Our example GTS has an initial graph as shown in Figure 1a and two transformation rules. These can be seen in Figures 2 and3. The sets of labels in the example GTS are L E = {flws, ldr , req} and L N = {fa, hob, hod , hon, flw }. U consists of the nodes from the start graph, called n 1 to n 4 . The encoding of the initial graph is straightforward as there are no binary edges in the initial graph and the nodes are only labeled with fa:

G 0 = 4 i=1 fa 0 (n i ) ∧ l∈L N l =f a 4 i=1 ¬l 0 (n i ) ∧ 4 i=1 j=1 l∈L E ¬l 0 (n i , n j ) ∧ 4 i=1 j=1 i =j ¬ (n i = n j )
The following lemma states the correctness of this encoding.

Lemma 1. Given a graph G, G is satisfiable only with I 0 (G) representing G.

Encoding of a transition. The i-th transition (i ∈ {1, ..., k}) can be caused by the application of any of the graph transformation rules to the host graph G i-1 .

For a GTS with the set P = {r 1 , ..., r n } of rules, the i-th transition is encoded as

T i = r 1 i ∨ ... ∨ r n i with r i = r Cond i ∧ r App i
. Thus, we have to encode the applicability and the application of each rule for each transition step.

Encoding r Cond i of the applicability of a transformation rule r. We first encode the check whether a rule is applicable to a host graph G j (Note that j = i -1 for the i-th transition). For each node n ∈ N L create a variable m j n , to which we want the SMT-Solver to assign a node from the universe U. In general, SMT uses sorts with an unbounded number of members. Thus, we have to assure that only nodes out of U are used. We do this with the disjunction (m j n = n 1 ) ∨ ... ∨ (m j n = n 2 ) for U = {n 1 , ..., n 2 }. The assignment of the variables to the actual nodes in the universe represents the match. Since the match must be injective, for each two distinct nodes n 1 , n 2 ∈ N L the literal ¬ m j n1 = m j n2 is added. In addition, each edge (n 1 , l, n 2 ) ∈ E L of the LHS has to exist within the matched nodes of G j . This is encoded by the literal l j m j n1 , m j n2 . The analog holds true for the unary edges. Thus, we encode a unary edge (l, n 1 ) ∈ U L by a literal l j m j n1 . All these literals are combined via conjunction.

Encoding of a NAC. If the transformation rule has Negative Application Conditions, these are encoded and added to the conjunction as well. Each total graph morphism of the NAC is encoded separately and combined afterwards by conjunction. Given such a morphism L → L, a variable m j n is created for each node n ∈ L \ L. These new variables are bound by a universal quantifier and have to be distinct from each other and the previously generated variables of this rule. The quantified formula for an injective match is true if the negation of the conjunction of literals representing the binary and unary edges specified in L \ L holds (l j m j n1 , m j n2 for a given edge (n 1 , l, n 2 ) ∈ E L \ E L and l j m j n for a unary edge (l, n) ∈ U L \ U L ). Within this negation we ensure an injective match with the tests that each newly created variable is disjoint from all other variables (m j n1 = m j n2 for n 1 ∈ L \ L and n 2 ∈ L).

Example 2. We continue the example and choose k = 2. We encode the injective applicability of both transformation rules (see Figures 2,3) for the first transition step. (The encoding for the second transition step only differs by the indices.)

Rule1 Cond 1 =fa 0 m 0 n1 ∧ ¬ m 0 n1 = m 0 n2 ∧ n∈U (m 0 n1 = n) ∧ n∈U (m 0 n2 = n) Rule13 Cond 1 =hob 0 m 0 n1 ∧ n∈U (m 0 n1 = n)∧ ∀m 0 n2 ∈ U : ¬ ¬ m 0 n2 = m 0 n1 ∧ flws 0 m 0 n1 , m 0 n2
Note that, while we use quantifiers here to make the presentation more concise, these can be (and are) eliminated in the encoding by explicit enumeration of their range, thus making the resulting formula quantifier-free.

Lemma 2. Given a graph transformation rule r = L, R and a host graph G j . r Cond j+1 is satisfiable with the interpretation I j (G j ) representing G j iff there exists a match m : L → G j and the assignment of the variables is according to that match (m j n = m N (n)).

In the following we describe the encoding of the actual application of a graph transformation rule. Note, that we do not describe graph transformation rules with node creation/deletion here to keep illustration simple. Nevertheless, at the end of this section we briefly discuss these features.

Encoding r App i of the application of a transformation rule r. Let graph G j (j = i-1) be the host graph as before. We use the previously created variables. Added binary edges (n 1 , l, n 2 ) ∈ E R \ E L have to exist in the resulting graph, encoded by a literal l j+1 m j n1 , m j n2 . Analogously, added unary edges are encoded by the corresponding positive unary literal. Similarly, deleted edges must not be present in the resulting graph and are encoded via the corresponding negated literals.

All other edges, which are neither deleted, nor added, exist in the resulting graph G j+1 if and only if they exist in the host graph G j . This is represented by a universally quantified equivalence for each pair of two nodes from U from which we exclude the changed edges. Let {(n 1 , l, n 2 ) , ..., (n 3 , l, n 4 )} ⊆ (E R \E L ∪ E L \ E R ) be the set of changed edges with label l, which we need to exclude. For each label l ∈ L E we encode as follows. (The same holds true analogously for unchanged unary edges. All these parts are combined by conjunction.) ∀n s , n t ∈ U :(l j (n s , n t ) ⇔ l j +1 (n s , n t ) same interpretation

∨ n s = m j n1 ∧ n t = m j n2 ∨ ... except for all the ∨ n s = m j n3 ∧ n t = m j n4 ). changed edges
Example 3. We continue the example. As mentioned before, the encodings for the second transition step differs only by the indices.

Rule1 App 1 =hon 1 m 0 n1 ∧ ldr 1 m 0 n1 , m 0 n2 ∧ req 1 m 0 n1 , m 0 n2 ∧ ¬fa 1 m 0 n1 ∧ ∀n s , n t ∈ U : (flws 0 (n s , n t ) ⇔ flws 1 (n s , n t )) ∧ ∀n s , n t ∈ U : ((ldr 0 (n s , n t ) ⇔ ldr 1 (n s , n t )) ∨ n s = m 0 n1 ∧ n t = m 0 n2 ) ∧ ∀n s , n t ∈ U : ((req 0 (n s , n t ) ⇔ req 1 (n s , n t )) ∨ n s = m 0 n1 ∧ n t = m 0 n2 ) ∧ ∀n ∈ U : (fa 0 (n) ⇔ fa 1 (n)) ∨ n = m 0 n1 ∧ ∀n ∈ U : (hob 0 (n) ⇔ hob 1 (n)) ∧ ∀n ∈ U : (hod 0 (n) ⇔ hod 1 (n)) ∧ ∀n ∈ U : (hon 0 (n) ⇔ hon 1 (n)) ∨ n = m 0 n1 ∧ ∀n ∈ U : (flw 0 (n) ⇔ flw 1 (n)) Rule13 App 1 =¬hob 1 m 0 n1 ∧ hod 1 m 0 n1 ∧ ∀n s , n t ∈ U : (flws 0 (n s , n t ) ⇔ flws 1 (n s , n t ))
∧ ∀n s , n t ∈ U : (ldr 0 (n s , n t ) ⇔ ldr 1 (n s , n t ))

∧ ∀n s , n t ∈ U : (req 0 (n s , n t ) ⇔ req 1 (n s , n t ))

∧ ∀n ∈ U : (fa 0 (n) ⇔ fa 1 (n)) ∧ ∀n ∈ U : (hob 0 (n) ⇔ hob 1 (n)) ∨ n = m 0 n1 ∧ ∀n ∈ U : (hod 0 (n) ⇔ hod 1 (n)) ∨ n = m 0 n1 ∧ ∀n ∈ U : (hon 0 (n) ⇔ hon 1 (n)) ∧ ∀n ∈ U : (flw 0 (n) ⇔ flw 1 (n))
Lemma 3. Given a graph transformation rule r = L, R and a host graph G j . r Cond j+1 ∧ r App j+1 is satisfiable with an interpretation representing graphs G j and G j+1 (i.e., I j (G j ) and I j+1 (G j+1 )), iff G j r,m =⇒ G j+1 holds and the assignment of the variables is according to that match (m j n = m N (n)).

Encoding of the forbidden pattern. In order to check reachability of the forbidden pattern for our path of length k, we have to check its applicability to G k . Thus, we encode the reachability check for the pattern F by F Cond k .

Dynamics of nodes.

For illustration purposes, we omitted the aspects of added and deleted nodes. These are more difficult to handle, as they can have many side effects. We summarize the additional encoding efforts necessary. Given that we cannot handle a changing universe in our formula, we need a universe U that can capture all possibilities. Thus, we search the transformation rule with the highest number max of new nodes and add k • max new nodes to U. This trick enables us to apply k transitions without the need to change the universe.

Of course this introduces the new problem of having "potential" nodes in U that do not actually belong to the graph. To solve this problem, we introduce the dead-predicate, initially valued 1 for all potential nodes and 0 for all nodes in the initial graph. The label set, the rules (including NACs) and their encodings can be automatically adjusted in a fairly straightforward manner to emulate the expected semantics of that predicate. In addition, one has to encode the deletion of all edges adjacent to deleted nodes to ensure the non-existence of dangling edges. For details, please refer to [START_REF] Isenberg | Bounded Model Checking für Graphtransformationssysteme als SMT-Problem[END_REF].

The central theorem of this paper states the correctness of our approach.

Theorem 1. Given a GTS G = (S, P ), a forbidden pattern F and a bound k.

The encoding

S ∧ T 1 ∧ ... ∧ T k ∧ F Cond k is satisfiable iff F is reachable in G in k steps.
The satisfying interpretation represents graphs G 0 to G k (i.e., I i (G i )) in a path G 0 , ..., G k of G containing the forbidden pattern.

As the satisfying interpretation represents the graphs along a path with the forbidden pattern, we can directly use this to present this path.

From Reachability to LTL. The version presented above of encoding paths of length k of a graph transformation system lacks the ability of describing finite paths of length smaller k. If a path has length i < k, then there is no transformation rule applicable to host graph G i . Thus, the encoding T i+1 of the transition i + 1 is not satisfiable, which means the path cannot be found and therefore not be checked for reachability. In consequence of this, we have to iteratively check all paths of length i with 1 ≤ i ≤ k. This however forces the satisfiability checking of up to k instances, resulting in a long runtime. To overcome this issue, we introduce a self-loop, which is only applicable, if and only if no transformation rule is applicable. In order to encode this self-loop, we developed an encoding of the non-applicability of a rule. The self-loop enables a path of length smaller than k to be represented by a path of length k. As strictly smaller paths are not checked separately, we adapt the encoding of the forbidden pattern to F Cond 0 ∨ ... ∨ F Cond k . Thus, we do not need to check for strictly smaller paths. We will compare both approaches in the next section.

This self-loop and the encoding of the non-applicability allow us to completely encode the BMC of LTL formulae. The semantics and the encoding of the LTL formula are the same as for standard BMC of Kripke structures, except that atomic propositions here mean the applicability of a pattern and negated atomic propositions mean the non-applicability. In general, our technique is slightly more expressive than LTL, as we can check whether a transformation rule actually was applied in a transition, not just its potential applicability to a host graph.

Theorem 1 describes the iterative version for a forbidden pattern. All previously mentioned lemmata and a more general theorem for LTL formulae without iterative checking are described and proved by Isenberg [START_REF] Isenberg | Bounded Model Checking für Graphtransformationssysteme als SMT-Problem[END_REF].

Implementation and Evaluation

In the following, we shortly describe our implementation and present results of the evaluation of our technique.

We built a prototypical implementation of our BMC technique as an extension to GROOVE [START_REF] Rensink | The GROOVE simulator: A tool for state space generation[END_REF], which can generate the encoding in two ways, the first of which is described in this paper. The second encoding does not use different predicates (numbering) to differentiate between the graphs in different steps of a path, but different universes. A first result of the evaluation is that these encodings are basically equally well suited; none can outperform the other. In both cases the result of the encoding is an SMT formula written according to the SMT-Lib v2.0 format [START_REF] Barrett | The SMT-LIB Standard: Version 2.0[END_REF], which is then fed into the SMT solver Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF]. If a satisfiable interpretation is found, the represented counterexample is displayed.

We tested our approach on several examples, including the car platooning GTS [START_REF] Backes | A graph transformation case study for the topology analysis of dynamic communication system[END_REF]. The forbidden pattern used by this example is shown in Figure 1b and does not occur within the state space of the original GTS. To check our approach, we also created a faulty specification of car platooning, essentially by omitting the NAC of rule 13 (Instance 1). With this rule modified, the graph transformation system yields several paths containing the forbidden pattern. To further increase the complexity of verification, we added a rule creating new cars as to make the state space infinite and to have an instance with node dynamics (Instance 2). These instances have 15, respectively 16 transformation rules.

On these two instances, we compare the iterative (it) reachability check and the non-iterative one (nit) using the self-loop. For this, we use several initial graphs with different numbers of nodes (see Figure 4b). In addition, we compared both the iterative and non-iterative reachability check for different bounds using Instance 1 with an initial graph consisting of 8 nodes (see Figure 4a). Note, that the shortest path containing the forbidden pattern has length 9.

Our technique works most efficiently in its non-iterative version when the guess of the bound is close to the size of the counterexample. If the bound is Fig. 4: Results of our experiments chosen much higher than the length of the smallest counterexample, the iterative can outrun the non-iterative version, as it only evaluates paths up to the length of the smallest counterexample (see Figure 4a). One further observation gained from looking at different case studies is that the order of the encodings of the transformation rules matters (with respect to solving time), in particular when having only one path containing the forbidden pattern in a huge set of paths. We also compared our tool with GROOVE's full state space exploration as well as its BMC technique. The BMC technique in its version as online in March 2013 cannot (strangely) deal with the car platooning GTS of Instance 2 which is infinite state. Unfortunately, we do not see the reason for this, and thus a meaningful comparison is not possible. A comparison with GROOVE's full state space exploration shows that GROOVE is faster for the finite state Instance 1, but -because of the very nature of the exploration technique -cannot deal with the infinite state Instance 2. The conclusion of our evaluation is thus that our technique can be seen as a complement to existing approaches, especially useful for bug finding in GTSs with infinite state spaces. We moreover think that our approach will prove its strength in cases when the error path is already approximately known, for instance when checking for spurious counterexamples.

Related Work

BMC [START_REF] Biere | Symbolic model checking without BDDs[END_REF] is a standard technique originally from the field of circuit verification. It unfolds the transition relation up to a predefined boundary to check for errors. One of its main concepts is the encoding of the problem as a SAT instance.

While the encoding of problems as a SAT/SMT problem is a well known standard technique in the field of planning [START_REF] Kautz | Planning as satisfiability[END_REF][START_REF] Rintanen | Planning and sat[END_REF], this is not the case for graph transformation systems. However, there are some approaches transforming GTSs into the planning language PDDL [START_REF] Tichy | Planning self-adaption with graph transformations[END_REF] to use recent progress in that field.

There is also research focusing on transformations into other target logics to verify graph properties, e.g., using rewriting logic [START_REF] Vandin | Towards a maude tool for model checking temporal graph properties[END_REF][START_REF] Bergmann | Advances in model transformations by graph transformation: Specification, execution and analysis[END_REF].

However, some approaches use only the concept of bounding the state space without the encoding as a SAT problem. Kastenberg [START_REF] Kastenberg | Graph-based software specification and verification[END_REF] constructs a Büchi automaton on-the-fly and uses a nested-DFS algorithm to check non-emptiness by iteratively searching the state space up to predefined boundaries.

Baresi [START_REF] Baresi | On the use of Alloy to analyze graph transformation systems[END_REF] transforms a given GTS into Alloy, a simple structural modeling language, which is then automatically transformed into a propositional formula. The generated formula is afterwards fed into a SAT-solver. This approach, however, doesn't utilize SAT-solving directly, but uses an intermediate tool.

Another approach using propositional formulae is the one presented by Kreowski [START_REF] Kreowski | Graph Transformation Units Guided by a SAT Solver[END_REF], which is very similar to ours, but differs in some major points. We use an encoding in first-order predicate logic, allowing us to represent the graph transformation system in a more compact and readable manner. This can be of great help with respect to planned future research, where we are interested in interpolation. In addition, the representation as SMT-formula gives us the ability to let the SMT-solver handle the matches itself. In contrast, Kreowski enumerates all possible matches in his encoding. The overhead of using SMT instead of SAT should be small for the used theory. Thus, our approach can be fast if the solver is able to restrict the search space quickly.

Other approaches to solving the problem with state space explosion and infinite growth focus on overapproximation, rather than on bounded state spaces (underapproximation). The upside to this is that positive results extend to the entire state space, rather than just a small subset that has been examined. The downside is that negative results might not be definite and there can be no guarantee of termination without excluding some types of inputs.

Into this class of approaches falls the work by Barbara König et al. [START_REF] König | Augur 2 -a new version of a tool for the analysis of graph transformation systems[END_REF], which uses a combined formalism of graphs and Petri nets. Other overapproximation approaches, inspired by shape analysis [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF], use a more direct encoding of abstraction. Examples are the work by Rensink and Zambon [START_REF] Rensink | Neighbourhood abstraction in GROOVE[END_REF][START_REF] Zambon | Graph subsumption in abstract state space exploration[END_REF] as well as Steenken, Wonisch and Wehrheim [START_REF] Steenken | Sound and Complete Abstract Graph Transformation[END_REF].

Another approach that performs a kind of overapproximation is given by Giese, Beyer et al. [START_REF] Becker | Symbolic invariant verification for systems with dynamic structural adaptation[END_REF]. Here the idea is to prove inductive invariants of GTS by starting at the error pattern and working backwards.

Conclusion

In this paper, we presented a technique for BMC of graph transformation systems via SMT solving. To this end we encoded the reachability problem of a forbidden pattern in a GTS as an SMT formula. The presented approach can easily be extended to cover properties specified in LTL, and we have already implemented this extension as well.

One idea for further research could be to optimize the way of handling new nodes in transformation rules. In addition, one could try to find good heuristics for arranging the encodings of the transformation rules to improve the speed even further. Our main objective for the future is, however, the usage of this approach for a fast counter example analysis in our shape analysis based verification technique for GTS [START_REF] Steenken | Sound and Complete Abstract Graph Transformation[END_REF].

Fig. 1 :

 1 Fig.1: Part of the car platooning GTS[START_REF] Backes | A graph transformation case study for the topology analysis of dynamic communication system[END_REF]

Definition 6 (

 6 NAC). A negative application condition for a graph transformation rule r = L, R is a set C of total graph morphisms with domain L. Let

  Different Instances with bound 10