Graph Transformations

This is an abstract of [1], a brief note describing the path of ideas that lead from the

theory of true concurrency

, a semantic theory about the nature of concurrent computation, to the

unfolding approach to model-checking

, a pragmatic technique for palliating the state-explosion problem in automatic verification. While the note provides a very incomplete and hence “false” view of true concurrency, it also includes several pages of references.

This keynote paper presents results coming out of an ongoing research project between Credit Suisse Luxembourg and the University of Luxembourg. It presents an approach that shows good potential to address security, risk and compliance issues the bank has in its daily business by the use of integrated organizational models build up by enterprise modeling activities. Such organizational models are intended to serve to describe, evaluate, automate, monitor and control as well as to develop an organization respecting given organizational security, risk and compliance side-constraints. Based on the empirical scenario at Credit Suisse, real-world requirements towards a modeling framework as well as the modeling process are developed. Graph Transformation techniques are proposed as formal framework for this purpose and they are evaluated in the sense of how far they can support the identified enterprise modeling activities in the context of the new enterprise modeling framework.

Graph transformation units are rule-based devices to model graph algorithms, graph processes, and the dynamics of systems the states of which are represented by graphs. Given a graph, various rules are applicable at various matches in general, but not any choice leads to a proper result so that one faces the problem of nondeterminism. As countermeasure, graph transformation units provide the generic concept of control conditions which allow one to cut down the nondeterminism and to choose the proper rule applications out of all possible ones. In this paper, we propose an alternative approach. For a special type of graph transformation units including the solution of many

NP

-complete and

NP

-hard problems, the successful derivations from initial to terminal graphs are described by propositional formulas. In this way, it becomes possible to use a SAT solver to find out whether there is a successful derivation for some initial graph or not and how it is built up in the positive case.

Applying an attributed graph transformation rule to a given object graph always implies some kind of constraint solving. In many cases, the given constraints are almost trivial to solve. For instance, this is the case when a rule describes a transformation

$G \Rightarrow H$

, where the attributes of

H

are obtained by some simple computation from the attributes of

G

. However there are many other cases where the constraints to solve may be not so trivial and, moreover, may have several answers. This is the case, for instance, when the transformation process includes some kind of searching. In the current approaches to attributed graph transformation these constraints must be completely solved when defining the matching of the given transformation rule. This kind of

early binding

is well-known from other areas of Computer Science to be inadequate. For instance, the solution chosen for the constraints associated to a given transformation step may be not fully adequate, meaning that later, in the search for a better solution, we may need to backtrack this transformation step.

In this paper, based on our previous work on the use of

symbolic graphs

to deal with different aspects related with attributed graphs, including attributed graph transformation, we present a new approach that allows us to delay constraint solving when doing attributed graph transformation. In particular we show that the approach is sound and complete with respect to

standard

attributed graph transformation. A running example, where a graph transformation system describes some basic operations of a travel agency, shows the practical interest of the approach.

We propose a dynamic logic tailored to describe graph transformations and discuss some of its properties. We focus on a particular class of graphs called termgraphs. They are first-order terms augmented with sharing and cycles. Termgraphs allow one to describe classical data-structures (possibly with pointers) such as doubly-linked lists, circular lists etc. We show how the proposed logic can faithfully describe (i) termgraphs as well as (ii) the application of a termgraph rewrite rule (i.e. matching and replacement) and (iii) the computation of normal forms with respect to a given rewrite system. We also show how the proposed logic, which is more expressive than propositional dynamic logic, can be used to specify shapes of classical data-structures (e.g. binary trees, circular lists etc.).

A new kind of behaviour-preserving insertions of new transitions in Petri nets is proposed, and a method for computing such insertions using a complete unfolding prefix of the Petri net is developed. Moreover, as several transformations often have to be applied one after the other, the developed theory allows one to avoid (expensive) re-unfolding after each transformation, and instead use local modifications on the existing complete prefix to obtain a complete prefix of the modified net.

In recent years, a research thread focused on the use of the unfolding semantics for verification purposes. This started with a paper by McMillan, which devises an algorithm for constructing a finite complete prefix of the unfolding of a safe Petri net, providing a compact representation of the reachability graph. The extension to contextual nets and graph transformation systems is far from being trivial because events can have multiple causal histories. Recently, we proposed an abstract algorithm that generalizes McMillan’s construction to bounded contextual nets without resorting to an encoding into plain P/T nets. Here, we provide a more explicit construction that renders the algorithm effective. To allow for an inductive definition of concurrency, missing in the original proposal and essential for an efficient unfolding procedure, the key intuition is to associate histories not only with events, but also with places. Additionally, we outline how the proposed algorithm can be extended to graph transformation systems, for which previous algorithms based on the encoding of read arcs would not be applicable.

We introduce an analysis method for graph transformation systems which checks that certain forbidden graphs are not reachable from the start graph. These forbidden graphs are specified by a context-free graph grammar. The technique is based on the approximation of graph transformation systems by Petri nets and on semilinear sets of markings. Especially we exploit Parikh’s theorem which says that the Parikh image of a context-free grammar is semilinear. An important application is deadlock analysis for interaction nets and we specifically show how to apply the technique to an infinite-state dining philosopher’s system.

G-Reactive Systems (GRSs) are a framework for the derivation of labelled transition systems (LTSs) from a set of unlabelled rules. A label for a transition from

A

to

B

is a context

C

[ − ] such that

C

[

A

] may perform a reaction and reach

B

. If either all contexts, or just the ”minimal” ones, are considered, the resulting LTS is called saturated (GIPO, respectively). The borrowed contexts (BCs) technique addresses the issue in the setting of the DPO approach. Indeed, from an adhesive rewriting system (ARS) a GRS can be defined such that DPO derivations correspond to reactions, and BC derivations to transitions of the GIPO LTS. This paper extends the BCs technique in order to derive saturated LTSs for ARSs, applying it to capture bisimilarity for asynchronous calculi.

We present Hoare-style axiom schemata and inference rules for verifying the partial correctness of programs in the graph programming language GP. The pre- and postconditions of this calculus are the nested conditions of Habel, Pennemann and Rensink, extended with expressions for labels in order to deal with GP’s conditional rule schemata and infinite label alphabet. We show that the proof rules are sound with respect to GP’s operational semantics.

Triple Graph Grammars (TGGs) are a well-established concept for the specification of model transformations. In previous work we have formalized and analyzed already crucial properties of model transformations like termination, correctness and completeness, but functional behaviour is missing up to now.

In order to close this gap we generate forward translation rules, which extend standard forward rules by translation attributes keeping track of the elements which have been translated already. In the first main result we show the equivalence of model transformations based on forward resp. forward translation rules. This way, an additional control structure for the forward transformation is not needed. This allows to apply critical pair analysis and corresponding tool support by the tool AGG. However, we do not need general local confluence, because confluence for source graphs not belonging to the source language is not relevant for the functional behaviour of a model transformation. For this reason we only have to analyze a weaker property, called translation confluence. This leads to our second main result, the functional behaviour of model transformations, which is applied to our running example, the model transformation from class diagrams to database models.

In model-driven engineering, models are primary artifacts and can evolve heavily during their life cycle. Therefore, versioning of models is a key technique which has to be offered by an integrated development environment for model-driven engineering. In contrast to text-based versioning systems we present an approach which takes abstract syntax structures in model states and operational features into account. Considering the abstract syntax of models as graphs, we define model revisions as graph modifications which are not necessarily rule-based. Building up on the DPO approach to graph transformations, we define two different kinds of conflict detection: (1) the check for operation-based conflicts, and (2) the check for state-based conflicts on results of merged graph modifications.

Model-driven development (MDD) has become a promising trend in software engineering. The model-driven development of highly complex software systems may lead to large models which deserve a modularization concept to enable their structured development in larger teams. Graphs are a natural way to represent the underlying structure of visual models. Typed graphs with inheritance and containment are well suited to describe the essentials of models based on the Eclipse Modeling Framework (EMF). EMF models already support the physical distribution of model parts. Based on the concept of distributed graphs, we propose typed composite graphs with inheritance and containment to specify logical distribution structures of EMF models. The category-theoretical foundation of this kind of composite graphs forms a solid basis for the precise definition of typed composite graph transformations obeying inheritance and containment conditions.

