key: cord-0046346-ssdj96t3 authors: Schneider, Sven; Dyck, Johannes; Giese, Holger title: Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions date: 2020-05-31 journal: Graph Transformation DOI: 10.1007/978-3-030-51372-6_15 sha: b1685b14ba786cf2a8e9bb25670fc6406cae754e doc_id: 46346 cord_uid: ssdj96t3 The behavior of various kinds of dynamic systems can be formalized using typed attributed graph transformation systems (GTSs). The states of these systems are then modelled using graphs and the evolution of the system from one state to another is described by a finite set of graph transformation rules. GTSs with small finite state spaces can be analyzed with ease but analysis is intractable/undecidable for GTSs inducing large/infinite state spaces due to the inherent expressiveness of GTSs. Hence, automatic analysis procedures do not terminate or return indefinite or incorrect results. We propose an analysis procedure for establishing state-invariants for GTSs that are given by nested graph conditions (GCs). To this end, we formalize a symbolic analysis algorithm based on k-induction using Isabelle, apply it to GTSs and GCs over typed attributed graphs, develop support to single out some spurious counterexamples, and demonstrate the feasibility of the approach using our prototypical implementation. The verification of formal models of complex dynamic systems w.r.t. to formal specifications is one of the grand challenges of model driven engineering. However, the expressiveness required to cover the multitude of complex actual and desired behaviors of such systems renders analysis often undecidable. Indeed, the formalism of graph transformation systems (GTSs) considered here is known to be Turing complete. Hence, fully-automatic procedures for establishing meaningful properties on the behavior of such systems are then guaranteed to be not terminating in general or to produce indefinite or even incorrect results. We subsequently focus on GTSs where an analysis using an explicit state space exploration using tools such as Groove [2] and Henshin [3] is not applicable due to infinite or intractably large sets of initial or reachable states. We approach this problem by combining the symbolic static analysis techniques of k-induction and state abstractions to establish state invariants for dynamic systems with infinite state spaces modelled by GTSs. The idea of kinduction is to establish a state invariant by iteratively computing all shortest derivations from an initial state to a violating state. The use of state abstractions, which preserve and reflect the systems' behavior w.r.t. the invariant candidate, permits to handle GTSs with infinite sets of initial or violating states at the concrete level but finite (and sufficiently small) such sets at the abstract level. As main contributions, we (a) formalize the principle of k-induction in the theorem prover Isabelle in the form of an analysis algorithm and (b) instantiate this analysis algorithm for the setting of (b1) invariant candidates formalized using the logic of nested graph conditions (GCs) and (b2) a suitable notion of typed attributed graph transformation. This instantiation based approach thereby also clearly separates aspects of k-induction from GTS related concepts. To represent typed attributed graphs, we employ symbolic graphs [18] [19] [20] [21] [22] , which are similar to E-Graphs [12] . These symbolic graphs also give rise to an instantiation of GCs that permits the specification of constraints on attributes throughout the GCs. We employ a graph transformation step relation on symbolic graphs that deviates from those formalized in [21, 22] by being symmetric (allowing a backwards application used in the k-induction analysis algorithm) and by allowing for the removal of variables (not requiring that additional variables and their values must be guessed when computing backward steps). As closest related work, approaches using k-induction have been used before without formal foundation in [4] and in [7] [8] [9] [10] [11] assuming k = 1, graphs without attributes, a single initial state, or a subclass of all GCs. Hence, we extend this line of research by formally treating the more general case of an arbitrary value of k, graphs with attributes, infinitely many initial states, and all GCs. In [5, 25, 27, 28] , an abstraction of graphs results in shape graphs (which have limited expressiveness compared to GCs) where multiple nodes in the graph are represented by so called summary nodes in the shape graph and where multiplicity or even first-order logic constraints may further restrict this abstraction (see also [6] ). Moreover, in [15] , an abstraction of graphs is given in terms of consistent compasses (which can be encoded in GCs of depth one) containing a set of graphs of which one is matchable and a set of non-matchable graphs. Also, in [29] , the tool Alloy is used to establish state invariants for typed graphs. Further related analysis approaches are as follows. The tool Augur2 [1] abstracts GTSs to Petri nets but imposes restrictions on graph transformation rules thereby limiting expressiveness. Lastly, static analysis of programs for GTSs w.r.t. pre/post conditions has been developed in [23] as well as [24] . In Sect. 2, we formalize the principle of k-induction in the form of an analysis algorithm. In Sect. 3, we discuss our running example, our notion of attributed graph transformation, and the logic of GCs. In Sect. 4, we instantiate the analysis algorithm for attributed graph transformation and apply our prototypical implementation of it to our running example demonstrating its feasibility. In Sect. 5, we provide a conclusion and a discussion of future work. We now introduce our formalization of the technique of k-induction for the verification of (state) invariants. For this purpose, we introduce labelled transition systems (LTS) as an abstract framework, which is instantiated later on for graph transformation. The results of this section have been formalized in the interactive theorem prover Isabelle and we therefore omit all proofs. An LTS consists of a set S of states, a set L of labels, a relation δ of labelled steps between states, and initial states identified via a state predicate Z. Definition 1 (Labelled Transition System (LTS)). If S and L are sets of states and labels, δ ⊆ S × L × S, Z : S B, and Γ = (S, L, δ, Z), then Γ is a labelled transition system, written Γ ∈ S lts . Moreover, a finite path π ∈ paths(Γ, n) of Γ of length n is a sequence of n states from S interleaved with labels from L where s·l·s in π implies (s, l, s ) ∈ δ. Also, π S and π L map indices to the states and labels of the path π. In Sect. 4, we restrict the states of an LTS resulting in a sub-LTS as follows. A predicate I on the states of an LTS is an invariant for the LTS, if all states that are reachable from an initial state of the LTS satisfy I. Definition 3 (Invariant). If Γ =(S, L, δ, Z)∈S lts , I :S B, and ∀n ∈N. ∀π ∈paths(Γ, n). Z(π S (0)) → I(π S (n)), then Γ has invariant I, written invariant(Γ, I). Subsequently, we assume an invariant A (e.g. expressing earlier established invariants) for the LTS to improve applicability of the analysis approach as explained later on. For characterizing the k-induction algorithm below, we define shortest violations of a state predicate I as a finite path leading from an initial state to a state violating I visiting no further initial states and only passing through states satisfying I as well as A. Definition 4 (Shortest Violation). If Γ = (S, L, δ, Z) ∈ S lts , I : S B, A : S B, k ∈ N, π ∈ paths(Γ, k), Z(π S (0)), ¬I(π S (k)), ∀0 < j ≤ k. ¬Z(π S (j)), and ∀j < k. I(π S (j)) ∧ A(π S (j)), then π is a shortest violation of I by Γ of length k under A, written π ∈ SVio(Γ, A, I, k). The analysis algorithm I below checks for such shortest violations by (a) selecting all violating states s satisfying ¬I(s) and by (b) computing up to k steps backwards ensuring that all k additional states s visited on each of the paths obtained satisfy A(s ) ∧ I(s ). Firstly, when a state s , which is visited in this process, satisfies Z(s ), a shortest violation is obtained. Secondly, when no such path of k steps exists, there cannot be a shortest violation of greater length. Note that this analysis process benefits from employing the assumed invariant A, which is used to rule out paths with states that are known to be unreachable from an initial state by not satisfying A. The analysis algorithm I returns a value b with three different values where b = i represents a successful verification of the given state predicate I as an invariant (when no paths are left that may be extended to shortest violations), where b = v represents that at least one shortest violation was determined, and where b = u represents the situation that the analysis was unable to return one of the two former definite results for the provided value of k that is decremented in each recursive application of I inner . where vio(paths) = {π ∈ paths | Z(π S (0))} ext(paths) = {s · · π | π ∈ paths ∧ (s, , π S (0)) ∈ δ ∧ A(s) ∧ I(s)} Moreover, if k ∈ N and paths 0 = {π ∈ paths(Γ, 0) | ¬I(π S (0))} is the set of violating paths of length 0, then I(Γ, A, I, k) = I inner (Γ, A, I, k, 0, paths 0 ). The following theorem states that the analysis algorithm I performs a sound state invariant analysis as just described above. paths ⊆ paths(Γ, j) and one of the following items holds. The analysis algorithm I is implementable when the set of paths considered is finite throughout its computation. This is guaranteed when the LTS has violations for at most finitely many states (finite initial set of paths handed to I inner ) and when every state has at most finitely many predecessors (each path can only be extended backwards to finitely many paths in I inner ). The concrete instantiation of LTSs for GTSs in Sect. 4 is not finitely backwards branching in general because invariant candidates I may be violated by infinitely many states. Hence, we apply in Sect. 4 an abstraction leading to an abstract instantiation of LTSs for GTSs where the corresponding invariant candidate I is violated by finitely many states. We then establish a connection between both instantiations in terms of an LTS abstraction relation (LTSAR), which permits to analyze the abstract instantiation using I instead of the concrete instantiation. Intuitively, the paths considered using I for the concrete LTS are symbolically represented by the finite set of paths considered using I for the abstract LTS. Formally, an LTSAR consists of two subrelations R S relating states and R L relating labels of the underlying concrete and abstract LTSs. Note that we state suitable requirements on the relations R S and R L of an LTSAR in the following theorem and define only the type of an LTSAR here. For invariant candidates I and I for Γ and Γ , the following theorem states six requirements on an LTSAR (R S , R L ), which guarantee that (a) a violation of I in Γ implies the existence of a violation of I in Γ and (b) the absence of violations of I in Γ implies the absence of violations of I in Γ . The requirements R1-R6 used in these items are as follows. (every forward step of the abstract LTS Γ can be mimicked (forwards) by the concrete LTS Γ for two related source states (s, s ) to allow for the concretization of a violating path) (every backward step of the concrete LTS Γ (except for those leading to initial states) can be mimicked (backwards) by the abstract LTS Γ for two related target states (s,s ) to allow for the abstraction of a violating path) As a running example, we consider a single shuttle travelling on a network of tracks (see Fig. 1a for the type graph used) where subsequent tracks are connected using next edges. The graph attribution stores the velocity v and acceleration a of the shuttle and, moreover, the constants for minimal, maximal, and safe velocities as well as the constant track length s in a System node. The rules refer to the attributes to describe the velocity v of a shuttle after travelling over a track based on its current velocity v, acceleration a, and the constant track length s using the standard equation v 2 = v 2 + 2as. The velocity of the shuttle should be below the safe velocity on tracks with flag signal, the velocity of the shuttle should be constant on tracks with flag const, and the flag warning on a track indicates that a track with flag signal is to be expected ahead. Analysis should establish the fact that the shuttle never violates signal and const flags as an invariant, which is formalized in Fig. 1c using graph conditions explained below. Note that tracks with flag const between tracks with flag warning and tracks with flag signal may prevent timely deceleration. We employ an assumed invariant to (a) specify the constant attribute values of the system node, (b) to rule out track networks with dead ends and loops, and (c) to ensure warnings n tracks ahead of signals for a parameter n ∈ N in all considered track networks. We now recall attribute conditions (ACs) used by symbolic graphs and then revisit GTSs and GCs over symbolic graphs for describing actual and desired behavior in terms of a concrete LTS and state predicates from before. (b) Graphs G 1 and G 2 with monomorphism m : G 1 G 2 ,which maps nodes, edges, and variables ase xpected. All variable valuations that satisfy theat tribute constraint of G 1 also satisfy theat tribute constraint of G 1 translatedvia m,that is, The invariant candidate φ I stating that shuttles cannot accelerate on tracks with const flag and that shuttles cannot exceed the safe velocity on tracks with signal flag. The attribute logic AL contains ACs γ ∈ S AC X of first-order logic (FOL) ranging over a set X of variables. The satisfaction of γ by a valuation α : X V is denoted by α |= AC γ. The SMT solver Z3 [17] supports ACs constructed using a restricted set of operators for the sorts bool, int, real, and string. When Z3 is unable to determine an answer to the satisfiability problem (note that AL satisfaction is undecidable), which does not occur for the examples considered here, we would notify the user in our prototypical implementation. Symbolic graphs (called graphs subsequently) [18] are an adaptation of E-Graphs [12] . A finite graph G (such as those depicted in Fig. 1b) contains nodes, edges, variables G.X, and an AC G.ac ranging over G.X. Moreover, nodes and edges are equipped with node and edge attributes, which are connected to variables for which values are specified in the AC G.ac. A morphism m : G 1 G 2 from graph G 1 to G 2 (see e.g. Fig. 1b) maps nodes, edges, variables, node attributes, and edge attributes of G 1 to those of G 2 . The mappings of m must be compatible with the source and target functions of G 1 and G 2 as usual and G 2 .ac must imply the translation m(G 1 .ac) of G 1 .ac for all variable valuations to ensure that m characterizes a restriction of attributes (cf. Fig. 1b where this implication is discussed). Moreover, the class of all finite graphs typed (as usual using a typing morphism) over a given type graph TG is given by S graphs fin,TG or simply S graphs fin when TG is known. In the remainder, we only employ monomorphisms, written m : G 1 G 2 , with only injective mappings. The unique monomorphism from the empty graph ∅ to a graph G is denoted i(G) : ∅ G. Finally, the special monomorphism a(G) : G G describes that G is obtained from G by setting the AC G.ac to true (i.e., G equals G except that G .ac = ). The graph logic GL [14, 26] supports the specification of the (non)existence of certain subgraphs in a given host graph G. Besides propositional operators for (finite) conjunction and negation, GL features the exists operator ∃, which specifies for a given match m : H G of a (context) graph H into the host graph G that m can be extended to a match m : H G by using a monomorphism f : H H that explains how H is extended to the (context) graph H . The graph G 2 from Fig. 1b does not satisfy φ I because the initial monomorphism i(G 2 ) : ∅ G 2 can be extended to m from Fig. 1b , which is forbidden by the left part ∃(i(G 1 ), ) of φ I . Moreover, we define that two GCs φ 1 and φ 2 are consistent, when φ 1 only describes elements also described by φ 2 or none of them. To check satisfiability of a GC and consistency of two GCs, we employ the automated reasoning technique for GL in the form of the algorithm A for which tool support is available in AutoGraph as introduced in [26] . The algorithm A takes a GC φ as input, is known to terminate for unsatisfiable GCs (i.e., it is refutationally complete), and incrementally generates the set of minimal graphs satisfying φ (this set is empty for unsatisfiable GCs). As for the case of AL and Z3, we carefully handle cases where A does not terminate and also generates no minimal graph as discussed later on. is a GC over the empty graph and A terminates for φ, it returns the finite set of all minimal graphs satisfying φ. The standard operation shift from [13] is also applicable to symbolic graphs [26] . It defines an adaptation of a GC φ with context graph H for a monomorphism m : H H resulting in an equivalent GC with context graph H in the sense of the following fact (by considering how additional elements of H may be used in a satisfaction proof for the given GC φ). Graph transformation steps are defined using rules specifying structural and attribute transformations. A rule ρ contains for the structural part (as in the DPO approach) two monomorphisms ρ.del : K L and ρ.add : K R where K, L − ρ.del(K), and R − ρ.add(K) contain the preserved/deleted/added elements. For the attribute part, L, K, and R have the trivial ACs and a rule ρ contains an AC ρ.ac instead, which is defined over the disjoint union V (i.e., the coproduct, written where ρ.lX and ρ.rX map variables to the disjoint union V ) of the variables of L and R. Intuitively, variables originating from L are used as unprimed variables and variables originating from R are used as primed variables. Finally, a rule contains left and right hand side application conditions ρ.lC and ρ.rC defined over the graphs L and R and checked during the transformation as in the DPO approach. See Fig. 3 for two simple rules 1 and, for our running example, Fig. 2 for two of the total nine rules (see [8, Section C.1.6, p. 336] for a full description of the assumed invariants and rules of the considered GTS). Definition 10 (Graph Transformation Rules). If ρ.del : K L, ρ.add : K R are to monomorphisms, (ρ.lX : L.X V, ρ.rX : R.X V ) is a coproduct, ρ.ac ∈ S AC V , ρ.lC ∈ S GC L , ρ.rC ∈ S GC R , and L.ac = K.ac = R.ac = , then ρ = (ρ. del, ρ.add, ρ.lX, ρ.rX, ρ.ac, ρ.lC, ρ.rC) is a rule, written ρ ∈ S rules . Moreover, we define the following abbreviations. Graph transformations systems then contain a finite set of finite rules (used for graph transformation steps) and initial states described by a GC. (a) The rule 1 ρ toDec describes that a shuttle moves to the nex track and sets the acceleration to −2 when the current track has no warning or signal flag and the next track has no const flag. (b) The rule 1 ρ toSteady-Const-Warning describes that a shuttle moves to the next track and sets the acceleration to 0 when the current track has no signal flag and the next track has a const flag. (c) A graph transformation sequence where a shuttle fails to decelerate sufficiently before moving to a track with a signal flag due to the track with the const flag prohibiting deceleration in between. Fig. 2 . Two rules and a graph transformation sequence for our shuttle scenario. 1 Here, L, K, and R are given in a single graph and preserved/deleted/added elements are colored black/red/green and deleted/added elements are marked with /⊕. (a)The rule ρ 1 .It is not applicable to graphs that contain a C node with E 2 loop. It adds a B node, adds loop on a, and changes the value of the id attribute (given by variable x) of node a using an AC that uses the if-then-else operation ite. (b) The rule ρ 2 . It is not applicable to graphs where the matched A node has an E 4 loop or an id attribute of at most 6. It adds a C node c , adds an edge from the matched A node to c ,and increases the id attribute (given by variable x) of node a. (c)The initial states φ Z have a C node with E 2 loop. (d)The assumed invariant φ A states that no A node may have an id of 0. (e)The invariant candidate φ I states reachable graph contain no B node. (f)The analysis using I starts with the path π 0 = X 0 of length 0 where X0=(∅,¬φI). Using Ext, a path π 1 = X 1 ·(k 1 , ρ 1 , k 2 )· X2 of length 1 is constructed by extending π 0 . Using Ext, a path π 2 = X 3 · (k 3 , ρ 2 , k 4 ) · X 4 · (k 5 • k 1 , ρ 1 , k 6 • k 2 ) · X 5 of length 2 is constructed by extending π 1 where the second step of π 2 is obtained by refinement of π 1 via Ref. (g) The abstract states X i = (G i , φ i ) from Figure 3f . To ease presentation, we use GCs such as ρ 1 . lC on graphs different from L 1 . The ACs of G i are obtained according to the step relation considering the AC of the given source/target graph. Definition 11 (Graph Transformation System (GTS)). If P ⊆ fin S rules fin and φ Z ∈ S GC ∅ , then (P, φ Z ) is a graph transformation system. Deviating from [22] , we now introduce a notion of graph transformation steps in which structural and attribute transformations are decoupled. The defined step relation is symmetric and supports the removal as well as addition of variables, which is also relevant when attribute values are to be modified. There is a step G 1 σ G 2 with label σ, whenever • there is a rule ρ ∈ S rules fin with ρ.lG = L and ρ.rG = R as depicted below, • the graph L can be matched to G 1 using m 1 : L G 1 that satisfies the lefthand side application condition ρ.lC, • the graphḠ 1 is obtained from G 1 by setting the AC of G 1 to inducing the morphisms c 1 and a(G 1 ) compatible with m 1 , • the graphs D andḠ 2 are constructed according to the double pushout approach as pushout complement and pushout from left to right, • the graph G 2 is obtained fromḠ 2 by setting the AC of G 2 according to the AC ρ.ac of the rule inducing morphisms m 2 and a(G 2 ) compatible with c 2 , and • the morphism m 2 satisfies the right-hand side application condition ρ.rC. For this construction, σ = (σ.rule, σ.drule, σ.match, σ.comatch) = (ρ,ρ, m 1 , m 2 ) is the used label whereρ is the derived rule (cf. [13] ) withρ.del = b 1 ,ρ.add = b 2 , ρ.lC = shift(c 1 , ρ.lC),ρ.rC = shift(c 2 , ρ.lC), and where the ACρ.ac is adapted from ρ.ac according to the renamings of c 1 and c 2 . For our running example, see Fig. 2c for a graph transformation sequence applying the two rules from Fig. 2a and Fig. 2b . Note that the last graph of this sequence violates the invariant candidate from Fig. 1c as the shuttle exceeds the permitted velocity on a track with signal flag. The steps defined by this construction immediately induce a concrete LTS (see Definition 1) for a given GTS where the initial states are given by all graphs satisfying the GC characterizing initial graphs of the GTS. G, σ, H) | G σ H} is given by graph transformation steps of (P, φ Z ), • Z(Ḡ) =Ḡ |= φ Z uses the GC satisfaction relation, Moreover, a state G of Γ (i.e., a finite graph) satisfies a state predicate (cf. the last item above) given by a GC φ defined over the empty graph ∅ iff G |= φ. Finally, the operations left and the reverse operation right introduced in [13] can be adapted to symbolic graphs. The operation left inductively propagates a GC φ over the right hand side graph ρ.rG = R (such as the application condition ρ.lC) of a rule ρ to the left hand side graph ρ.lG = L of ρ by applying the renaming of graph elements according to ρ.del and ρ.add to the graphs in the GC φ. The two operations ensure the following compatibility with steps (cf. [13] ). Based on the preliminaries from the previous section on graph transformation and graph specification using GCs, we now apply our theory on k-induction from Sect. 2. Note that the instantiation presented here is specific to the step relation for graph transformation presented in the previous section due to the decoupling of transformation of structure and ACs. For this instantiation, we construct an LTS that is finitely backwards branching (see Definition 6) and that is related to the concrete LTS Γ from the previous section via a suitable LTSAR (see Definition 7) to permit an application of Theorem 2 for enabling the analysis of the GTS using I according to Theorem 1. For this purpose, we assume a fixed GTS (P, φ Z ), the induced LTS cLTS((P, φ Z )) = Γ (see Definition 13), an assumed invariant φ A ∈ S GC ∅ , and an invariant candidate φ I ∈ S GC ∅ . For demonstration purposes, we consider the GTS ({ρ 1 , ρ 2 }, φ Z ) with assumed invariant φ A and invariant candidate φ I from Fig. 3 . As an initial candidate for the LTS to be constructed, we define the LTS Γ in which each state (Ḡ,φ) is given by a GCφ and the graphḠ over whichφ is defined for improved readability. The LTS Γ induces an LTSAR in which the relation R S contains pairs (G, (Ḡ,φ)) for which some monomorphism m :Ḡ G with m |=φ exists. The steps of Γ adapt states (G 1 , φ 1 ) to states (G 2 , φ 2 ) using a rule ρ of the GTS (P, φ Z ) for matches k 1 : ρ.lG G 1 and k 2 : ρ.rG G 2 at the abstract level by considering all concrete steps of graphs H 1 and H 2 that are related to G 1 and G 2 via R S (by means of instantiation morphisms m 1 and m 2 ). That is, the same rule ρ can be applied to each graph covered by (G 1 , φ 1 ) and, vice versa, (G 2 , φ 2 ) covers only the graphs reachable using such steps. Definition 14 (Abstract LTS of GC Transformation). If (P, φ Z ) is a GTS then aLTS((P, φ Z )) = Γ = (S , L , δ , Z ) is the abstract LTS of (P, φ Z ) with Moreover, a state (Ḡ,φ) of Γ satisfies a state predicate (cf. the last item above) given by a GC φ defined over the empty graph ∅ iff ∃(i(Ḡ),φ) ∧ φ = ∅. 2 We state that each sub-LTS Γ of Γ induces a certain LTSAR for the LTS Γ . Selecting the entire LTS Γ = Γ results in an LTSAR, which does not satisfy the requirements of Theorem 2 in general. Instead, we obtain a suitable sub-LTS Γ of Γ in an on-the-fly manner during an application of I (see Definition 5): Γ then describes precisely the paths maintained by I inner in its parameter paths at any point in the computation. Hence, the initial candidate is the sub-LTS Γ 0 that contains the single state (∅, ¬φ I ) violating φ I . Note that Γ 0 induces an LTSAR satisfying the requirements R1-R5 already. See Fig. 3f where node X 0 represents this initial state inducing the path π 0 of length 0. Inside an application of I inner (Γ , φ A , φ I , k, i, paths) (see Definition 5), we extend paths in paths w.r.t. Γ and thereby adapt Γ i to Γ i+1 such that the LTSAR for Γ i+1 (see Lemma 1) also satisfies the requirements R1-R5 of Theorem 2. The satisfaction of requirement R6 for the backwards simulation may require that further path extensions are computed in subsequent iterations of I inner . In Fig. 3f , the path π 0 is extended to paths π 1 and π 2 where the last nodes X 2 and X 5 are then incrementally more specific than X 0 (w.r.t. the monomorphisms that satisfy their GCs). When the application of I terminates with a definite result b ∈ {i, v}, the obtained sub-LTS Γ i constructed up to this point induces an LTSAR, which meets the relevant requirements listed in Theorem 2. In particular (see also Theorem 3 later on), (a) for the result (v, paths) meaning that the invariant candidate φ I is violated by Γ , we can apply Part1 of Theorem 2 because R1-R5 are satisfied and (b) for the result (i, ∅) meaning that φ I is established as an invariant for Γ , we can apply Part2 of Theorem 2 because there are no further backward steps that require consideration since all paths constructed so far were discarded for not having any further relevant step implying also R6 as required. In the remainder, we discuss the backwards construction of paths of Γ for a GTS using the operation Ext. This extension operation (see Definition 16) entails a refining operation Ref (see Definition 15) used to adapt paths in line with the operation ext(paths) used in I to ensure that the requirements R1-R5 are satisfied by the corresponding sub-LTS Γ i+1 constructed so far. Extending a path π of Γ starting in a state (Ḡ,φ) adding a backwards step for a rule ρ may result in a refinement due to (a) additional graph elements when the comatch of the step does not only match elements ofḠ, (b) additional restrictions originating from the application conditions of ρ, and (c) fewer variable valuations satisfying the AC of the start graph of the path. For example, in Fig. 3f , the path π 1 = X 1 · (k 1 , ρ 1 , k 2 ) · X 2 (in the second line) is refined to X 4 · (k 5 • k 1 , ρ 1 , k 6 • k 2 ) · X 5 according to the monomorphism k 5 : G 1 G 4 for the application of ρ 2 in Extension-Step 2. Considering the elements X 1 and X 4 given in more detail in Fig. 3g , we see that X 4 is much more specific than X 2 due to the additional GC originating from ρ 2 , the inclusion of node c and edge e, and a more restrictive AC. The following operation Ref refines the path π starting in (Ḡ,φ G ) to a path π starting in (X,φ X ) for a monomorphism m :ḠX and a GCφ X defined on X, which describe the effect of the backwards step on π. It does so by adapting the monomorphisms contained in the labels of the steps in π, performs a step leading to a graphȲ to propagate attribute restrictions given by the AC ofX, and propagates the additional GCφ X to the resulting graphȲ . Definition 15 (Refinement of Abstract Paths). If Γ = (S , L , δ , Z ) ∈ S lts , π ∈ paths(Γ , n), m :ḠX,φ X ∈ S GC X , π ∈ paths(Γ , n), then π is the refinement of π via m andφ X , written π = Ref(π, m,φ X ), if an item applies. • n = 0, π = (Ḡ,φ G ), and π = (X,φ X ∧ shift(m,φ G )). Concrete violating paths of Γ (such as in Fig. 2c for our running example) can be constructed from symbolic violating paths of Γ starting in (Ḡ,φ G ) by (a) running the algorithm A from Fact 1 to obtain some monomorphism m :ḠX satisfyingφ G , (b) employing Z3 to determine a variable valuation satisfying the AC ofX resulting in some monomorphism m :ḠȲ , and (c) applying the operation Ref for m andφ Y = . Besides such concrete violating paths, we return all symbolic violating paths to the user for which A or Z3 fail to determine definite results (which does not occur in the examples considered here). We now introduce the operation Ext for extending a path of Γ by adding a further backwards step. To ensure that we construct all paths, we follow the definition of E-concurrent rules from [13] to generate all minimal overlaps for each successive rule application and to adjust GCs to the application conditions of the rules. Moreover, in item (8), we employ the operation Ref to adapt the given path of Γ to the additional step. Finally, in item (9), item (10), and item (11), we further split and filter the constructed paths to ensure that the state predicate satisfaction is compatible with R S (see Theorem 3). Definition 16 (Extension of Abstract Paths). If (P, φ Z ) is a GTS, Γ = aLTS((P, φ Z )), π ∈ paths(Γ , n), then Ext(π) computes the possibly empty set of all path extensions π ∈ paths(Γ , n + 1) of π using the following procedure. (1) (Ḡ,φ G ) is the first state of π. (2) ρ ∈ P is some rule of the GTS with ρ.lG = L and ρ.rG = R. (3) (e 1 :R E, e 2 :Ḡ E) ∈ E is a minimal overlapping of R andḠ (cf. [13] ). 3 (4) E (rev(ρ),ρ,e1,m)X is a step of the GTS where ρ is reversed using rev and applied forwards to E using match e 1 to obtain the required backwards step. (5)φ X = shift(a(X),ρ.lC ∧ left(ρ,ρ.rC ∧ ∃(a(E), shift(e 2 ,φ G )))) is the GC for X obtained using GC propagation as in [13] . (6)X (ρ,ρ,m,m•e1)Ȳ is a step of the GTS using the rule ρ possibly further restricting the AC from E toȲ . (7)φ Y = shift(a(Ȳ ),ρ.rC ∧ right(ρ,ρ.lC)) ∧ shift(m • e 2 ,φ G ) is the GC forȲ obtained using GC propagation as in [13] . (8) π 0 = (X,φ X )·(m, ρ, n =m•e 1 )·Ref(π,m•e 2 ,φ Y ) is obtained by prepending the new step to the path refinement of π according tom • e 2 andφ Y . Definition 8) , which can be checked using A, we know that (X,φ X ) either only covers graphs satisfying φ I or no such graphs. In this case, is the identity morphism onX) andπ 1 =π otherwise. (10) (Disambiguation of Abstraction for φ Z ) Analogous to item (9) for the GC φ Z representing the initial state of the GTS at hand obtainingπ 2 fromπ 1 . Figure 3f depicts two applications of Ext both requiring applications of Ref (the first refinement regarding the empty path π 0 is trivial and the second has been discussed above). The first extension uses ρ 1 from Fig. 3a , constructs the overlapping E 0 where the two B nodes are identified (not explicitly depicted), applies the reversal of rule ρ 1 using the match e 01 to obtain X 1 , and then applies ρ 1 to obtain the AC refinement X 2 = (G 2 , φ 2 ) of E 0 depicted in Fig. 3g . Note that X 2 = (G 2 , φ 2 ) still violates the invariant candidate φ I (for all monomorphisms m : G 2 H). The further extension using ρ 2 then results in path π 2 ending in X 5 = (G 5 , φ 5 ), which does not need to be considered further as X 5 violates the assumed invariant φ A (for all monomorphisms m : G 5 H). Finally, I from Definition 5 can be used to check a GTS against an invariant candidate φ I by applying I using the described instantiation. Theorem 3 (Instantiation of k-Induction for GTSs). If (P, φ Z ) is a GTS, φ A ∈ S GC ∅ is an assumed invariant, φ I ∈ S GC ∅ is an invariant candidate, k ∈ N, and the application of the algorithm I using the described instantiation Γ for Γ , Ext (from Definition 16) for ext, and {(∅, ¬φ I )} for paths 0 terminates with (b, paths), then Theorem 1 and Theorem 2 are applicable and (b, paths) is a sound judgement on whether φ I is an invariant for (P, φ Z ). Proof. The used operation Ext for path extension ensures that the last computed sub-LTS Γ of Γ results in an LTSAR (see Lemma 1) meeting the requirements R1-R5 from Theorem 2 as follows (by induction on the parameter k for R4). • Requirements R1 and R2 (preservation of invariant and initial state): Ensured by item (9) and item (10) in Definition 16. • Requirement R3 (R S is right total): Ensured by item (11) in Definition 16. • Requirement R4 (R S is left total on violating states): R4 means that each state G that violates φ I in Γ via some shortest violation is covered by some state (Ḡ,φ G ) of Γ . R4 is obviously satisfied by the initial LTS candidate that has the only state (∅, ¬φ I ). Moreover, every extension (entailing the described refinement) of the set of paths in each iteration preserves this property because the refinement only excludes paths that are known to be only covering paths not representing shortest violations. • Requirement R5 (forward steps of Γ are simulated by Γ ): Ensured by applying the path refinement operation Ref in the operation Ref. Lastly, the requirement R6 is satisfied for all states that are not at the beginning of a path in Γ since Ext considers all possible backward steps. For our running example, we applied our prototypical implementation of the analysis algorithm I. For k = 2, we obtained the indefinite result (u, paths) where the sequence from Fig. 2c is a concretization of a path in paths that could not be ruled out. As stated in Table 1 , a path length of k = 5 (i.e., 5-induction) was required to establish that φ I is an invariant. While the time required for invariant analysis increases exponentially with longer values of k due to the exponentially increasing number of paths of that length, we believe that the analysis times required for the running example already demonstrate feasibility albeit a potential for further optimizations of our prototypical implementation. Also note that the number of path extensions in each step grows exponentially with the size of the rules. Graphs for Object-Oriented Verification (GROOVE On safe service-oriented real-time coordination for autonomous vehicles Graph abstraction and abstract graph transformation Rewriting abstract structures: materialization explained categorically Increasing expressive power of graph rules and conditions and automatic verification with inductive invariants Verification of graph transformation systems with k-inductive invariants Inductive invariant checking with partial negative application conditions k -inductive invariant checking for graph transformation systems k-inductive invariant checking for graph transformation systems Fundamentals of Algebraic Graph Transformation M-adhesive transformation systems with nested application conditions. part 1: parallelism, concurrency and amalgamation Correctness of high-level transformation systems relative to nested conditions A compass to controlled graph rewriting Probabilistic timed graph transformation systems Microsoft Corporation: Z3 Attributed graph constraints Symbolic graphs for attributed graph constraints Delaying constraint solving in symbolic graph transformation Symbolic attributed graphs for attributed graph transformation Lazy graph transformation Development of correct graph transformation systems Verifying monadic second-order properties of graph programs Canonical graph shapes Automated reasoning for attributed graph properties Verification of infinite-state graph transformation systems via abstraction Sound and complete abstract graph transformation Verification of graph-based model transformations using alloy We formalized the static analysis approach of k-induction using Isabelle for the abstract setting of LTSs establishing sufficient conditions for the preservation/reflection of invariants by means of an abstraction relation. We then applied this analysis approach to typed attributed GTSs by abstracting graphs by nested graph conditions (GCs) and by applying k-induction on these GCs. Our results extend the state of the art by permitting attributes as well as nested GCs for the specification of initial states, assumed invariants, and invariant candidates.In the future, we want to develop support for probabilistic/timed GTSs such as [16] . Moreover, we strive to develop further abstractions to improve support for GTSs with multiple active components such as shuttles. Finally, heuristics guiding the computation of paths in the analysis procedure using parameterizations may improve performance by e.g. prioritizing path extension over checking for violations of attribute constraints of assumed invariants.