=Paper=
{{Paper
|id=Vol-1955/staf-ds-2017-4
|storemode=property
|title=Analysis and Abstraction of Graph Transformation Systems via Type Graphs
|pdfUrl=https://ceur-ws.org/Vol-1955/staf-ds-2017-4.pdf
|volume=Vol-1955
|authors=Dennis Nolte
}}
==Analysis and Abstraction of Graph Transformation Systems via Type Graphs==
https://ceur-ws.org/Vol-1955/staf-ds-2017-4.pdf
Analysis and Abstraction of Graph
Transformation Systems via Type Graphs
Dennis Nolte
Abteilung für Informatik und Angewandte Kognitionswissenschaft,
Universität Duisburg-Essen, Germany
dennis.nolte@uni-due.de
Abstract. We generalize verification techniques from the theory of for-
mal languages to the framework of graph languages. For this purpose,
we investigate formalisms for specifying graph languages based on type
graphs and compare them to existing formalisms. To adapt the verifica-
tion approaches one needs a specification formalism with suitable closure
properties and positive results for decidability problems.
Introduction
The theory of formal languages plays an important role in computer science
and there exists a large number of applications for this theory, for instance
in compiler construction, parsing and verification. In verification some typical
methods are (non-)termination analysis [16,18], reachability analysis [17] and
counterexample-guided abstraction refinement [6]. Reachability analysis for ex-
ample is based on the decidability of the language inclusion problem, in com-
bination with the closure under union property and the possibility to compute
postconditions. Starting with an initial set of states, one builds the set of all
reachable states iteratively by computing the strongest postcondition and adding
all new states to the current set with the union operator. An inclusion check af-
ter each iteration is used to check if no new reachable state was added. Using
this analysis, one can prove the absence of erroneous states.
Many concurrent and distributed systems, especially those with a dynami-
cally evolving topology, can be naturally modelled by graphs and graph trans-
formation rules. Work on the verification of dynamic, graph-like structures has
shown that they introduce an additional level of complexity, compared to rule-
based systems where states have either a word or tree structure. While the theory
of formal languages is worked out very well in string and tree/term rewriting, it
is often non-trivial to solve the same problems when it comes to graph rewriting.
Therefore, it is natural to ask for generalizations of these verification techniques
for the framework of graph rewriting and additionally for a theory of graph
languages, where these techniques can be applied. The analysis of pointer struc-
tures, in the research field of heap analysis, is just one example, where the ade-
quate specification of sets of graphs in combination with verification techniques
is needed.
For this purpose, one needs a specification formalisms for graph languages
with suitable closure properties, positive results for decidability problems (like
membership, language inclusion and emptiness) and computable pre- and post-
conditions. Instead of just tinkering with fitting existing specification formalisms
for any given verification problem, we try to achieve a different main goal here:
The contribution of this research is help to understand the essence of different
graph specification languages, which grant them the possibility to adapt the
verification techniques. Therefore, we have started research on a very simple
specification formalism based on type graphs [9]. This formalism is analysed in
detail with respect to desirable properties and then refined stepwise to enrich its
expressiveness. Each refinement is again analysed and in addition compared to
existing formalisms. With this approach, we want to contribute to the compari-
son of existing formalisms and structure them according to their capabilities to
use in certain verification techniques.
Related Work
There already exist several approaches to specifying graph languages, for in-
stance via logics [10,11], grammars [14,19], automata [1,2] or even annotated
abstract graphs [22,24]. Most of these formalisms differ in terms of closure prop-
erties and there exists a trade off between expressiveness and decidability prop-
erties. This might lead to incompatibility with certain verification techniques.
Courcelle’s notion of recognizable graph languages [11] (which is equivalent
to regular word languages and closely related with monadic second-order graph
logic [10]) is widely known and accepted. However, it becomes quite impractical
with respect to actual applications due to the large size of the resulting graph
automata [1]. Nested application conditions [20] (as the counterpart to first order
logic [23]) can already be used to compute pre- and postconditions. However,
implication and satisfiability are already undecidable for this formalism. There
also exist hyperedge replacement grammars [19] (being equivalent to the notion
of context-free (word-)grammars), three valued logic analyser [24] (representing
heaps via graphs annotated with predicates from a three-valued logic) and several
other approaches one could name.
Usually these specification languages have at least one of the following prob-
lems: Language inclusion checks, needed for invariant checking, are usually un-
decidable. This is already true once the formalism has an expressive power of at
least first-order logic. On the other hand, expressiveness might sometimes not be
sufficient enough, for instance the existence of paths can not be specified in first-
order logic. The computation of postconditions, used in reachability analysis, is
often impossible or just too difficult, such that some kind of over-approximation
might be necessary to compute it. Or the computation can become way too
costly in general, which makes the formalism impractical from some point.
We believe that there is no one-fits-all solution. Our approach is to study
graph specification languages and classify them according to their properties.
Proposed solution
We focus on specification languages based on type graphs [8], where the language
of a type graph T consists of all graphs that can be mapped homomorphically
into T (with potentially extra constraints to extend the framework). Many spec-
ification formalisms that are usually used in abstract graph transformation [25]
and verification, are based on type graphs. For instance, shape graphs [22] can
be seen as type graphs with additional annotations.
We work with the algebraic double-pushout (DPO) approach to graph rewrit-
ing [13] to analyse graph transformation systems. Since we are interested in the
verification of graphs which may model specific systems, the advantage in using
DPO lies in the fact that deletion in unknown contexts is forbidden per default.
Therefore, by using DPO instead of other approaches like single-pushout (SPO),
we can ensure that the application of our rules never cause unwanted side-effects,
which could lead to inadequate models of the described system.
Type graphs are a standard tool for typing graph transformation systems
[7,13], but we are not aware of any case where they have been extensively studied
from the perspective of specification languages. Usually, one assumes that the
rules and the graphs to be rewritten are typed. This idea serves the purpose of
introducing constraints on the applicability of the rules and therefore type graphs
can be understood as a form of labelling. However, this is different from our
point of view, where graphs and rules remain untyped (even while working with
labelled graphs) and the type graphs are simply meant to represent a possibly
infinite set of graphs. Type graphs retain a nice intuition from regular languages
when it comes to specifying graph languages. The language of a given finite
state automaton M can be interpreted as the set of all string graphs that can be
mapped homomorphically to M (respecting initial and final states).
Preliminary Work
The following section presents my joint work with several co-authors and gives
an overview of my research topics. Up until now we have achieved several results,
which can be divided into the following two work packages:
– Termination Analysis. Proving the termination property of a rewriting sys-
tem, e.g. the absence of rewriting or derivation sequences of infinite length, is
an undecidable problem in general [21]. Nonetheless, given a rewriting system
(for instance in graph rewriting), one can try to run several proposed methods
in parallel to possibly find a solution for the specific termination problem. One
possible approach of proving termination is to construct a monotone function
that measures structural properties of the graphs to be rewritten. Afterwards
one shows that the value of such a function (or assigned weight of the graph)
decreases with every rule application. This is usually achieved by evaluating the
weights directly on the left-hand side and right-hand side of every rule in the
rewriting system.
We introduced a technique based on type graphs which are weighted over
different kinds of semirings (see [3,4]), to check if a given graph transformation
system is uniformly terminating, i.e. independently of the initial graph the rules
of the system can only be applied a finite number of times. This technique
was inspired by an existing method based on matrix interpretations for proving
termination in string, cycle and term rewriting systems [15]. The type graph was
used to specify the set of all possible graphs by finite means and at the same time
assign weights to the graphs to be rewritten. Depending on the semiring chosen
for the computation, we were able to prove termination for graph transformation
systems consisting of rules, that can be applied up to an exponential number of
times.
We implemented the new termination analysis technique (among others) in
a prototype Java-based tool named Grez [5]. The tool concurrently runs several
algorithms to possibly prove the termination of a given graph transformation
system. Our work in [3] extended Grez to be able to employ an SMT solver, to
solve inequalities resulting from our method. The inequalities encode all possible
morphisms from the given rule graphs (both left- and right-hand side) into po-
tential weighted type graph candidates. The variables, used in these encodings,
represent weights for each element of the type graph. Therefore, whenever the
SMT solver returns a valid solution for the inequalities, it gives rise to the weights
assigned to the type graph such that it becomes a witness for the termination
proof.
Finally, in [26] we translated term rewrite systems from the Termination
Problems Database (TPDB) into graph transformation systems and let Grez au-
tomatically prove termination on them. We investigated two different encodings
(namely the function and number encoding) in two possible rewriting interpre-
tations (called basic and extended version) for term rewrite rules into graph
transformation rules that preserve the termination property, e.g. whenever the
graph transformation system terminates, so does the term rewrite system. The
following table is an excerpt of our experimental results given in [26]:
Termination Analysis using Grez
Tested Total 201
No Result Found 84
Terminating Total 117 24
117 115 24 24
Terminating using Number Function Number Function
Encoding Encoding Encoding Encoding
Version Basic Extended
– Specifying Graph Languages. In our recent work [8] we analysed decidability
and closure properties for graph languages specified by type graphs. While not
being as expressive as recognizable graph languages, we proved positive results
with respect to decidability problems for the two simplest cases of specification
formalisms, namely type graph languages and restriction graph languages. A type
graph language contains all graphs which allow a homomorphism into a given
type graph, whereas a restriction graph language includes all graphs that do
not contain an homomorphic image of a given type graph. We also extended
the formalism in two different ways: First, we introduced boolean connectives
between type graphs to generate a type graph logic and second, we increased
the expressiveness of the type graph itself, by adding annotations to every type
graph element.
In case of the type graph logic, one already obtains the desired closure proper-
ties for free since they are semantically given by the logical conjunction, disjunc-
tion and negation operators. Due to the presence of these boolean operators the
language inclusion problem can be reduced to the emptiness problem. However,
it is still impossible to compute postconditions within this formalism. This is due
to the fact that one can not express the existence of a subgraph (here the right
hand-side graph from a graph transformation rule) in every graph contained in
the specified graph language.
We defined a category of annotated type graphs, to generate an abstract
framework, from which existing formalisms based on type graphs can be instan-
tiated. Each type graph is enriched with a set of annotations, whereas every
annotation can be parametrized. For instance, in one of our settings, the an-
notations are used to globally count all elements that can be mapped to the
elements in the type graph. This is different from UML multiplicities, which are
locally specified on the edges. The reason to allow several annotations for one
type graph, instead of a single annotation, is mainly to ensure closure under
union.
By adding annotations to the type graph, the expressiveness is too pow-
erful, such that the language inclusion problem becomes hard to decide. We
only obtained positive results for the language inclusion problem by restricting
the analysed graph languages to only contain graphs up to a given pathwidth
(equivalent to [1]). The situation remains unclear for the unbounded case and
is an open problem. At the same time, it remained unclear if the framework of
annotated type graphs is closed under the complement operation. However, by
adding annotations to the formalism, we were able to compute postconditions
of rule applications, which was impossible in the other refinements of the type
graph specification language. In addition, we investigated closure under rule ap-
plication, e.g. invariant checking for our frameworks. An overview of the results
given in [8] is shown in the following table, where the checkmark is shown in
brackets, whenever the results hold only for the bounded case so far:
Investigation Pure Restrict Logic Annotated
G ∈ L(T ) 3 3 3 3
Decidability L(T ) = ∅ 3 3 3 3
L(T1 ) ⊆ L(T2 ) 3 3 3 (3)
L(T1 ) ∪ L(T2 ) 7 3 3 3
Closure Prop. L(T1 ) ∩ L(T2 ) 3 7 3 3
G∗ \ L(T ) 7 7 3 ?
Invariant Checking 3 3 ? (3)
Future Work
While classifying specification languages via our categorical approach, we are
still interested in characterizing a specification language that allows to gener-
alize verification techniques, from the theory of formal languages. Our current
results show that one needs to extend the expressiveness of the type graphs by
allowing a set of annotations on the type graph elements, to be able to compute
postconditions. This is necessary, if we want to extensively use these formalisms
in application scenarios such as reachability analysis or non-termination analy-
sis. To compute the pre-/postconditions within the formalism, we will also have
to generalize Hoare logic. We still plan to study the possibility to integrate UML
multiplicities into our framework and investigate if the framework is able to
handle attributes and inheritance (like in [12]). Exploiting universal properties
from category theory, we are currently working on a materialisation construc-
tion (similar to [24]) for our generalized abstract setting. The basic observation
is that in most specification frameworks an abstract rewriting step is performed
by computing the (strongest) postcondition in two steps: by first materializing
the left-hand side of the rule to be applied (also called shift in some specification
formalisms), followed by adding the right-hand side (existentially quantified).
Being able to compute postconditions for the specification of graph languages
by using annotated type graphs, we plan to implement verification techniques
for this formalism in a prototype Java-tool called DrAGoM. We further plan to
benchmark the techniques of the tool with respect to runtime results.
References
1. Christoph Blume. Graph Automata and Their Application to the Verification of
Dynamic Systems. PhD thesis, University of Duisburg-Essen, 2014.
2. H.J. Sander Bruggink and Barbara König. On the recognizability of arrow and
graph languages. In Proc. of ICGT ’08. Springer, 2008. LNCS.
3. H.J. Sander Bruggink, Barbara König, Dennis Nolte, and Hans Zantema. Prov-
ing termination of graph transformation systems using weighted type graphs over
semirings. In Proc. of ICGT ’15, volume 9151 of LNCS. Springer, 2015.
4. H.J. Sander Bruggink, Barbara König, and Hans Zantema. Termination analysis
for graph transformation systems. In Proceedings of IFIP-TCS 2014, 2014.
5. H.J.S. Bruggink. Grez user manual. www.ti.inf.uni-due.de/research/tools/
grez, 2015.
6. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.
Counterexample-guided abstraction refinement for symbolic model checking. Jour-
nal of the ACM, 50(5):752–794, 2003.
7. A. Corradini, U. Montanari, F. Rossi, H. Ehrig, R. Heckel, and M. Löwe. Algebraic
approaches to graph transformation—part I: Basic concepts and double pushout
approach. In G. Rozenberg, editor, Handbook of Graph Grammars and Computing
by Graph Transformation, Vol. 1: Foundations, chapter 3. World Scientific, 1997.
8. Andrea Corradini, Barbara König, and Dennis Nolte. Specifying graph languages
with type graphs. In Proc. of ICGT ’17 (International Conference on Graph Trans-
formation), pages 73–89. Springer, 2017. LNCS 10373.
9. Andrea Corradini, Ugo Montanari, and Francesca Rossi. Graph processes. Funda-
menta Informaticae, 26(3/4):241–265, 1996.
10. Bruno Courcelle. The monadic second-order logic of graphs I. Recognizable sets
of finite graphs. Information and Computation, 85:12–75, 1990.
11. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order
Logic, A Language-Theoretic Approach. Cambridge University Press, June 2012.
12. Juan de Lara, Roswitha Bardohl, Hartmut Ehrig, Karsten Ehrig, Ulrike Prange,
and Gabriele Taentzer. Attributed graph transformation with node type inheri-
tance. Theoretical Computer Science, 376(3):139 – 163, 2007. Fundamental Aspects
of Software Engineering.
13. H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer. Fundamentals of Algebraic Graph
Transformation. Monographs in Theoretical Computer Science. Springer, 2006.
14. H. Ehrig, M. Pfender, and H. Schneider. Graph grammars: An algebraic approach.
In Proc. 14th IEEE Symp. on Switching and Automata Theory, 1973.
15. J. Endrullis, J. Waldmann, and H. Zantema. Matrix interpretations for proving
termination of term rewriting. Journal of Automated Reasoning, 40:195–220, 2008.
16. Jörg Endrullis and Hans Zantema. Proving non-termination by finite automata. In
RTA ’15, volume 36 of LIPIcs, pages 160–176. Schloss Dagstuhl–Leibniz-Zentrum
fuer Informatik, 2015.
17. Laurent Fribourg and Hans Olsén. Reachability sets of parameterized rings as
regular languages. In Proceedings of Infinity ’97, volume 9 of Electronic Notes in
Theoretical Computer Science. Elsevier, 1997.
18. Alfons Geser, Dieter Hofbauer, and Johannes Waldmann. Match-bounded string
rewriting. Applicable Algebra in Engineering, Communication and Computing,
15(3–4):149–171, 2004.
19. Annegret Habel. Hyperedge Replacement: Grammars and Languages. Springer-
Verlag, 1992. LNCS 643.
20. Annegret Habel and Karl-Heinz Pennemann. Nested constraints and application
conditions for high-level structures. In Formal Methods in Software and Systems
Modeling. Essays Dedicated to Hartmut Ehrig, on the Occasion of His 60th Birth-
day, pages 294–308. Springer, 2005. LNCS 3393.
21. D. Plump. Termination of graph rewriting is undecidable. Fundamenta Informat-
icae, 33(2):201–209, 1998.
22. Arend Rensink. Canonical graph shapes. In Proc. of ESOP ’04, pages 401–415.
Springer, 2004. LNCS 2986.
23. Arend Rensink. Representing first-order logic using graphs. In Proc. of ICGT ’04,
pages 319–335. Springer, 2004. LNCS 3256.
24. Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis
via 3-valued logic. TOPLAS, 24(3):217–298, 2002.
25. Dominik Steenken, Heike Wehrheim, and Daniel Wonisch. Sound and complete
abstract graph transformation. In Proc. of SBMF ’11, pages 92–107. Springer,
2011. LNCS 7021.
26. Hans Zantema, Dennis Nolte, and Barbara König. Termination of term graph
rewriting. In Proc. of WST ’16 (Workshop on Termination), 2016.