Search

We introduce an extension of Graph Grammars (GGs), called Dynamic Graph Grammars (DynGGs), where the right-hand side of a production can spawn fresh parts of the type graph and fresh productions operating on it. The features of DynGGs make them suitable for the straightforward modeling of reflexive mobile systems like dynamic nets and the Join calculus. Our main result shows that each DynGG can be modeled as a (finite) GG, so that the dynamically generated structure can be typed statically, still preserving exactly all derivations. [ABSTRACT FROM AUTHOR]

Model-based tool data transformation and integration are crucial tasks in software and system development relying on model-driven development (MDD). Since the tool-specific meta models of the involved system development tools are often too generic and lack the desired level of abstraction, it is inappropriate to specify model transformation and integration rules on top of them. Domain-specific views on tool-specific meta models are needed which provide meaningful information on a higher level of abstraction. Current approaches usually consider a view as a separate model which has to be kept consistent with the tool's model and, thus, duplicate the data. In this paper we discuss different implementations of our declarative view specification approach called VTGG that are based on modified triple graph grammars. As a result we come up with an implementation with non-materialized views that avoids the duplication of data. [ABSTRACT FROM AUTHOR]

In proof theory, a standard method for showing the correctness of a program w.r.t. given pre- and postconditions is to construct a weakest precondition and to show that the precondition implies the weakest precondition. In this paper, graph programs in the sense of Habel and Plump 2001 are extended to programs over high-level rules with application conditions, a formal definition of weakest preconditions for high-level programs in the sense of Dijkstra 1975 is given, and a construction of weakest preconditions is presented. [ABSTRACT FROM AUTHOR]

In this paper, we consider high-level structures like graphs, Petri nets, and algebraic specifications and investigate two kinds of satisfiability of conditions and two kinds of rule matching over these structures. We show that, for weak adhesive HLR categories with class ${\mathcal{A}}$ of all morphisms and a class ${\mathcal {M}}$ of monomorphisms, strictly closed under decompositions, ${\mathcal{A}}$- and ${\mathcal{M}}$-satisfiability and ${\mathcal{A}}$- and $P{\mathcal{M}}$-matching are expressively equivalent. The results are applied to the category of graphs, where ${\mathcal{M}}$ is the class of all injective graph morphisms. [ABSTRACT FROM AUTHOR]

Graph rewriting is a powerful technique that requires graph pattern matching, which is an NP-complete problem. We present GrGen, a generative programming system for graph rewriting, which applies heuristic optimizations. According to Varró's benchmark it is at least one order of magnitude faster than any other tool known to us. Our graph rewriting tool implements the well-founded single-pushout approach. We define the notion of search plans to represent different matching strategies and equip these search plans with a cost model, taking the present host graph into account. The task of selecting a good search plan is then viewed as an optimization problem. For the ease of use, GrGen features an expressive specification language and generates program code with a convenient interface. [ABSTRACT FROM AUTHOR]

This paper studies two realizations of graph transformations which are based on a UML class diagram. The first realization achieves a representation in terms of descriptive pre- and postconditions. The second one yields an operationally executable command sequence in terms of basic commands for object and link creation, attribute modification, and object and link destruction. Our aim for realizing graph transformations in terms of target languages offering different views, i.e., descriptive or operational, is to take advantage of both views and to utilize the benefits which both views provide. [ABSTRACT FROM AUTHOR]

Graphs are suitable modeling formalisms for software and hardware systems involving aspects such as communication, object orientation, concurrency, mobility and distribution. State spaces of such systems can be represented by graph transition systems, which are basically transition systems whose states and transitions represent graphs and graph morphisms. Heuristic search is a successful Artificial Intelligence technique for solving exploration problems implicitly present in games, planning, and formal verification. Heuristic search exploits information about the problem being solved to guide the exploration process. The main benefits are significant reductions in the search effort and the size of solutions. We propose the application of heuristic search for the analysis of graph transition systems. We define algorithms and heuristics and present experimental results. [ABSTRACT FROM AUTHOR]

