In order to model the behaviour of open concurrent systems by means of Petri nets, we introduce open Petri nets, a generalization of the ordinary model where some places, designated as open, represent an interface of the system towards the environment. Besides generalizing the token game to reflect this extension, we define a truly concurrent semantics for open nets by extending the Goltz-Reisig process semantics of Petri nets. We introduce a composition operation over open nets, characterized as a pushout in the corresponding category, suitable to model both interaction through open places and synchronization of transitions. The deterministic process semantics is shown to be compositional with respect to such composition operation. If a net Z3 results as the composition of two nets Z1 and Z2, having a common subnet Z0, then any two deterministic processes of Z1 and Z2 which ``agreé' on the common part, can be ``amalgamated'' to produce a deterministic process of Z3. Vice versa, any deterministic process of Z3 can be decomposed into processes of the component nets. The amalgamation and decomposition operations are shown to be inverse to each other, leading to a bijective correspondence between the deterministic processes of Z3 and pair of deterministic processes of Z1 and Z2 which agree on the common subnet Z0. Technically, our result is similar to the amalgamation theorem for data-types in the framework of algebraic specification. A possible application field of the proposed constructions and results is the modeling of interorganizational workflows, recently studied in the literature. This is illustrated by a running example.

Visual languages (VLs) play a central role in modelling various system aspects. Besides standard languages like UML, a variety of domain-specific languages exist which are the more used the more tool support is available for them. Different kinds of generators have been developed which produce visual modelling environments based on VL specifications. To define a VL, declarative as well as constructive approaches are used. The meta modelling approach is a declarative one where classes of symbols and relations are defined and associated to each other. Constraints describe additional language properties. Defining a VL by a graph grammar, the constructive way is followed where graphs describe the abstract syntax of models and graph rules formulate the language grammar. In this paper, we extend algebraic graph grammars by a node type inheritance concept which opens up the possibility to integrate both approaches by identifying symbol classes with node types and associations with edge types of some graph class. In this way, declarative as well as constructive elements may be used for language definition and model manipulation. Two concrete approaches, the GenGED and the AToM3 approach, illustrate how VLs can be defined and models can be manipulated by the techniques described above.

Visual rewriting techniques are increasingly used to model transformations of systems specified through diagrammatic sentences. Graph transformations, in particular, are a widespread formalism with several applications, from parsing to model animation or transformation. Although a wealth of rewriting models have been proposed, differing in the expressivity of the types of rules and in the complexity of the rewriting mechanism, basic results concerning the formal properties of these models are still missing for many of them. In this paper, we propose a contribution towards solving the termination problem for rewriting systems with external control mechanisms for rule application. In particular, we obtain results of more general validity by extending the concept of transformation unit to high-level replacement systems, a generalization of graph transformation systems. For the resulting high-level replacement units, we state and prove several abstract properties based on termination criteria. Then, we instantiate the high-level replacement systems by attributed graph transformation systems and present concrete termination criteria. These are used to show the termination of some replacement units needed to express model transformations consequent to software refactoring.

During refactoring, the internal structure of a software system changes to improve its structure in support of subsequent reuse and maintenance, while preserving the behavior. To maintain the consistency between the code (represented as a flow graph) and the model given by several UML diagrams of different kinds, we propose a framework based on distributed graphs, where each refactoring is specified as a set of distributed graph transformations structured and organized into transformation units. This formalism could be used as the basis for important extensions to current refactoring tools.

Complex systems are characterized by components that may have to be described using different notations. For the analysis of such a system, our approach is to transform each component (preserving behaviour) into a single common formalism with appropriate analysis methods. Both source and target notations are described by means of meta-modelling whereas the translation is modelled by means of graph transformation. During the transformation process, the intermediate models can be a blend of elements of the source and target notations, but at the end the resulting model should be expressed in the target notation alone. In this work we propose defining also a meta-model for the intermediate process, in such a way that we can apply some validation methods to the transformation. In particular, we show how to prove functional behaviour (confluence and termination) via critical pair analysis and layering conditions, and discuss other desirable properties of the transformation, namely: syntactic consistency and behaviour preservation. The automation of these concepts has been carried out by combining the AToM3 and AGG tools.

