Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions
 68 Downloads
Abstract
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 stateinvariants for GTSs that are given by nested graph conditions (GCs). To this end, we formalize a symbolic analysis algorithm based on kinduction 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.
Keywords
Formal static analysis Symbolic state space abstraction kinduction Symbolic graphs Isabelle1 Introduction
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, fullyautomatic 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 Open image in new window [2] and Open image in new window [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 kinduction 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 kinduction 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 ( Open image in new window ) and (b2) a suitable notion of typed attributed graph transformation. This instantiation based approach thereby also clearly separates aspects of kinduction from GTS related concepts.
To represent typed attributed graphs, we employ symbolic graphs [18, 19, 20, 21, 22], which are similar to Open image in new window [12]. These symbolic graphs also give rise to an instantiation of Open image in new window that permits the specification of constraints on attributes throughout the Open image in new window . 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 kinduction 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 kinduction 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 Open image in new window . 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 Open image in new window .
In [5, 25, 27, 28], an abstraction of graphs results in shape graphs (which have limited expressiveness compared to Open image in new window ) where multiple nodes in the graph are represented by so called summary nodes in the shape graph and where multiplicity or even firstorder 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 Open image in new window of depth one) containing a set of graphs of which one is matchable and a set of nonmatchable graphs. Also, in [29], the tool Open image in new window is used to establish state invariants for typed graphs.
Further related analysis approaches are as follows. The tool Open image in new window [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 kinduction 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 Open image in new window . 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.
2 Invariant Verification Using kInduction
We now introduce our formalization of the technique of kinduction 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 \(\delta \) 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, \(\delta \subseteq S\times L\times S\), Open image in new window and \(\varGamma =(S,L,\delta ,Z)\), then \(\varGamma \) is a labelled transition system, written Open image in new window.
Moreover, a finite path Open image in new window of \(\varGamma \) of length n is a sequence of n states from S interleaved with labels from L where \(s\cdot l\cdot s'\) in \(\pi \) implies \((s,l,s')\in \delta \). Also, Open image in new window and Open image in new window map indices to the states and labels of the path \(\pi \).
In Sect. 4, we restrict the states of an LTS resulting in a subLTS as follows.
Definition 2
(SubLTS). If Open image in new window, \(S'\subseteq S\), and Open image in new window, then \(\varGamma '\) is a subLTS of \(\varGamma \).
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 Open image in new window, Open image in new window, and Open image in new window Open image in new window, then \(\varGamma \) has invariant I, written Open image in new window.
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 kinduction 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 Open image in new window , and Open image in new window , then \(\pi \) is a shortest violation of I by \(\varGamma \) of length k under A, written Open image in new window .
The analysis algorithm \({\mathcal {I}}\) below checks for such shortest violations by (a) selecting all violating states s satisfying \(\lnot 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')\wedge 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 \({\mathcal {I}}\) returns a value b with three different values where \(b=\mathsf {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=\mathsf {v}\) represents that at least one shortest violation was determined, and where \(b=\mathsf {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 \({\mathcal {I}^{\mathrm {inner}}}\).
Definition 5
The following theorem states that the analysis algorithm \({\mathcal {I}}\) performs a sound state invariant analysis as just described above.
Theorem 1
(Soundness of \({{\mathcal {I}} {}}\)). If Open image in new window , and Open image in new window , then there is Open image in new window and one of the following items holds.

\(b=\mathsf {u}\), Open image in new window , and Open image in new window.

\(b=\mathsf {i}\), Open image in new window and Open image in new window .

\(b=\mathsf {v}\), Open image in new window, Open image in new window.
The analysis algorithm \({\mathcal {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 \(\mathcal {I}^\text {inner}\)) and when every state has at most finitely many predecessors (each path can only be extended backwards to finitely many paths in \(\mathcal {I}^\text {inner}\)).
Definition 6
(Finitely Backwards Branching LTS). If Open image in new window , and Open image in new window , then \(\varGamma \) is finitely backwards branching for I.
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 \({\mathcal {I}}\) instead of the concrete instantiation.
Intuitively, the paths considered using \({\mathcal {I}}\) for the concrete LTS are symbolically represented by the finite set of paths considered using \({\mathcal {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.
Definition 7
(LTS Abstraction Relation (LTSAR)). If Open image in new window , then \((R_S,R_L)\) is an LTS Abstraction Relation from \(\varGamma \) to \(\varGamma '\), written Open image in new window .
For invariant candidates I and \(I'\) for \(\varGamma \) and \(\varGamma '\), the following theorem states six requirements on an LTSAR \((R_S,R_L)\), which guarantee that (a) a violation of \(I'\) in \(\varGamma '\) implies the existence of a violation of I in \(\varGamma \) and (b) the absence of violations of \(I'\) in \(\varGamma '\) implies the absence of violations of I in \(\varGamma \).
Theorem 2
(Preservation/Reflection of Invariants using LTS Abstraction Relations). If Open image in new window and Open image in new window , then both of the following items hold.

Part1: R1, R2, R3, R4, R5, and not Open image in new window imply not Open image in new window .

Part2: R1, R2, R3, R4, R6, and Open image in new window imply Open image in new window .
The requirements R1–R6 used in these items are as follows.

R1: Open image in new window(\(R_S\) is compatible with invariant satisfaction)

R2: Open image in new window(\(R_S\) is compatible with initial states)

( \(R_S\) relates a concrete state \(s\in S\) to each abstract state \(s'\in S'\) )

R4: Open image in new window (\(R_S\) relates an abstract state \(s'\in S'\) to each concrete state \(s\in S\) for which a shortest violation of I exists)

(every forward step of the abstract LTS \(\varGamma '\) can be mimicked (forwards) by the concrete LTS \(\varGamma \) for two related source states \((s,s')\) to allow for the concretization of a violating path)

R6: Open image in new window(every backward step of the concrete LTS \(\varGamma \) (except for those leading to initial states) can be mimicked (backwards) by the abstract LTS \(\varGamma '\) for two related target states \((\bar{s},\bar{s}')\) to allow for the abstraction of a violating path)
3 Modelling and Specifying Graph Transformation
We now recall attribute conditions ( Open image in new window ) used by symbolic graphs and then revisit GTSs and Open image in new window over symbolic graphs for describing actual and desired behavior in terms of a concrete LTS and state predicates from before.
The attribute logic AL contains Open image in new window of firstorder logic (FOL) ranging over a set X of variables. The satisfaction of Open image in new window by a valuation Open image in new window is denoted by Open image in new window . The Open image in new window solver Open image in new window [17] supports Open image in new window constructed using a restricted set of operators for the sorts Open image in new window . When Open image in new window is unable to determine an answer to the satisfiability problem (note that Open image in new window 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 Open image in new window [12]. A finite graph G (such as those depicted in Fig. 1b) contains nodes, edges, variables Open image in new window, and an AC Open image in new window ranging over Open image in new window . Moreover, nodes and edges are equipped with node and edge attributes, which are connected to variables for which values are specified in the AC Open image in new window . A morphism Open image in new window 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 Open image in new window must imply the translation Open image in new window of Open image in new window 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 Open image in new window is given by Open image in new window or simply Open image in new window when Open image in new window is known. In the remainder, we only employ monomorphisms, written Open image in new window, with only injective mappings. The unique monomorphism from the empty graph Open image in new window to a graph G is denoted Open image in new window. Finally, the special monomorphism Open image in new window describes that \(G'\) is obtained from G by setting the Open image in new window to true (i.e., \(G'\) equals G except that Open image in new window ).
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 Open image in new window operator Open image in new window , which specifies for a given match Open image in new window of a (context) graph H into the host graph G that m can be extended to a match Open image in new window by using a monomorphism Open image in new window that explains how H is extended to the (context) graph \(H'\).
The graph \(G_2\) from Fig. 1b does not satisfy Open image in new window because the initial monomorphism Open image in new window can be extended to m from Fig. 1b, which is forbidden by the left part Open image in new window of Open image in new window.
Definition 8
Open image in new window , and (for satisfaction) Open image in new window .
Open image in new window , and (for satisfaction) Open image in new window.
Open image in new window is a GC over the extended graph \(H'\), and (for satisfaction) there is Open image in new window\(m=m'\circ f\) and Open image in new window .
Moreover, we define the following notions.

Derived operators: (true) Open image in new window , and (for all) Open image in new window .

Graph Satisfaction: If Open image in new window is a GC over the empty graph satisfied by the initial morphism Open image in new window (i.e., Open image in new window ) then Open image in new window is satisfied by G, written Open image in new window .

Satisfying morphisms: If Open image in new window is a GC, then Open image in new window.
Moreover, we define that two Open image in new window and Open image in new window are consistent, when Open image in new window only describes elements also described by Open image in new window or none of them.
Definition 9
(Consistent GCs). If Open image in new window and Open image in new window implies Open image in new window, then Open image in new windowis consistent withOpen image in new window , written Open image in new window .
To check satisfiability of a GC and consistency of two Open image in new window , we employ the automated reasoning technique for GL in the form of the algorithm Open image in new window for which tool support is available in Open image in new window as introduced in [26]. The algorithm Open image in new window takes a GC Open image in new window as input, is known to terminate for unsatisfiable Open image in new window (i.e., it is refutationally complete), and incrementally generates the set of minimal graphs satisfying Open image in new window (this set is empty for unsatisfiable Open image in new window ). As for the case of Open image in new window and Open image in new window , we carefully handle cases where Open image in new window does not terminate and also generates no minimal graph as discussed later on.
Fact 1
(Algorithm \(\mathcal {A}\)). If Open image in new window is a GC over the empty graph and Open image in new window terminates for Open image in new window , it returns the finite set of all minimal graphs satisfying Open image in new window .
The standard operation Open image in new window from [13] is also applicable to symbolic graphs [26]. It defines an adaptation of a GC Open image in new window with context graph H for a monomorphism Open image in new window 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 Open image in new window).
Fact 2
(Operation Open image in new window ). If Open image in new window and Open image in new window , then Open image in new window iff Open image in new window .
Definition 10
(Graph Transformation Rules). If Open image in new window are to monomorphisms, Open image in new window is a coproduct, Open image in new window , and Open image in new window , then Open image in new windowis a rule, written Open image in new window .
Moreover, we define the following abbreviations.

Open image in new window and Open image in new window are the left and right hand side graphs of the rule Open image in new window .

Open image in new window is the set of all rules where L, K, and R are finite.
Graph transformations systems then contain a finite set of finite rules (used for graph transformation steps) and initial states described by a GC.
Definition 11
(Graph Transformation System (GTS)). If Open image in new window and Open image in new window , then Open image in new windowis 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.
Definition 12
there is a rule Open image in new window with Open image in new window and Open image in new window as depicted below,
the graph L can be matched to \(G_1\) using Open image in new window that satisfies the lefthand side application condition Open image in new window ,
the graph \(\bar{G}_1\) is obtained from \(G_1\) by setting the AC of \(G_1\) to Open image in new window inducing the morphisms \(c_1\) and Open image in new window compatible with \(m_1\),
the graphs D and \(\bar{G}_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 \(\bar{G}_2\) by setting the AC of \(G_2\) according to the AC Open image in new window of the rule inducing morphisms \(m_2\) and Open image in new window compatible with \(c_2\), and
the morphism \(m_2\) satisfies the righthand side application condition Open image in new window.
For this construction, Open image in new window is the used label where Open image in new window is the derived rule (cf. [13]) with Open image in new window and where the Open image in new window is adapted from Open image in new window 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.
Definition 13
Open image in new window is the set of all finite graphs,
Open image in new window is the set of all step labels,
Open image in new window is given by graph transformation steps of Open image in new window,
Open image in new window uses the GC satisfaction relation,
Moreover, a state G of \(\varGamma \) (i.e., a finite graph) satisfies a state predicate (cf. the last item above) given by a GC Open image in new window defined over the empty graph Open image in new window iff Open image in new window .
Finally, the operations Open image in new window and the reverse operation Open image in new window introduced in [13] can be adapted to symbolic graphs. The operation Open image in new window inductively propagates a GC Open image in new window over the right hand side graph Open image in new window (such as the application condition Open image in new window) of a rule Open image in new window to the left hand side graph Open image in new window of Open image in new window by applying the renaming of graph elements according to Open image in new window and Open image in new window to the graphs in the GC Open image in new window. The two operations ensure the following compatibility with steps (cf. [13]).
Fact 3
(Operations Open image in new window and Open image in new window ). If Open image in new window is a finite rule with the left and right hand side graphs L and R, Open image in new window and Open image in new window are Open image in new window over L and R, and Open image in new window is a graph transformation step, then Open image in new window iff Open image in new window and Open image in new window iff Open image in new window .
4 Invariant Analysis for Graph Transformation Systems
Based on the preliminaries from the previous section on graph transformation and graph specification using Open image in new window , we now apply our theory on kinduction 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 \(\varGamma \) 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 \({\mathcal {I}}\) according to Theorem 1. For this purpose, we assume a fixed GTS Open image in new window , the induced LTS Open image in new window (see Definition 13), an assumed invariant Open image in new window , and an invariant candidate Open image in new window .
For demonstration purposes, we consider the GTS Open image in new window with assumed invariant Open image in new window and invariant candidate Open image in new window from Fig. 3.
As an initial candidate for the LTS to be constructed, we define the LTS \(\varGamma '\) in which each state Open image in new window is given by a GC Open image in new window and the graph \(\bar{G}\) over which Open image in new window is defined for improved readability. The LTS \(\varGamma '\) induces an LTSAR in which the relation \(R_S\) contains pairs Open image in new window for which some monomorphism Open image in new window with Open image in new window exists. The steps of \(\varGamma '\) adapt states Open image in new window to states Open image in new window using a rule Open image in new window of the GTS Open image in new window for matches Open image in new window and Open image in new window 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 Open image in new window can be applied to each graph covered by Open image in new window and, vice versa, Open image in new window covers only the graphs reachable using such steps.
Definition 14
Moreover, a state Open image in new window of \(\varGamma '\) satisfies a state predicate (cf. the last item above) given by a GC Open image in new window defined over the empty graph Open image in new window iff Open image in new window.^{2}
We state that each subLTS \(\varGamma ''\) of \(\varGamma '\) induces a certain LTSAR for the LTS \(\varGamma \).
Lemma 1
(LTSAR for GTS). If Open image in new window is a GTS, Open image in new window, \(\varGamma ''\) is a subLTS of Open image in new window, Open image in new window, and Open image in new window, then Open image in new window by Definition 7. \(\square \)
Selecting the entire LTS \(\varGamma ''=\varGamma '\) results in an LTSAR, which does not satisfy the requirements of Theorem 2 in general. Instead, we obtain a suitable subLTS \(\varGamma ''\) of \(\varGamma '\) in an onthefly manner during an application of \({\mathcal {I}}\) (see Definition 5): \(\varGamma ''\) then describes precisely the paths maintained by \({{\mathcal {I}^{\mathrm {inner}}}}\) in its parameter Open image in new window at any point in the computation. Hence, the initial candidate is the subLTS \(\varGamma ''_0\) that contains the single state Open image in new window violating Open image in new window . Note that \(\varGamma ''_0\) induces an LTSAR satisfying the requirements R1–R5 already. See Fig. 3f where node \(X_0\) represents this initial state inducing the path \(\pi _0\) of length 0.
Inside an application of Open image in new window (see Definition 5), we extend paths in Open image in new window w.r.t. \(\varGamma '\) and thereby adapt \(\varGamma ''_i\) to \(\varGamma ''_{i+1}\) such that the LTSAR for \(\varGamma ''_{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 \({{\mathcal {I}^{\mathrm {inner}}}}\). In Fig. 3f, the path \(\pi _0\) is extended to paths \(\pi _1\) and \(\pi _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 Open image in new window ).
When the application of \({\mathcal {I}}\) terminates with a definite result \(b\in \{\mathsf {i},\mathsf {v}\}\), the obtained subLTS \(\varGamma ''_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 Open image in new window meaning that the invariant candidate Open image in new window is violated by \(\varGamma '\), we can apply Part1 of Theorem 2 because R1–R5 are satisfied and (b) for the result \((\mathsf {i},\emptyset )\) meaning that Open image in new window is established as an invariant for \(\varGamma '\), 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 \(\varGamma '\) for a GTS using the operation Open image in new window . This extension operation (see Definition 16) entails a refining operation Open image in new window (see Definition 15) used to adapt paths in line with the operation Open image in new window used in \({\mathcal {I}}\) to ensure that the requirements R1–R5 are satisfied by the corresponding subLTS \(\varGamma ''_{i+1}\) constructed so far.
Extending a path \(\pi \) of \(\varGamma '\) starting in a state Open image in new window adding a backwards step for a rule Open image in new window may result in a refinement due to (a) additional graph elements when the comatch of the step does not only match elements of \(\bar{G}\), (b) additional restrictions originating from the application conditions of Open image in new window, and (c) fewer variable valuations satisfying the AC of the start graph of the path.
For example, in Fig. 3f, the path Open image in new window (in the second line) is refined to Open image in new window according to the monomorphism Open image in new window for the application of Open image in new window in ExtensionStep 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 Open image in new window, the inclusion of node c and edge e, and a more restrictive AC.
The following operation Open image in new window refines the path \(\pi \) starting in Open image in new window to a path \(\pi '\) starting in Open image in new window for a monomorphism Open image in new window and a GC Open image in new window defined on \(\bar{ X}\), which describe the effect of the backwards step on \(\pi \). It does so by adapting the monomorphisms contained in the labels of the steps in \(\pi \), performs a step leading to a graph \(\bar{ Y}\) to propagate attribute restrictions given by the AC of \(\bar{ X}\), and propagates the additional GC Open image in new window to the resulting graph \(\bar{ Y}\).
Definition 15
Concrete violating paths of \(\varGamma \) (such as in Fig. 2c for our running example) can be constructed from symbolic violating paths of \(\varGamma '\) starting in Open image in new window by (a) running the algorithm Open image in new window from Fact 1 to obtain some monomorphism Open image in new window satisfying Open image in new window , (b) employing Open image in new window to determine a variable valuation satisfying the AC of \(\bar{ X}\) resulting in some monomorphism Open image in new window , and (c) applying the operation Open image in new window for \(m'\) and Open image in new window . Besides such concrete violating paths, we return all symbolic violating paths to the user for which Open image in new window or Open image in new window fail to determine definite results (which does not occur in the examples considered here).
We now introduce the operation Open image in new window for extending a path of \(\varGamma '\) by adding a further backwards step. To ensure that we construct all paths, we follow the definition of Econcurrent rules from [13] to generate all minimal overlaps for each successive rule application and to adjust Open image in new window to the application conditions of the rules. Moreover, in item (8), we employ the operation Open image in new window to adapt the given path of \(\varGamma '\) 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 Open image in new window is a GTS, Open image in new window , then Open image in new window computes the possibly empty set of all path extensions Open image in new window of \(\pi \) using the following procedure.
 (1)
Open image in new window is the first state of \(\pi \).
 (2)
Open image in new window is some rule of the GTS with Open image in new window and Open image in new window .
 (3)
Open image in new window is a minimal overlapping of R and \(\bar{G}\) (cf. [13]).^{3}
 (4)
Open image in new window is a step of the GTS where Open image in new window is reversed using Open image in new window and applied forwards to E using match \(e_1\) to obtain the required backwards step.
 (5)
Open image in new window is the GC for \(\bar{ X}\) obtained using GC propagation as in [13].
 (6)
Open image in new window is a step of the GTS using the rule Open image in new window possibly further restricting the AC from E to \(\bar{ Y}\).
 (7)
Open image in new window is the GC for \(\bar{ Y}\) obtained using GC propagation as in [13].
 (8)Open image in new window is obtained by prepending the new step to the path refinement of \(\pi \) according to \(\bar{ m}\circ e_2\) and Open image in new window.
 (9)
(Disambiguation of Abstraction for Open image in new window) If Open image in new window is consistent with Open image in new window (see Definition 8), which can be checked using Open image in new window , we know that Open image in new window either only covers graphs satisfying Open image in new window or no such graphs. In this case, \(\tilde{\pi }_1\) is Open image in new window or Open image in new window (where Open image in new window is the identity morphism on \(\bar{ X}\)) and \(\tilde{\pi }_1=\tilde{\pi }\) otherwise.
 (10)
(Disambiguation of Abstraction for Open image in new window) Analogous to item (9) for the GC Open image in new window representing the initial state of the GTS at hand obtaining \(\tilde{\pi }_2\) from \(\tilde{\pi }_1\).
 (11)
(Nonemptyness of Abstraction) If Open image in new window and Open image in new window determine that \(\tilde{\pi }_2\) represents at least one concrete violation (as discussed subsequent to Definition 15) compatible with \(\phi _A\), then \(\pi '\) is equal to \(\tilde{\pi }_2\) (otherwise \(\tilde{\pi }_2\) results in no path extension).
Figure 3f depicts two applications of Open image in new window both requiring applications of Open image in new window (the first refinement regarding the empty path \(\pi _0\) is trivial and the second has been discussed above). The first extension uses Open image in new window from Fig. 3a, constructs the overlapping \(E_0\) where the two B nodes are identified (not explicitly depicted), applies the reversal of rule Open image in new window using the match \(e_{01}\) to obtain \(X_1\), and then applies Open image in new window to obtain the AC refinement Open image in new window of \(E_0\) depicted in Fig. 3g. Note that Open image in new window still violates the invariant candidate Open image in new window (for all monomorphisms Open image in new window). The further extension using Open image in new window then results in path \(\pi _2\) ending in Open image in new window , which does not need to be considered further as \(X_5\) violates the assumed invariant Open image in new window (for all monomorphisms Open image in new window).
Finally, \({\mathcal {I}}\) from Definition 5 can be used to check a GTS against an invariant candidate Open image in new window by applying \({{\mathcal {I}}}\) using the described instantiation.
Theorem 3
(Instantiation of kInduction for GTSs). If Open image in new window is a GTS, Open image in new window is an assumed invariant, Open image in new window is an invariant candidate, Open image in new window , and the application of the algorithm Open image in new window using the described instantiation \(\varGamma '\) for \(\varGamma \), Open image in new window (from Definition 16) for Open image in new window , and Open image in new window terminates with Open image in new window , then Theorem 1 and Theorem 2 are applicable and Open image in new window is a sound judgement on whether Open image in new window is an invariant for Open image in new window.
Results of invariant analysis for the abstract LTS for shuttle scenario.
Outcome Open image in new window of analysis algorithm \({\mathcal {I}}\)  

Lookahead n  Path length k  Duration  Element b  Size of element Open image in new window 
2  2  1 s  \(\mathsf {u}\)  6 
3  3  2 s  \(\mathsf {u}\)  12 
4  4  12 s  \(\mathsf {u}\)  8 
5  5  63 s  \(\mathsf {i}\)  0 
Proof
The used operation Open image in new window for path extension ensures that the last computed subLTS \(\varGamma ''\) of \(\varGamma '\) 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 Open image in new window in \(\varGamma \) via some shortest violation is covered by some state Open image in new window of \(\varGamma ''\). R4 is obviously satisfied by the initial LTS candidate that has the only state Open image in new window . 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 \(\varGamma '\) are simulated by \(\varGamma \)): Ensured by applying the path refinement operation Open image in new window in the operation Open image in new window .
Lastly, the requirement R6 is satisfied for all states that are not at the beginning of a path in \(\varGamma ''\) since Open image in new window considers all possible backward steps. \(\square \)
For our running example, we applied our prototypical implementation of the analysis algorithm \({\mathcal {I}}\). For \(k=2\), we obtained the indefinite result Open image in new window where the sequence from Fig. 2c is a concretization of a path in Open image in new window that could not be ruled out. As stated in Table 1, a path length of \(k=5\) (i.e., 5induction) was required to establish that Open image in new window 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.
5 Conclusion and Future Work
We formalized the static analysis approach of kinduction 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 kinduction 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.
Footnotes
 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 \(\ominus \)/\(\oplus \).
 2.
Definition 16 resolves cases where Open image in new window and Open image in new window are not consistent (Definition 8).
 3.
Open image in new window denotes the set of pairs of monomorphisms that are jointly epimorphic, that is, two monomorphisms that map to each graph element of their common target graph.
References
 1.Augur 2 (2008). http://www.ti.inf.unidue.de/en/research/tools/augur2
 2.Graphs for ObjectOriented Verification (GROOVE) (2011). http://groove.cs.utwente.nl
 3.EMF Henshin (2013). http://www.eclipse.org/modeling/emft/henshin
 4.Becker, B., Giese, H.: On safe serviceoriented realtime coordination for autonomous vehicles. In: 11th IEEE International Symposium on ObjectOriented RealTime Distributed Computing (ISORC 2008), 5–7 May 2008, Orlando, Florida, USA, pp. 203–210. IEEE Computer Society (2008). https://doi.org/10.1109/ISORC.2008.13
 5.Boneva, I., Rensink, A., Kurbán, M.E., Bauer, J.: Graph abstraction and abstract graph transformation. Technical report LNCS4549/TRCTIT0750, July 2007Google Scholar
 6.Corradini, A., Heindel, T., König, B., Nolte, D., Rensink, A.: Rewriting abstract structures: materialization explained categorically. In: Bojańczyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 169–188. Springer, Cham (2019). https://doi.org/10.1007/9783030171278_10CrossRefzbMATHGoogle Scholar
 7.Dyck, J.: Increasing expressive power of graph rules and conditions and automatic verification with inductive invariants. Master’s thesis, University of Potsdam, Hasso Plattner Institute, Potsdam, Germany (2012)Google Scholar
 8.Dyck, J.: Verification of graph transformation systems with kinductive invariants. Ph.D. thesis, University of Potsdam, Hasso Plattner Institute, Potsdam, Germany (2020). https://doi.org/10.25932/publishup44274
 9.Dyck, J., Giese, H.: Inductive invariant checking with partial negative application conditions. In: ParisiPresicce, F., Westfechtel, B. (eds.) ICGT 2015. LNCS, vol. 9151, pp. 237–253. Springer, Cham (2015). https://doi.org/10.1007/9783319211459_15CrossRefGoogle Scholar
 10.Dyck, J., Giese, H.: kinductive invariant checking for graph transformation systems. In: de Lara, J., Plump, D. (eds.) ICGT 2017. LNCS, vol. 10373, pp. 142–158. Springer, Cham (2017). https://doi.org/10.1007/9783319614700_9CrossRefzbMATHGoogle Scholar
 11.Dyck, J., Giese, H.: kinductive invariant checking for graph transformation systems. Technical report 119, Hasso Plattner Institute at the University of Potsdam, Potsdam, Germany (2017)Google Scholar
 12.Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer, Berlin (2006). https://doi.org/10.1007/3540311882CrossRefzbMATHGoogle Scholar
 13.Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: \(\cal{M}\)adhesive transformation systems with nested application conditions. part 1: parallelism, concurrency and amalgamation. Math. Struct. Comput. Sci. 24(4) (2014). https://doi.org/10.1017/S0960129512000357
 14.Habel, A., Pennemann, K.: Correctness of highlevel transformation systems relative to nested conditions. Math. Struct. Comput. Sci. 19(2), 245–296 (2009). https://doi.org/10.1017/S0960129508007202
 15.Kulcsár, G.: A compass to controlled graph rewriting. Ph.D. thesis, Technische Universität Darmstadt, January 2019. http://tuprints.ulb.tudarmstadt.de/9304/
 16.Maximova, M., Giese, H., Krause, C.: Probabilistic timed graph transformation systems. J. Log. Algebr. Meth. Program. 101, 110–131 (2018). https://doi.org/10.1016/j.jlamp.2018.09.003MathSciNetCrossRefzbMATHGoogle Scholar
 17.Microsoft Corporation: Z3. https://github.com/Z3Prover/z3
 18.Orejas, F.: Attributed graph constraints. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 274–288. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540874058_19CrossRefzbMATHGoogle Scholar
 19.Orejas, F.: Symbolic graphs for attributed graph constraints. J. Symb. Comput. 46(3), 294–315 (2011). https://doi.org/10.1016/j.jsc.2010.09.009MathSciNetCrossRefzbMATHGoogle Scholar
 20.Orejas, F., Lambers, L.: Delaying constraint solving in symbolic graph transformation. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 43–58. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642159282_4CrossRefzbMATHGoogle Scholar
 21.Orejas, F., Lambers, L.: Symbolic attributed graphs for attributed graph transformation. ECEASST 30 (2010). http://journal.ub.tuberlin.de/index.php/eceasst/article/view/405
 22.Orejas, F., Lambers, L.: Lazy graph transformation. Fundam. Inform. 118(1–2), 65–96 (2012). https://doi.org/10.3233/FI2012706MathSciNetCrossRefzbMATHGoogle Scholar
 23.Pennemann, K.: Development of correct graph transformation systems. Ph.D. thesis, University of Oldenburg, Germany (2009). http://oops.unioldenburg.de/884/. URN http://nbnresolving.de/urn:nbn:de:gbv:715oops9483
 24.Poskitt, C.M., Plump, D.: Verifying monadic secondorder properties of graph programs. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 33–48. Springer, Cham (2014). https://doi.org/10.1007/9783319091082_3CrossRefzbMATHGoogle Scholar
 25.Rensink, A.: Canonical graph shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 401–415. Springer, Heidelberg (2004). https://doi.org/10.1007/9783540247258_28CrossRefGoogle Scholar
 26.Schneider, S., Lambers, L., Orejas, F.: Automated reasoning for attributed graph properties. STTT 20(6), 705–737 (2018). https://doi.org/10.1007/s1000901804963CrossRefGoogle Scholar
 27.Steenken, D.: Verification of infinitestate graph transformation systems via abstraction. Ph.D. thesis, University of Paderborn (2015). https://nbnresolving.de/urn:nbn:de:hbz:466:215768
 28.Steenken, D., Wehrheim, H., Wonisch, D.: Sound and complete abstract graph transformation. In: Simao, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 92–107. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642250323_7CrossRefzbMATHGoogle Scholar
 29.Wang, X., Büttner, F., Lamo, Y.: Verification of graphbased model transformations using alloy. ECEASST 67 (2014). https://doi.org/10.14279/tuj.eceasst.67.943