We present conditions under which graph transformation rules can be applied in time independent of the size of the input graph: graphs must contain a unique root label, nodes in the left-hand sides of rules must be reachable from the root, and nodes must have a bounded outdegree. We establish a constant upper bound for the time needed to construct all graphs resulting from an application of a fixed rule to an input graph. We also give an improved upper bound under the stronger condition that all edges outgoing from a node must have distinct labels. Then this result is applied to identify a class of graph reduction systems that define graph languages with a linear membership test. In a case study we prove that the (non-context-free) language of balanced binary trees with backpointers belongs to this class. [ABSTRACT FROM AUTHOR]

In this paper, we present our approach for model view management in the context of Multi-View Visual Languages (MVVLs). These are made of a number of diagram types (or viewpoints) that can be used for the specification of the different aspects of a system. Therefore, the user can build different system views conform to the viewpoints, which are merged in a repository in order to perform consistency checking. In addition, the user can define derived views by means of graph query patterns in order to extract information from a base model (a system view or the repository). We have provided automatic mechanisms to keep synchronized the base model and the derived view when the former changes. Predefined queries by the MVVL designer result in so-called audience-oriented views. Finally, semantic views are used for analysing the system by its translation into a semantic domain. Our approach is based on meta-modelling to describe the syntax of the MVVL and each viewpoint, and on triple graph transformation systems to synchronize and maintain correspondences between the system views and the repository, as well as between the derived, audience-oriented and semantic views and the base models. We illustrate these concepts by means of an example in the domain of security for web systems. [ABSTRACT FROM AUTHOR]

The model-driven development (MDD) approach for constructing software systems advocates a stepwise refinement and transformation process starting from high-level models to concrete program code. In contrast to numerous research efforts that try to generate executable function code from models, we propose a novel approach termed model-driven monitoring. Here, models are used to specify minimal requirements and are transformed into assertions on the code level for monitoring hand-coded programs during execution. We show how well-understood results from the graph transformation community can be deployed to support this model-driven monitoring approach. In particular, models in the form of visual contracts are defined by graph transitions with loose semantics, while the automatic transformation from models to JML assertions on the code level is defined by strict graph transformation rules. Both aspects are supported and realized by a dedicated Eclipse plug-in. [ABSTRACT FROM AUTHOR]

Graph transformation techniques have already been used successfully by several research groups to support re-engineering of large legacy systems. Where others often aim at transforming the system to improve it, we advocate an evolutionary approach that embeds transformations within the ordinary development process and provides tool support to monitor the ongoing progress regularly. In this paper, we discuss how temporal graph queries based on Fujaba story diagrams can provide a natural means to express trend-oriented metrics and consistency rules that we identified in our industrial case studies. To this end, we discuss a first-order logic rather than operational interpretation of a graph queries and show how well-known temporal logic operators can be added to express rules over consecutive states of the same instance graph. [ABSTRACT FROM AUTHOR]

This paper proposes a methodology to analyze graph transformation systems by means of Alloy and its supporting tools. Alloy is a simple structural modeling language, based on first-order logic, that allows the user to produce models of software systems by abstracting their key characteristics. The tools can generate instances of invariants, and check properties of models, on user-constrained representations of the world under analysis. The paper describes how to render a graph transformation system —specified using AGG— as an Alloy model and how to exploit its tools to prove significant properties of the system. Specifically, it allows the user to decide whether a given configuration (graph) can be obtained through a finite and bounded sequence of steps (invocation of rules), whether a given sequence of rules can be applied on an initial graph, and, given an initial graph and an integer n, which are the configurations that can be obtained by applying a sequence of n (particular) rules. [ABSTRACT FROM AUTHOR]

Despite the increasing relevance of model transformation techniques in model-driven software development, research is mainly conducted to the specification and the automation of such transformations. However, since the transformations themselves may also contain conceptual flaws, it is essential to formally analyze them prior to executing them on user models. In the current paper, we focus on a central validation problem of trusted model transformations, namely, termination and propose a Petri net based analysis method that provides a sufficient criterion for the termination problem of model transformations captured by graph transformation systems. Keywords: graph transformation, termination, model transformation, Petri nets. [ABSTRACT FROM AUTHOR]