The functional behaviour of a graph transformation system is a crucial property in several application domains including model transformations and visual language engineering. Termination is one of the ingredients of functional behaviour and thus equally important. However, the termination of graph transformation systems is generally undecidable. Hence, most of the published termination criteria focus on specific classes of graph transformations. Unfortunately graph transformations with lots of production rules usually do not fit into one of these classes. It would be advantageous if different sets of the production rules in the graph transformation system could be verified using different criteria. This paper addresses this problem by providing structural conditions on the rules enabling such combination of termination criteria.

There are three variations of algebraic graph rewriting, the double-pushout, the single-pushout, and the sesqui-pushout approach. In this paper, we show that all three approaches can be considered special cases of a general rewriting framework in suitable categories of spans over a graph-like base category. From this new view point, it is possible to provide a general and unifying theory for all approaches. We demonstrate this fact by the investigation of general parallel independence. Besides this, the new and more general framework offers completely new ways of rewriting: Using spans as matches, for example, provides a simple mechanism for universal quantification. The general theory, however, applies to these new types of rewriting as well.

Finitary

$\mathcal{M}$

-adhesive categories are

$\mathcal{M}$

-adhesive categories with finite objects only, where the notion

$\mathcal{M}$

-adhesive category is short for weak adhesive high-level replacement (HLR) category. We call an object finite if it has a finite number of

$\mathcal{M}$

-subobjects. In this paper, we show that in finitary

$\mathcal{M}$

-adhesive categories we do not only have all the well-known properties of

$\mathcal{M}$

-adhesive categories, but also all the additional HLR-requirements which are needed to prove the classical results for

$\mathcal{M}$

-adhesive systems. These results are the Local Church-Rosser, Parallelism, Concurrency, Embedding, Extension, and Local Confluence Theorems, where the latter is based on critical pairs. More precisely, we are able to show that finitary

$\mathcal{M}$

-adhesive categories have a unique

$\mathcal{E}$

-

$\mathcal{M}$

factorization and initial pushouts, and the existence of an

$\mathcal{M}$

-initial object implies in addition finite coproducts and a unique

$\mathcal{E'}$

-

$\mathcal{M'}$

pair factorization. Moreover, we can show that the finitary restriction of each

$\mathcal{M}$

-adhesive category is a finitary

$\mathcal{M}$

-adhesive category and finitariness is preserved under functor and comma category constructions based on

$\mathcal{M}$

-adhesive categories. This means that all the classical results are also valid for corresponding finitary

$\mathcal{M}$

-adhesive systems like several kinds of finitary graph and Petri net transformation systems. Finally, we discuss how some of the results can be extended to non-

$\mathcal{M}$

-adhesive categories.

The introduction of adhesive categories revived interest in the study of properties of pushouts with respect to pullbacks, which started over thirty years ago in the category of graphs. Adhesive categories provide a single property of pushouts that suffices to derive lemmas that are essential for central theorems of double pushout rewriting such as the local Church-Rosser Theorem.

The present paper shows that the same lemmas already hold for pushouts that are hereditary, i.e. those pushouts that remain pushouts when they are embedded into the associated category of partial maps. Hereditary pushouts – a twenty year old concept – induce a generalization of adhesive categories, which will be dubbed partial map adhesive. An application relevant category that does not fit the framework of adhesive categories and its variations in the literature will serve as an illustrating example of a partial map adhesive category.

Graph transformation is being increasingly used to express the semantics of domain specific visual languages since its graphical nature makes rules intuitive. However, many application domains require an explicit handling of time in order to represent accurately the behaviour of the real system and to obtain useful simulation metrics.

Inspired by the vast knowledge and experience accumulated by the discrete event simulation community, we propose a novel way of adding explicit time to graph transformation rules. In particular, we take the event scheduling discrete simulation world view and incorporate to the rules the ability of scheduling the occurrence of other rules in the future. Hence, our work combines standard, efficient techniques for discrete event simulation (based on the handling of a future event set) and the intuitive, visual nature of graph transformation. Moreover, we show how our formalism can be used to give semantics to other timed approaches.

We propose a novel approach to the semantics of quantified

μ

-calculi, considering models where states are algebras; the evolution relation is given by a counterpart relation (a family of partial homomorphisms), allowing for the creation, deletion, and merging of components; and formulas are interpreted over sets of state assignments (families of substitutions, associating formula variables to state components). Our proposal avoids the limitations of existing approaches, usually enforcing restrictions of the evolution relation: the resulting semantics is a streamlined and intuitively appealing one, yet it is general enough to cover most of the alternative proposals we are aware of.

Mesh subdivision algorithms are usually specified informally using graphical schemes defining local mesh refinements. These algorithms are then implemented efficiently in an imperative framework. The implementation is cumbersome and implies some tricky indices management. Smith et al. (2004) asks the question of the declarative programming of such algorithms in an index-free way. In this paper, we positively answer this question by presenting a rewriting framework where mesh refinements are described by simple rules. This framework is based on a notion of topological chain rewriting. Topological chains generalize the notion of labeled graph to higher dimensional objects. This framework has been implemented in the domain specific language

MGS

. The same generic approach has been used to implement Loop as well as Butterfly, Catmull-Clark and Kobbelt subdivision schemes.

The distribution and revocation of public-key certificates are essential aspects of secure digital communication. As a first step towards a methodology for the development of reliable models, we present a formalism for the specification and reasoning about the distribution and revocation of public keys, based on graphs. The model is distributed in nature; each entity can issue certificates for public keys that it knows, and distribute these to other entities. Each entity has its own public key bases and can derive new certificates from this knowledge. If some of the support for the derived knowledge is revoked, then some of the derived certificates may be revoked as well. Cyclic support is avoided. Graph transformation rules are used for the management of the certificates, and we prove soundness and completeness for our model.

Local confluence is an important property in many rewriting and transformation systems. The notion of critical pairs is central for being able to verify local confluence of rewriting systems in a static way. Critical pairs are defined already in the framework of graphs and adhesive rewriting systems. These systems may hold rules with or without negative application conditions. In this paper however, we consider rules with more general application conditions — also called nested application conditions — which in the graph case are equivalent to finite first-order graph conditions. The classical critical pair notion denotes conflicting transformations in a minimal context satisfying the application conditions. This is no longer true for combinations of positive and negative application conditions — an important special case of nested ones — where we have to allow that critical pairs do not satisfy all the application conditions. This leads to a new notion of critical pairs which allows to formulate and prove a Local Confluence Theorem for the general case of rules with nested application conditions. We demonstrate this new theory on the modeling of an elevator control by a typed graph transformation system with positive and negative application conditions.

Amalgamation is a well-known concept for graph transformations in order to model synchronized parallelism of rules with shared subrules and corresponding transformations. This concept is especially important for an adequate formalization of the operational semantics of statecharts and other visual modeling languages, where typed attributed graphs are used for multiple rules with general application conditions. However, the theory of amalgamation for the double pushout approach has been developed up to now only on a set-theoretical basis for pairs of standard graph rules without any application conditions.

For this reason, we present the theory of amalgamation in this paper in the framework of adhesive categories for a bundle of rules with (nested) application conditions. In fact, it is also valid for weak adhesive HLR categories. The main result is the Multi-Amalgamation Theorem, which generalizes the well-known Parallelism and Amalgamation Theorems to the case of multiple synchronized parallelism.

The constructions are illustrated by a small running example. A more complex case study for the operational semantics of statecharts based on multi-amalgamation is presented in a separate paper.

The relation-algebraic approach to graph transformation replaces the universal category-theoretic characterisations of pushout and pullbacks with the local characterisations of tabulations and co-tabulations. The theory of collagories is a weak axiomatisation of relation-algebraic operations that closely corresponds to adhesive categories.

We show how to amalgamate double-pushout and double-pullback rewriting steps into a fused rewriting concept where rules can contain subgraph variables in a natural and flexible way, and rewriting can delete or duplicate the matched instances of such variables.

Given the success of the Doctoral Symposium held for the first time during ICGT in 2008 in Leicester, also this year a specific event of the International Conference on Graph Transformation was explicitly dedicated to Ph.D. students. The Doctoral Symposium consisted of technical sessions dedicated to presentations by doctoral students, held during the main conference, giving them a unique opportunity to present their research project and to interact with established researchers of the graph transformation community and with other students.

Model-driven software development is considered as a promising paradigm in software engineering [10].

Models are the central artifacts in model-driven development. Hence, inspecting and modifying models to reduce their complexity and improve their readability, maintainability and extensibility (i.e. by performing

model refactoring

[8]) are important issues of model development. Thus model transformation can be considered as one of the key activities in model-driven software development.

The theory of regular word languages has a large number of applications in computer science, especially in verification. The notion of regularity can be straightforwardly generalized to trees and tree automata. Therefore it is natural to ask for a theory of regular graph languages.

In contrast to computer systems, human behaviour is only predictable to a certain degree of probability. In semi-automated business processes human actors are guided by predetermined policies and regulations but retain the freedom to react to unforeseen events. For example, if an urgent prescription has to be dispensed by a pharmacist and the current pharmacist on duty is busy, it is likely that they would interrupt their current activity. The assignment policies in a model of this process should accurately define exception handling procedures in order to realistically simulate business processes. Other policies may require task assignment to the least-qualified person available to do the job if the people involved have different levels of access rights and qualifications.

The main focus of our work is to analyze and compare the behavior of graph transformation systems (GTSs). Therefore, we use the borrowed context technique to specify the behavior of a single graph with interface in different contexts. This mechanism is used to construct an LTS with graphs as states and rule applications as transitions. Each transition is labeled with the rule name and the borrowed context that is needed to perform the step. This makes the ideas of behavior comparison from LTS theory applicable to GTSs [1,9,6].

We propose first steps towards an extension of interaction nets for handling functions with side effects via monads.

The rising paradigm of model-driven development (MDD) promises to be a new technique to control the complexity of today’s software systems. However, increasing complexity may lead to large models which may justify a logical and/or physical distribution into several component models for better manageability. The concurrent development by distributed teams is desirable and already common practice in conventional software development. Naive solutions as storing all models in a central repository may not be adequate for distributed software development. E.g. Open Source Development is performed by distributed developer teams working in independent projects.

The aim of this PhD thesis is to use an extension of Petri nets and Petri net transformation systems called AHOI nets in order to allow formal modeling and analysis of communication platforms (CP) like Skype. In the following, we explain the main ideas of AHOI nets and discuss how they can be used to model features of Skype. We give an overview of results achieved so far and remaining open problems to be solved in this PhD thesis.

The behaviour of a computational device is often naturally defined by means of reduction semantics: a set representing the possible states of the device, and an unlabelled relation among them, usually inductively defined, representing the possible evolutions of the device. Despite the advantage of conveying the semantics with few compact rewriting rules, freely instantiated and contextualized, the main drawback of reduction-based solutions is that the dynamic behaviour of a system is described in a monolithic way, and so it can be interpreted only by inserting the system in appropriate contexts, where a reduction may take place.

Refactoring has emerged as a successful technique to enhance the internal structure of software by a series of small, behaviour-preserving transformations [4]. However, due to complex dependencies and conflicts between the individual refactorings, it is difficult to choose the best sequence of refactoring steps in order to effect a specific improvement. In the case of large systems the situation becomes acute because existing tools offer only limited support for their automated application [8]. Therefore, search-based approaches have been suggested in order to provide automation in discovering appropriate refactoring sequences [6,11]. The idea is to see the design process as a combinatorial optimization problem, attempting to derive the best solution (with respect to a quality measure called objective function) from a given initial design [9].

In (Pennemann 2009), the correctness of graph programs relative to nested graph conditions is considered. Since these conditions are expressively equivalent to first-order graph formulas, non-local graph properties in the sense of Gaifman are not expressible by nested graph conditions. We generalize the concept of nested graph conditions to socalled HR

 + 

conditions and investigate the correctness for graph programs relative to these generalized conditions.

Model transformations, utilized for various tasks, such as formal model analysis or code generation are key elements of model-driven development processes. As the complexity of developed model transformations grows, ensuring the correctness of transformation programs becomes increasingly difficult. Nonetheless, error detection is critical as errors can propagate into the target application.

In this abstract we present an overview of our intended approach for the verification of software written in imperative programming languages. This approach is based on model checking of graph transition systems (GTS), where each program state is modeled as a graph and the exploration engine is specified by graph transformation rules. We believe that graph transformation [13] is a very suitable technique to model the execution semantics of languages with dynamic memory allocation. Furthermore, such representation provides a clean setting to investigate the use of graph abstractions, which can mitigate the space state explosion problem that is inherent to model checking techniques.