This paper discusses the use of parallel graph transformation systems for (multi-formalism) modeling and simulation and their implementation in the meta-modeling tool AToM3. Parallel graph transformation is used to describe the application of rule schemes in an unknown context. This is important for obtaining general descriptions of the behavior of visual models like Petri nets. After reviewing the concepts of parallel graph transformation which is based on rule amalgamation according to certain rule interaction schemes, a simulator for Timed Transition Petri Nets is modeled using meta-modeling and parallel graph transformation. The extensions of AToM3 in order to support the definition and application of amalgamated rules are also discussed in the paper.

Motivated by recent work on the derivation of labelled transitions and bisimulation congruences from unlabelled reaction rules, we show how to solve this problem in the DPO (double-pushout) approach to graph rewriting. Unlike in previous approaches, we consider graphs as objects, instead of arrows, of the category under consideration. This allows us to present a very simple way of deriving labelled transitions (called rewriting steps with borrowed context) which smoothly integrates with the DPO approach, has a very constructive nature and requires only a minimum of category theory. The core part of this paper is the proof sketch that the bisimilarity based on rewriting with borrowed contexts is a congruence relation.

Graph constraints and application conditions are most important for graph grammars and transformation systems in a large variety of application areas. Although different approaches have been presented in the literature already there is no adequate theory up to now which can be applied to different kinds of graphs and high-level structures. In this paper, we introduce an improved notion of graph constraints and application conditions and show under what conditions the basic results can be extended from graph transformation to high-level replacement systems. In fact, we use the new framework of adhesive HLR categories recently introduced as combination of HLR systems and adhesive categories. Our main results are the transformation of graph constraints into right application conditions and the transformation from right to left application conditions in this new framework.

Adhesive high-level replacement (HLR) categories and systems are introduced as a new categorical framework for graph transformation in a broad sense, which combines the well-known concept of HLR systems with the new concept of adhesive categories introduced by Lack and Sobocinski. In this paper we show that most of the HLR properties, which had been introduced ad hoc to generalize some basic results from the category of graphs to high-level structures, are valid already in adhesive HLR categories. As a main new result in a categorical framework we show the Critical Pair Lemma for local con uence of transformations. Moreover we present a new version of embeddings and extensions for transformations in our framework of adhesive HLR systems.

The aim of this paper is to present a generic component framework for system modeling that satisfies main requirements for component-based development in software engineering. In this sense, we have defined a framework that can be used, by providing an adequate instantiation, in connection with a large class of semi-formal and formal modeling techniques. Moreover, the framework is also flexible with respect to the connection of components, providing a compositional semantics of components. This means more precisely that the semantics of a system can be inferred from the semantics of its components.

The relationship between graph grammars and Petri nets is the topic of this workshop with the emphasis on work in progress and especially the transfer of concepts between both areas. Both areas are prominent specification formalisms for concurrent and distributed systems. The workshop brings together people working especially in the area of low-level and high-level Petri nets and in the area of graph transformation and high-level replacement systems. According to the main idea and in order to further stimulate the research in this important area, this workshop triggers discussion and transfer of concepts across the borders of these and related research fields.

The concept of typed attributed graph transformation is most significant for modeling and meta modeling in software engineering and visual languages, but up to now there is no adequate theory for this important branch of graph transformation. In this paper we give a new formalization of typed attributed graphs, which allows node and edge attribution. The first main result shows that the corresponding category is isomorphic to the category of algebras over a specific kind of attributed graph structure signature. This allows to prove the second main result showing that the category of typed attributed graphs is an instance of adhesive HLR categories . This new concept combines adhesive categories introduced by Lack and Sobocinski with the well-known approach of high-level replacement (HLR) systems using a new simplified version of HLR conditions. As a consequence we obtain a rigorous approach to typed attributed graph transformation providing as fundamental results the Local Church-Rosser, Parallelism, Concurrency, Embedding and Extension Theorem and a Local Confluence Theorem known as Critical Pair Lemma in the literature.

This work discusses the state-of-the-art of visual editor generation based on graph transformation concepts on one hand, and using the Eclipse technology which includes the Graphical Editor Framework (GEF), on the other hand. Due to existing shortcomings in both approaches, we present a combined approach for a tool environment that allows to generate a GEF-based editor from a formal, graph-transformation based visual language specification.

Attributed graphs and typing play an important role in theory and applications of graph grammars, graph transformation systems, visual languages and metamodelling. Attributed graphs can be represented basically as pairs of graphs and algebras on one hand and as algebras of suitable algebraic signatures on the other hand. In this note the different notions are compared on the syntactical and on the semantical level. Two different kinds of algebraic signatures for attributed algebras are discussed leading to different results on both levels. In the case of attributed graph signatures the corresponding category of algebras is isomorphic to the category of typed attributed graphs, while we have only a non-surjective functor in the more general case of attributed algebras for graph structure signatures. An overview of all results is given in the last section of this paper.

Visualizing and simulating formal models in a flexible way becomes increasingly important for the design of complex systems. With GenGED, a tool is available which automatically generates a visual environment to process (create, edit, check, simulate) visual models over a specified visual language. Both the specification of the language and the model manipulation are based on graph grammars. In this paper, we present the means to transform visual models into application oriented views, called scenario views. We show how a model is consistently transferred to a scenario views and animated there. The extension of GenGED concerning scenario animation is discussed.

Visualizing and simulating the behavior of formal models in an adequate and flexible way becomes increasingly important for the design and validation of complex systems. Using graph transformation, the concrete and abstract syntax of various visual modelling languages can be described, and the semantics can be formalized. Moreover, graph transformation tools support visual model specification, simulation and analysis on the basis of the rich underlying theory. Despite these benefits, often the simulation of formal visual behavior models (e.g. Petri nets or statecharts) is not flexible enough and results in an ineffective validation process. In this paper we propose a formal, view-based approach to simulate and animate the behavior of visual models at different abstraction levels on the basis of typed, attributed graph transformation. We introduce so-called animation views, which allow to define scenario animations for a given behavior model in a systematic way. Based on the visual language definition for Algebraic High-Level Petri nets, the well-known specification of The Dining Philosophers serves as running example for the definition of an animation view and a scenario animation which directly visualizes the behavior of the dining philosophers sitting around a table. A prototypical implementation of the concepts for view definition, view transformation, simulation and scenario animation as new features of GenGEDp , an environment for the definition of visual languages and the specification and simulation of visual behavior models, is presented.

A policy is a set of rules that controls the behavior of complex systems. In [icgt04] a policy framework based on graph transformations is presented providing an intuitive visual formalism for the manipulation of policy-based systems. The policy framework is defined by a type graph and sets of policy rules, positive and negative constraints, resp. Mobile policies have the additional capability to move around with the object e.g between different companies. We investigate how the distribution and modification of mobile policies can be modeled with Algebraic Higher-Order (AHO) nets, a high-level net class which is an extension of Petri nets by concepts of the higher-order specification language HasCASL. Due to the higher-order features graphs and rules are allowed to be dynamical objects in AHO-nets and the behavior of an AHO-net simulates the modification needed to achieve the flexibility of adapting objects. For our purpose, the AHO-net gives an overview of the different locations where the mobile policies could reside. Furthermore, the coupling of a set of rules which are used to modify the mobile policies, to certain locations, which have the authority to modify the mobile policies, is given by the net topology. Technically, we extent the HasCASL-specification of rule-based modifications on the one hand by adding negative application conditions and on the other hand by using specific operations for the modification of mobile policies.

A nondeterministic finite automaton with e-transitions (eNFA) accepts a regular language. Among the eNFA accepting a certain language some are more compact than others. This essay treats the problem how to compactify a given eNFA by reducing the number of transitions. Compared to the standard techniques to minimize deterministic complete finite automata (complete DFA) two novel features matter in compactifying eNFA: the principle of transition partition and the principle of transition union. An algorithm for compactifying eNFA is presented that exploits the union principle. This algorithm has the following property: if the algorithm returns an unambiguous automaton, then this automaton is the transition minimal eNFA.

Motivated by the wide acceptance of component based technologies in software development it is shown by example, how to apply component concepts for software engineering to modeling in the field of production automation. Taking the modeling of a holonic transport system as an example, it is shown how functionblocks in the sense of production automation can be understood as software engineering components. Thus, the advantages of component based modeling with respect to structuring, exchange and reuse can be transferred to systems in production automation.

GTXL (Graph Transformation Exchange Language) is designed to support and stimulate developers to provide their graph transformation-based tools with an exchange functionality regarding the integration with other tools. For this exchange XML was chosen as underlying technology. The exchange of graphs is facilitated by the exchange format GXL which is also XML-based. GTXL uses GXL to describe the graph parts of a graph transformation system. A first version of GTXL arose from the format discussion within the EU Working Group APPLIGRAPH. Trying to restimulate the discussion on a common exchange format for graph transformation systems, this paper presents a new version of GTXL. Three important changes have been made. At first, an integrated presentation of rules is introduced, secondly the expression of more general conditions is supported and finally the storage of the underlying semantics of a graph transformation system by means of special attributes is proposed.

Graphs are well-known, well-understood, and frequently used means to depict networks of related items. They are successfully used as the underlying mathematical concept in various application domains. In all these domains, tools are developed that store, retrieve, manipulate and display graphs. It is the purpose of this workshop to summarize the state of the art of graph-based tool development, bring together developers of graph-based tools in different application fields and to encourage new tool development cooperations.

Refactorings are program transformations that improve the software structure while preserving the external behaviour. In spite of this very useful property, refactorings can still give rise to structural conflicts when parallel evolutions to the same software are made by different developers. This paper explores this problem of structural evolution conflicts in a formal way by using graph transformation and critical pair analysis. Based on experiments carried out in the graph transformation tool AGG, we show how this formalism can be exploited to detect and resolve refactoring conflicts.

This paper introduces safety properties in the temporal logic sense to Petri net modules. Petri net moduleshave been achieved by a transfer of algebraic specification modules to Petri nets. They consist of three nets; the interface nets import and export, and the body of the module. The import net states the prerequisites the modules assumes. The body net represents the internal functionality. The export net gives an abstraction of the body that can be used by the environment. The interfaces IMP and EXP are related to the body BOD via morphisms. These modules conform with the basic concepts of components and component-based systems of Continuous Software Engineering (CSE). We make precise what it means that a Petri net module has specific safety properties. We differentiate between explicit and implicit properties. Explicit safety properties are stated additionally to the export net. Implicit are those properties that hold in the export net without being stated explicitly.The main advantage of our approach are module operations to compose larger modules from basic ones. We can show that the composition of modules preserves safety properties: Given two modules with implicit or explicit safety properties then the composition of these modules is again a module with implicit or explicit safety properties.

The paper addresses the problem of how to create a coherent application out of a series of independent Web pages. We provide a modelling approach for powerful and flexible Web session management based on UML. We propose the definition of a session model concerning consistency issues. The validation of a session model is possible due to the formal basis of our approach using graph transformation.

The role of the viewpoint concept, known from software engineering, is of increasing importance for modeling in production automation. While most often only a syntactical consistency check is performed for viewpoint oriented modeling techniques, this work examines semantical consistency. Semantical modeling and model based consistency checks are presented along an example of a machining tool robot.

AGG is a general development environment for algebraic graph transformation systems which follows the interpretative approach. Its special power comes from a very flexible attribution concept. AGG graphs are allowed to be attributed by any kind of Java objects. Graph transformations can be equipped with arbitrary computations on these Java objects described by a Java expression. The AGG environment consists of a graphical user interface comprising several visual editors, an interpreter, and a set of validation tools. The interpreter allows the stepwise transformation of graphs as well as rule applications as long as possible. AGG supports several kinds of validations which comprise graph parsing, consistency checking of graphs and conflict detection in concurrent transformations by critical pair analysis of graph rules. Applications of AGG include graph and rule-based modeling of software, validation of system properties by assigning a graph transformation based semantics to some system model, graph transformation based evolution of software, and the definition of visual languages based on graph grammars.