In unreliable environments, e.g. wireless networks, often there are messages lost, connection and process crashes, among other undesirable fault occurrences. Mechanisms to enhance the dependability of these systems can be employed, but with a performance cost. Analytical approaches are useful to predict performance and dependability values, guiding the system developer to adjust bounds for specific requirements in complex systems. In this paper we use non-functional analysis of Stochastic Object-Based Graph Grammars (SOBGG) models considering classical fault behaviors in distributed systems, allowing the developer to predict performance and dependability values for high performance and resilient systems. The specific contributions of this paper are: (i) revisit the notion of fault representation to allow non-functional analysis, more specifically, steady-state analysis; (ii) discuss the specification of rates associated to SOBGG rules, describing an adequate approach to distributed systems; (iii) show the suitability of the proposed techniques through their application to a case study. Keywords: Object-based graph grammars, distributed systems, fault-tolerance, non-functional analysis, dependability. [ABSTRACT FROM AUTHOR]

In this paper, we introduce the notion of a community of autonomous units as a rule-based and graph-transformational device to model processes that run interactively but independently of each other in a common environment. The emphasis of the approach is laid on the study of the formal semantics of a community as a whole and of each of its member units separately. We concentrate on the sequential case where only one unit can act at a time and the rule applications of the involved units are interleaved with each other. [ABSTRACT FROM AUTHOR]

A distributed graph (N,D) consists of a network graph N and a commutative diagram D over the scheme N which associates local graphs D(ni) and graph morphisms D(e): D(n1) →D(n2) to nodes n1, n2 and edges e: n1 →n2 in N. Although there are several interesting applications of distributed graphs and transformations, even the basic pushout constructions for the double pushout approach of distributed graph transformation could be shown up to now only in very special cases. In this paper we show that the category of distributed graphs can be considered as a Grothendieck category over a specific indexed category, which assigns to each network N the category of all diagrams D of shape N. In this framework it is possible to give a free construction which allows to construct for each diagram D1 over N1 and network morphism h:N1 →N2 a free extension Fh(D1) over N2 and to show that the Grothendieck category is complete and cocomplete if the underlying category of local graphs has these properties. Moreover, an explicit construction for general pushouts of distributed graphs is given. This pushout construction is based on the free construction. The non-trivial proofs for free constructions and pushouts are the main contributions of this paper and they are compared with the special cases known up to now. [ABSTRACT FROM AUTHOR]

The paper presents a case study on the synthesis of labelled transition systems (ltss) for process calculi, choosing as testbed Milner's Calculus of Communicating System (ccs). The proposal is based on a graphical encoding: each ccs process is mapped into a graph equipped with suitable interfaces, such that the denotation is fully abstract with respect to the usual structural congruence. Graphs with interfaces are amenable to the synthesis mechanism based on borrowed contexts (bcs), proposed by Ehrig and König (which are an instance of relative pushouts, originally introduced by Milner and Leifer). The bc mechanism allows the effective construction of an lts that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence. Our paper focuses on the analysis of the lts distilled by exploiting the encoding of ccs processes: besides offering some technical contributions towards the simplification of the bc mechanism, the key result of our work is the proof that the bisimilarity on processes obtained via bcs coincides with the standard strong bisimilarity for ccs. [ABSTRACT FROM AUTHOR]

Transactional graph transformation systems (t-gtss) have been recently proposed as a mild extension of the standard dpo approach to graph transformation, equipping it with a suitable notion of atomic execution for computations. A typing mechanism induces a distinction between stable and unstable items, and a transaction is defined as a shift-equivalence class of computations such that the starting and ending states are stable and all the intermediate states are unstable. The paper introduces an equivalent, yet more manageable definition of transaction based on graph processes. This presentation is used to provide a universal characterisation for the class of transactions of a given t-gts. More specifically, we show that the functor mapping a t-gts to a graph transformation system having as productions exactly the transactions of the original t-gts is the right adjoint to an inclusion functor. Keywords: Graph processes, refinement, transactions, zero-safe nets. [ABSTRACT FROM AUTHOR]

Double-pushout (DPO) transformations with borrowed context extend the standard DPO approach by allowing part of the graph needed in a transformation to be borrowed from the environment. The bisimilarity based on the observation of borrowed contexts is a congruence, thus facilitating system analysis. In this paper, focusing on the situation in which the states of a global system are built out of local components, we show that DPO transformations with borrowed context defined on a global system state can be decomposed into corresponding transformations on the local states and vice versa. Such composition and decomposition theorems, developed in the framework of adhesive categories, can be seen as a first step towards an inductive definition, in sos style, of the labelled transition system associated to a graph transformation system. As a special case we show how an ordinary DPO transformation on a global system state can be decomposed into local DPO transformations with borrowed context using the same production. [ABSTRACT FROM AUTHOR]

Adhesive categories have recently been proposed as a categorical foundation for facets of the theory of graph transformation, and have also been used to study techniques from process algebra for reasoning about concurrency. Here we continue our study of adhesive categories by showing that toposes are adhesive. The proof relies on exploiting the relationship between adhesive categories, Brown and Janelidze's work on generalised van Kampen theorems as well as Grothendieck's theory of descent. [ABSTRACT FROM AUTHOR]

In this work we present our approach to (simple di-)graph transformation based on an algebra of boolean matrices. Rules are represented as boolean matrices for nodes and edges and derivations can be efficiently characterized with boolean operations only. Our objective is to analyze properties inherent to rules themselves (without considering an initial graph), so this information can be calculated at specification time. We present basic results concerning well-formedness of rules and derivations (compatibility), as well as concatenation of rules, the conditions under which they are applicable (coherence) and permutations. We introduce the match, which permits the identification of a grammar rule left hand side inside a graph. We follow a similar approach to the single pushout approach (SPO), where dangling edges are deleted, but we first adapt the rule in order to take into account any deleted edge. To this end, a notation borrowed from functional analysis is used. We study the conditions under which the calculated data at specification time can be used when the match is considered. [ABSTRACT FROM AUTHOR]

Discontinuous constituents and free word order pose constant problems in natural language parsing. String generating hypergraph grammars have been proven useful for handling discontinuous constituents. In this paper we describe a new notation for hypergraph productions that allows on-the-fly interconnection of graph parts with regard to user-defined constraints. These constraints handle the order of nodes within the string hypergraph. The HyperEarley parser for string generating hypergraph grammars [1] is adapted to the new formalism. A German example is used for the explanation of the new notation and algorithms. [ABSTRACT FROM AUTHOR]

Metabolic pathway analysis is one of the tools used in biology and medicine in order to understand reaction cycles in living cells. A shortcoming of the approach, however, is that reactions are analysed only at a level corresponding to what is known as the 'collective token view' in Petri nets, i.e., summarising the number of atoms of certain types in a compound, but not keeping track of their identity. In this paper we propose a refinement of pathway analysis based on hypergraph grammars, modelling reactions at a molecular level. We consider as an example the citric acid cycle, a classical, but non-trivial reaction for energy utilisation in living cells. Our approach allows the molecular analysis of the cycle, tracing the flow of individual carbon atoms based on a simulation using the graph transformation tool AGG. [ABSTRACT FROM AUTHOR]

We investigate the narrowing relation in a wide class of (cyclic) term-graph rewrite systems. We propose a new sound and complete narrowing-based algorithm able to solve goals in presence of data structures with pointers (e.g., circular lists, doubly linked lists etc.). We first define the class of rewrite systems we consider. Our rules provide features such as pointer (edge) redirections, relabeling of existing nodes, in addition to the creation of new nodes. Moreover, we split the set of nodes of term-graphs in two (possibly empty) subsets: (i) variables and (ii) names. Variable nodes can be mapped against any other node whereas names act as constants and thus they are supposed to match themselves. This distinction between nodes allows us to synthesize, through the narrowing process, data-structures with circular shapes. In a second step, we define the rewriting and narrowing relations. We then show the soundness and completeness of narrowing. [ABSTRACT FROM AUTHOR]

We propose an extension of node and hyperedge replacement grammars, called adaptive star grammars, and study their basic properties. A rule in an adaptive star grammar is actually a rule schema which, via the so-called cloning operation, yields a potentially infinite number of concrete rules. Adaptive star grammars are motivated by application areas such as modeling and refactoring object-oriented programs. We prove that cloning can be applied lazily. Unrestricted adaptive star grammars are shown to be capable of generating every type-0 string language. However, we identify a reasonably large subclass for which the membership problem is decidable. [ABSTRACT FROM AUTHOR]

This paper introduces a new theory needed for the purpose of conflict detection for graph transformation with negative application conditions (NACs). Main results are the formulation of a conflict notion for graph transformation with NACs and a conflict characterization derived from it. A critical pair definition is introduced and completeness of the set of all critical pairs is shown. This means that for each conflict, occuring in a graph transformation system with NACs, there exists a critical pair expressing the same conflict in a minimal context. Moreover a necessary and sufficient condition is presented for parallel independence of graph transformation systems with NACs. In order to facilitate the implementation of the critical pair construction for a graph transformation system with NACs a correct construction is formulated. Finally, it is discussed how to continue with the development of conflict detection and analysis techniques in the near future. [ABSTRACT FROM AUTHOR]

We investigate two models of finite-state automata that operate on rooted directed graphs by marking either vertices (V-automata) or edges (E-automata). Runs correspond to locally consistent markings and acceptance is defined by means of regular conditions on the paths emanating from the root. Comparing the expressive power of these two notions of graph acceptors, we show that E-automata are more expressive than V-automata. Moreover, we prove that E-automata are at least as expressive as the μ-calculus. Our main result implies that every MSO-definable tree language can be recognised by E-automata with uniform runs, that is, runs that do not distinguish between isomorphic subtrees. [ABSTRACT FROM AUTHOR]

Sesqui-pushout (SqPO) rewriting—"sesqui" means "one and a half" in Latin—is a new algebraic approach to abstract rewriting in any category. SqPO rewriting is a deterministic and conservative extension of double-pushout (dpo) rewriting, which allows to model "deletion in unknown context", a typical feature of single-pushout (spo) rewriting, as well as cloning. After illustrating the expressiveness of the proposed approach through a case study modelling an access control system, we discuss sufficient conditions for the existence of final pullback complements and we analyze the relationship between SqPO and the classical dpo and spo approaches. [ABSTRACT FROM AUTHOR]

Reference counting is a simple and efficient way of performing graph transformation and management in which each graph node stores the number of pointers to it. Graph operations are performed in such a way to keep this property invariant. The major drawback of standard reference counting is its inability to work with cyclic structures, which appear ever so often in real applications. The author of this talk developed a series of cyclic reference counting algorithms whose applicability goes far beyond the implementation of garbage collectors in programming languages. This paper presents the milestones in the history of cyclic reference counting followed by two new applications: the consistent management of Web pages in the Internet and the correctly handling of processes in clusters and grids. Keywords: cyclic graphs, reference counting, webpage management, process management. [ABSTRACT FROM AUTHOR]

In this paper we describe a way to integrate Taentzer's rule amalgamation with the recently proposed notions of nested graph conditions. The resulting so-called quantified graph transformation rules include (universally and existentially) quantified sub-structures in a flexible way. This can be used for instance to specify a larger-step operational semantics, thus improving the scalability of graph transformation as a technique for software verification. [ABSTRACT FROM AUTHOR]

Understanding biochemical pathways is one of the big challenges of the field of molecular biology nowadays. Computer science can contribute in this area in a variety of ways. One of them is providing formalisms and tools to simulate and check properties of pathways. One formalism that is well known and suited for modeling concurrent and distributed systems is Milner's Calculus of Communicating Systems (CCS). CCS is a process algebra and there are many tools that support modeling and automatic verification of properties of systems modeled in terms of CCS processes. This paper describes the regulation of the lactose operon using CCS. We validate our formal model by automatic checking a series of properties that are known for the regulation of the lactose. Thus, we show the viability of using process algebras to model and reason about biochemical networks. [ABSTRACT FROM AUTHOR]

In this paper we present a framework for developing concurrent object-based systems. The framework is based on graph grammars and includes techniques for specification, simulation, animation and verification. [ABSTRACT FROM AUTHOR]

The main aim of this paper is to analyze the similarities and differences between graph grammars and Petri nets. Particularly we compare the high-level versions of nets and grammars, namely AHL nets and attributed graph grammars and the corresponding flattening constructions to PT nets and labeled graph grammars, and show that these flattenings are compatible (syntactically and semantically) with the translations of nets to grammars. Thus Petri nets are equivalent to their graph grammar translations. Due to the fact that graphs correspond to sets of tokens, Petri nets can syntactically be considered as special (simple) graph grammars. In their basic semantics however this is not precisely true: tokens without individuality are in contrast to corresponding vertices showing individuality. (Reachability and derivation) Trees have been chosen as a common semantical domain. [ABSTRACT FROM AUTHOR]

Transformation-based techniques such as refactoring, model transformation and model-driven development, architectural reconfiguration, etc. are at the heart of many software engineering activities, making it possible to cope with an ever changing environment. This workshop provides a forum for discussing these techniques, their formal foundations and applications. [ABSTRACT FROM AUTHOR]

The Workshop on Petri Nets and Graph Transformations, which is currently at its second edition, is focussed on the mutual relationship between two prominent specification formalisms for concurrency and distribution, namely Petri nets and graph transformation systems. It belongs to the folklore that Petri nets can be seen as rewriting systems over (multi)sets, the rewriting rules being the transitions, and, as such, they can be seen as special graph transformation systems, acting over labelled discrete graphs. The basic notions of Petri nets like marking, enabling, firing, steps and step sequences can be naturally "translated" to corresponding notions of graph transformation systems. Due to this close correspondence there has been a mutual influence between the two fields, which has lead to a fruitful cross-fertilisation. [ABSTRACT FROM AUTHOR]

The International Workshop on Graph Based Tools (GraBaTs 2006) is the third workshop of a series that serves as a forum for researchers and practitioners interested in the development and application of graph-based tools. Based upon mathematically solid underlying concepts, graph-based tools are frequently used in various application areas in software and systems engineering. [ABSTRACT FROM AUTHOR]

A variety of computation models have been developed using graphs and graph transformations. These include models for sequential, distributed, parallel or mobile computation. A graph may represent, in an abstract way, the underlying structure of a computer system, or it may stand for the computation steps running on such a system. In the former, the computation can be carried on the corresponding graph, implying a simplification of the complexity of the system. The aim of the workshop is to bring together researchers interested in all aspects of computation models based on graphs, and their applications. A particular emphasis will be made for models and tools describing general solutions. The workshop will include contributed papers, tutorials and tool demonstrations. [ABSTRACT FROM AUTHOR]

This tutorial is intended as a general introduction to graph transformation for scientists who are not familiar with the field. The tutorial will start with an informal introduction to the basic concepts like graph, rule, transformation, etc., discussing semantic choices like which notion of graph to use; how to put labels, attributes, or types; or what to do with dangling links during rewriting, etc., and mentioning different ways to formalise the basic concepts. In the second part, the tutorial will give a survey of typical applications of graph transformation in software engineering, e.g., as a specification language and semantic model for concurrent and distributed systems, as a meta language for defining the syntax, semantics, and manipulation of diagrams, etc. Finally, the tutorial will go into some details about the algebraic approach to graph transformation, its formal foundations and relevant theory and tools. This shall enable the participants to better appreciate the conference and its satellite events. [ABSTRACT FROM AUTHOR]

Most modeling languages embody a particular idiom: the state/invariant/operations idiom for VDM and Z; the variable-update/temporal-logic idiom for SMV and Murphi; the imperative-programming idiom for Promela and Zing; and so on. Fixing an idiom makes tools easier to build, and helps novice modellers. But it also makes the language less flexible. [ABSTRACT FROM AUTHOR]