Invariant Analysis for Multi-agent Graph Transformation Systems Using k-Induction

The analysis of behavioral models such as Graph Transformation Systems (GTSs) is of central importance in model-driven engineering. However, GTSs often result in intractably large or even infinite state spaces and may be equipped with multiple or even infinitely many start graphs. To mitigate these problems, static analysis techniques based on finite symbolic representations of sets of states or paths thereof have been devised. We focus on the technique of k-induction for establishing invariants specified using graph conditions. To this end, k-induction generates symbolic paths backwards from a symbolic state representing a violation of a candidate invariant to gather information on how that violation could have been reached possibly obtaining contradictions to assumed invariants. However, GTSs where multiple agents regularly perform actions independently from each other cannot be analyzed using this technique as of now as the independence among backward steps may prevent the gathering of relevant knowledge altogether.

In this paper, we extend k-induction to GTSs with multiple agents thereby supporting a wide range of additional GTSs. As a running example, we consider an unbounded number of shuttles driving on a large-scale track topology, which adjust their velocity to speed limits to avoid derailing. As central contribution, we develop pruning techniques based on causality and independence among backward steps and verify that k-induction remains sound under this adaptation as well as terminates in cases where it did not terminate before.

1. 1.

   Approaches such as CEGAR [4] also aim at minimizing symbolic state spaces.

2. 2.

   Intuitively, GTSs have no built-in support for different agents as opposed to other non-flat formalisms (such as e.g. process calculi) where a multi-agent system is lazily constructed using a parallel composition operation where interaction steps between agents are then resolved at runtime. For such different formalisms, causality is much easier to analyze but it is one of the many strengths of GTSs that agents can interact in complex patterns not restricted by the formalism at hand.

3. 3.

   The computational trade-off between pruning costs and costs for continued analysis of retained paths will play out differently for each example but, due to the usually exponential number of paths of a certain length, already the rather simple pruning technique based on assumed invariants was highly successful in [6, 19] where it was also required to establish a definite judgement at all.

4. 4.

   To ease the presentation, we omit further assumed invariants excluding graphs with duplicate next edges or tracks with more than two successor/predecessor tracks.

5. 5.

   Note that our approach extends to the usage of general match morphisms.

6. 6.

   The candidate invariant \(\phi _{\mathsf {CI}}\) could also be violated because (a) it is not satisfied by all start graphs (which is excluded since \(\phi _{\mathsf {SC}} \,{\wedge }\,\phi _{\mathsf {CI}} \) captures the start graphs of the GTS), (b) a slow shuttle becomes a fast shuttle between a warning and a construction site (for which no rule exists in the GTS), and (c) a pair of a warning and a construction site could wrap a fast shuttle at runtime (for which no rule exists in the GTS).

7. 7.

   The considered GT steps must preserve the matched graph elements and thereby explain how one match is propagated over a GT step resulting in the other match.

8. 8.

   Similarly to the requirement on matches, which must essentially match the same graph elements, the extension monos must extend the graphs with the same graph elements up to the propagation along the considered symbolic steps.

9. 9.

   For concrete GT steps, we rely on [10, Theorem 4.7] to obtain a construction procedure for the operation \(\mathsf {linearize}\). Also, this construction procedure extends to the case of symbolic steps as the additional GCs in symbolic states are extended precisely by the application conditions of the two involved rules in exchanged order only.

10. 10.

    A symbolic state \((G,\phi )\) satisfies the start state condition \(\phi _{\mathsf {SC}} \) (or analogously an assumed invariant \(\phi _{\mathsf {AI}}\)) iff \(\phi \wedge \phi _{\mathsf {SC}} \) is satisfiable. The model generation procedure from [20] implemented in the tool AutoGraph [18] can be used to check GCs for satisfiability (if it returns unknown, the problem must be delegated to the user for \(\phi _{\mathsf {SC}} \) and satisfiability may be assumed for \(\phi _{\mathsf {AI}}\)). If \(\phi \wedge \lnot \phi _{\mathsf {SC}} \) (or, analogously, \(\phi \wedge \lnot \phi _{\mathsf {AI}} \)) is also satisfiable, not every concretization of paths \((G,\phi )\cdot \pi \) will be a violation. This source of overapproximation can be eliminated using splitting of states as in [19].

11. 11.

    Note that, due to linearization, \(R_p\) may already contain some of the steps derived here. By implicitly comparing steps derived here to those in \(R_p\), we ensure to not derive isomorphic copies of steps. Also, two distinct parallel independent steps do not need to be linearized if not both steps are already contained in \(R_p\).

12. 12.

    Two nodes \(n_1\) and \(n_2\) of a graph G are in a common weakly connected component (given by a set of nodes of G) of G iff there is a sequence of the edges of G from \(n_1\) to \(n_2\) where edges may be traversed in either direction.

13. 13.

    Parallel independent backward steps are always performed by different agents.

14. 14.

    This pruning technique can be refined by attributing agents to steps to then determine prunable states with greater precision complicating forward propagation.

Authors and Affiliations

1. Hasso Plattner Institute, University of Potsdam, Potsdam, Germany

   Sven Schneider, Maria Maximova & Holger Giese

Corresponding author

Correspondence to Sven Schneider .

Editors and Affiliations

1. Université Paris Cité, Paris, France

   Nicolas Behr

2. Computer Science and Engineering, Chalmers | Gothenburg University, Gothenburg, Sweden

   Daniel Strüber

Reprints and permissions

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics