Preface: UNIGRA''03 - Uniform Approaches to Graphical Process Specification Techniques

This volume contains selected papers of the proceedings of the workshop on Uniform Approaches to Graphical Process Specification Techniques (UNIGRA'03). The workshop was held in Warsaw, Poland, on April 5 and 6, 2003, as a satellite event of the sixth European Joint Conference on Theory and Practice of Software (ETAPS 2003). The workshop continues the UNIGRA workshop in 2001 which has been a successful satellite event of ETAPS 2001.Workshop ObjectivesDue to the increasing amount of divergent formalisms, the main idea of the UNIGRA workshops is to bring together people working especially in the following three areas:

• Low Level and High-Level Petri Nets

• Graph Transformation and High-Level Replacement Systems

• Visual Modeling Techniques including UML

In each of these areas there is a large variety of different approaches, however, first attempts for uniform approaches have been made already. According to the main idea and in order to further stimulate the research in this important area, this volume presents some uniform approaches and further introduce unifying and comparative studies across the borders of the three and related areas.Workshop ProgramIn the first part, unifying approaches for low-level and high-level Petri nets are proposed:The contribution by Ehrig shows how the notions occurrence net and process can be generalized from low-level to high-level Petri nets, and studies the behavior and instantiations of this new view of processes for high-level nets.In his overview on new developments in the area of Petri net transformations for Software Engineering, Urbášek presents recent work on net model transformations and net class transformations. Both kinds of transformations are studied with regard to the preservation of system properties such as safety properties or liveness. The formalization of Petri net transformations is originally based on the theory of graph transformation.Padberg considers a case study (the call center of a phone company)which is modeled using Petri net modules for structuring the operational behavior of the system. The notion of Petri net modules was achieved by a transfer from the concepts of algebraic module specifications to the modeling of component-based systems by Petri nets.Desel, Juhás and Lorenz deal with the semantics of place/transition nets. The authors relate the process semantics based on partial orders (individual token semantics) to the collective token semantics by defining partial orders associated to process terms of place/transition nets.In the second part concerning graph transformation and high-level replacement systems, new aspects of component modeling and application of graph transformation techniques are discussed:In their contribution on components for algebra transformation systems, Ehrig and Orejas define a component transformation semantics in terms of the semantics of the specifications included in the components. The underlying formal basis of the instantiation of their generic component framework are algebra transformation systems and high-level replacement rules.An application of the formal unifying framework of distributed transformation units is presented by Kuske and Knirsch. The authors illustrate how different features of agent systems can be modeled by distributed graph transformation systems in a uniform way.Another application for graph rewriting, presented by Van Eetvelde and Janssens, is the modeling of refactoring operations for programs. The authors propose a hierarchical graph representation for programs to facilitate the study of refactoring operation effects at class level.The third part contains contributions focusing on unifying concepts for visual modeling techniques including UML:Minas describes a graphical specification tool for DIAGEN, a diagram editor generator based on hypergraph transformation. The specification tool simplifies the specification and generation of diagram editors. It uses an XML-based specification language and comes with a generic XML editor.In his contribution on dynamic aspects of visual modeling languages, Bottoni proposes an approach to the definition of the syntax and semantics of visual languages based on a notion of transition of production/consumption of resources. Abstract meta-models for this notion of transition are presented.An approach to the model-based verification and validation of properties of UML models is presented by Engels, Kïster, Heckel and Lohmann. The authors use graph transformation techniques as a meta-language for the translation and analysis of models.In model-driven architectures, the problem arises to deal with multiple models. Kent and Smith focus in their contribution on bidirectional mappings between models for software requirements and models for software design as basis for tools checking model traceability and consistency.Program CommitteeThe following program committee of UNIGRA'03 has given valuable scientific support:

• Hartmut Ehrig (TU Berlin, Germany) [chair]

• Roswitha Bardohl (TU Berlin, Germany) [co-chair]

• Luciano Baresi (University of Milano, Italy)

• Paolo Bottoni (University of Pisa, Italy)

• Claudia Ermel (TU Berlin, Germany)

• Reiko Heckel (University of Paderborn, Germany)

• Dirk Janssens (University of Antwerp, Belgium)

• Stuart Kent (University of Kent, Great Britain)

• Hans-Jörg Kreowski (University of Bremen, Germany)

• Fernando Orejas (University of Catalunya, Espania)

• Julia Padberg (University of Bremen, Germany)

• Grzegorz Rozenberg (University of Leiden, The Netherlands)

AcknowledgementThis workshop is supported by the European research training network SegraVis, and by the steering committee of the International Conference on Graph Transformation (ICGT).June 2003, Roswitha Bardohl and Hartmut Ehrig     

A Conceptual and Formal Framework for the Integration of Data Type and Process Modeling Techniques

A conceptual framework for the integration of data type and process modeling techniques, called integration paradigm, has been presented by the authors in previous papers already. The aim of this paper is to give a short review of this conceptual framework and to present a formal model for the integration paradigm. The formal model for the four layers, called data type, data states and transformations, processes and system architecture layers respectively, is based on an integration of abstract data types and structured transition systems. This formal model can be instantiated by all kinds of basic and integrated modeling techniques. Algebraic high-level nets, attributed graph transformation, an integration of Z with statecharts, and some diagram techniques of UML are discussed on the conceptual level. As instantiation of the formal model, a well-known CCS sender specification, place/transition nets, algebraic high-level nets and attributed graph transformation are presented in this paper, while instantiations of other modeling techniques will be discussed elsewhere.     

Can I find a partner? Undecidability of partner existence for open nets

We study open nets as Petri net models of web services, with a link to the practically relevant language WS-BPEL. For those nets, we investigate the problem of operability which we consider as fundamental as the successful notion of soundness for workflow nets, i.e., Petri net models of business processes and workflows. While we could give algorithmic solutions to the operability problem for subclasses of open nets in earlier work, this article shows that the problem is in general undecidable.     

Abstract processes of place/transition systems

A well-known problem in Petri net theory is to formalise an appropriate causality-based concept of process or run for place/transition systems. The so-called individual token interpretation, where tokens are distinguished according to their causal history, giving rise to the processes of Goltz and Reisig, is often considered too detailed. The problem of defining a fully satisfying more abstract concept of process for general place/transition systems has so-far not been solved. In this paper, we recall the proposal of defining an abstract notion of process, here called BD-process, in terms of equivalence classes of Goltz-Reisig processes, using an equivalence proposed by Best and Devillers. It yields a fully satisfying solution for at least all one-safe nets. However, for certain nets which intuitively have different conflicting behaviours, it yields only one maximal abstract process. Here we identify a class of place/transition systems, called structural conflict nets, where conflict and concurrency due to token multiplicity are clearly separated. We show that, in the case of structural conflict nets, the equivalence proposed by Best and Devillers yields a unique maximal abstract process only for conflict-free nets. Thereby BD-processes constitute a simple and fully satisfying solution in the class of structural conflict nets.     

Integer Linear Programming and the Analysis of Some Petri Net Problems

A class of Petri nets (called type \cal L Petri nets in this paper) whose reachability sets can be characterized by integer linear programming is defined. Such Petri nets include the classes of conflict-free , normal , BPP , trap-circuit , and extended trap-circuit Petri nets, which have been extensively studied in the literature. We demonstrate that being of type \cal L is invariant with respect to a number of Petri net operations, using which Petri nets can be pieced together to form larger ones. We also show in this paper that for type \cal L Petri nets, the model checking problem for a number of temporal logics is reducible to the integer linear programming problem, yielding an NP upper bound for the model checking problem. Our work supplements some of the previous results concerning model checking for Petri nets. Received October 1997, and in revised form July 1998.     

Complexity Results on Learning by Neural Nets

We consider the computational complexity of learning by neural nets. We are interested in how hard it is to design appropriate neural net architectures and to train neural nets for general and specialized learning tasks. Our main result shows that the training problem for 2-cascade neural nets (which have only two non-input nodes, one of which is hidden) is N-complete, which implies that finding an optimal net (in terms of the number of non-input units) that is consistent with a set of examples is also N-complete. This result also demonstrates a surprising gap between the computational complexities of one-node (perceptron) and two-node neural net training problems, since the perceptron training problem can be solved in polynomial time by linear programming techniques. We conjecture that training a k-cascade neural net, which is a classical threshold network training problem, is also N-complete, for each fixed k2. We also show that the problem of finding an optimal perceptron (in terms of the number of non-zero weights) consistent with a set of training examples is N-hard.Our neural net learning model encapsulates the idea of modular neural nets, which is a popular approach to overcoming the scaling problem in training neural nets. We investigate how much easier the training problem becomes if the class of concepts to be learned is known a priori and the net architecture is allowed to be sufficiently non-optimal. Finally, we classify several neural net optimization problems within the polynomial-time hierarchy.     

Zero-Safe Nets: Comparing the Collective and Individual Token Approaches

The main feature of zero-safe nets is a primitive notion of transition synchronization. To this aim, besides ordinary places, called stable places, zero-safe nets are equipped with zero places, which in an observable marking cannot contain any token. This yields the notion of transaction: A basic atomic computation, which may use zero tokens as triggers, but defines an evolution between observable markings only. The abstract counterpart of a generic zero-safe net B consists of an ordinary P/T net whose places are the stable places of B and whose transitions represent the transactions of B. The two nets offer the refined and the abstract models of the same system, respectively, where the former can be much smaller than the latter, because of the transition synchronization mechanism. Depending on the chosen approach—collective vs individual token philosophy—two notions of transaction may be defined, each leading to different operational and abstract models. Their comparison is fully discussed on the basis of a multicasting system example. In the second part of the paper, we make use of category theory to analyze and motivate our framework. More precisely, the two operational semantics of zero-safe nets are characterized as adjunctions, and the derivation of abstract P/T nets as coreflections.     

Petri nets with causal time for system verification

We present a new approach to the modelling of time constrained systems. It is based on untimed high-level Petri nets using the concept of causal time. With this concept, the progression of time is modelled in the system by the occurrence of a distinguished event, tick, which serves as a reference to the rest of the system. In order to validate this approach as suitable for automated verification, a case study is provided and the results obtained using a model-checker on high-level Petri nets are compared with those obtained for timed automata using prominent tools. The comparison is encouraging and shows that the causal time approach is intuitive and modular. It also potentially allows for efficient verification.     

Executable Petri net models for the analysis of metabolic pathways

Computer-assisted simulation of biochemical processes is a means to augment the knowledge about the control mechanisms of such processes in particular organisms. This knowledge can be helpful for the goal-oriented design of drugs. Normally, continuous models (differential equations) are chosen for modelling such processes. The application of discrete event systems such as Petri nets has been restricted in the past to low-level modelling and qualitative analysis. To demonstrate that Petri nets are indeed suitable for simulating metabolic pathways, the glycolysis and citric acid cycle are selected as well-understood examples of enzymatic reaction chains (metabolic pathways). The paper discusses the steps that lead from gaining necessary knowledge about the involved enzymes and substances, to establishing and tuning high-level net models, to performing a series of simulations, and finally to analysing the results. We show that the consistent application of the Petri net view to these tasks has certain advantages, and – using advanced net tools – reasonable simulation times can be achieved. Published online: 24 August 2001     

An ASM-based characterisation of starvation-free systems

Abstract State Machines (ASMs) have been successfully applied for modeling critical and complex systems in a wide range of application domains. However, unlike other well-known formalisms, e.g. Petri nets, ASMs lack inherent, domain-independent characterisations of computationally important properties. Here, we provide an ASM-based characterisation of the starvation-free property. The classic, informal notion of starvation, usually provided in literature, is analysed and expressed as a necessary condition in terms of ASMs. Thus, we enrich the ASM framework with the notion of vulnerable rule as a practical tool for analysing starvation issues in an operational fashion.     

On the Regularity of Petri Net Languages

Petri nets are known to be useful for modeling concurrent systems. Once modeled by a Petri net, the behavior of a concurrent system can be characterized by the set of all executable transition sequences, which in turn can be viewed as a language over an alphabet of symbols corresponding to the transitions of the underlying Petri net. In this paper, we study the language issue of Petri nets from a computational complexity viewpoint. We analyze the complexity of theregularity problem(i.e., the problem of determining whether a given Petri net defines an irregular language or not) for a variety of classes of Petri nets, includingconflict-free,trap-circuit,normal,sinkless,extended trap-circuit,BPP, andgeneralPetri nets. (Extended trap-circuit Petri nets are trap-circuit Petri nets augmented with a specific type ofcircuits.) As it turns out, the complexities for these Petri net classes range from NL (nondeterministic logspace), PTIME (polynomial time), and NP (nondeterministic polynomial time), to EXPSPACE (exponential space). In the process of deriving the complexity results, we develop adecomposition approachwhich, we feel, is interesting in its own right, and might have other applications to the analysis of Petri nets as well. As a by-product, an NP upper bound of the reachability problem for the class of extended trap-circuit Petri nets (which properly contains that of trap-circuit (and hence, conflict-free) and BPP-nets, and is incomparable with that of normal and sinkless Petri nets) is derived.     

M-nets: An algebra of high-level Petri nets, with an application to the semantics of concurrent programming languages

This paper describes a high-level Petri net model called M-nets (for modular multilabelled nets). A distinctive feature of this model is that it allows both: unfolding, as do most other high-level net models; and composition – in particular, synchronisation – in a process algebraic style, turning the set of M-nets into an algebraic domain. It turns out that the composition operations of this domain have various algebraic properties. Moreover, the model is such that composition operations are coherent with unfolding, in the sense that the unfolding of a composite high-level net is the composition of the unfoldings of its components. One of the motivations for M-nets is that they be a vehicle for giving semantics of concurrent programming languages. To illustrate their capability for that, the compositional semantics of – a simple, expressive concurrent programming language – is given. An associated low-level net semantics is described, and the coherence of these high-level and low-level semantics is proved. Received: 20 November 1996 / 13 January 1998     

Petri nets,event structures and domains,part I

The general aim of this paper is to find a theory of concurrency combining the approaches of Petri and Scott (and others).In part I we introduce our formalisms. To connect the abstract ideas of events and domains of information, we show how casual nets induce certain kinds of domains where the information points are certain sets of events. This allows translations between the languages of net theory and domain theory. Following the idea that events of causal nets are occurrences, we generalise causal nets to occurrence nets, by adding forwards conflict. Just as infinite flow charts unfold finite ones, so transition nets can be unfolded into occurrence nets. Next we extend the above connections between nets and domains to these new nets. Event structures which are intermediate between nets and domains play an important part in all our work. Finally, as an example of how concepts translate from one formalism to the other, we show how Petri's notion of confusion ties up with Kahn and Plotkin's concrete domains.In part II we shall continue the job of connecting up notions within net theory and the theory of domains. In particular, we shall examine the idea of states of computations.     

Capturing contextual relationship for effective media search

One of the central problems regarding media search is the semantic gap between the low-level features computed automatically from media data and the human interpretation of them. This is because the notion of similarity is usually based on high-level abstraction but the low-level features do not sometimes reflect the human perception. In this paper, we assume the semantics of media is determined by the contextual relationship in a dataset, and introduce the method to capture the contextual information from a large media (especially image) dataset for effective search. Similarity search in an image database based on this contextual information shows encouraging experimental results.     

A theory of structural stationarity in the <Emphasis Type="Italic">π</Emphasis>-Calculus

Automata-theoretic representations have proven useful in the automatic and exact analysis of computing systems. We propose a new semantical mapping of π-Calculus processes into place/transition Petri nets. Our translation exploits the connections created by restricted names and can yield finite nets even for processes with unbounded name and unbounded process creation. The property of structural stationarity characterises the processes mapped to finite nets. We provide exact conditions for structural stationarity using novel characteristic functions. As application of the theory, we identify a rich syntactic class of structurally stationary processes, called finite handler processes. Our Petri net translation facilitates the automatic verification of a case study modelled in this class.     

A semantic measure of the execution time in linear logic

We give a semantic account of the execution time (i.e. the number of cut elimination steps leading to the normal form) of an untyped MELL net. We first prove that: (1) a net is head-normalizable (i.e. normalizable at depth 0) if and only if its interpretation in the multiset based relational semantics is not empty and (2) a net is normalizable if and only if its exhaustive interpretation (a suitable restriction of its interpretation) is not empty. We then give a semantic measure of execution time: we prove that we can compute the number of cut elimination steps leading to a cut free normal form of the net obtained by connecting two cut free nets by means of a cut-link, from the interpretations of the two cut free nets. These results are inspired by similar ones obtained by the first author for the untyped lambda-calculus.     

How to calculate symmetries of Petri nets

Symmetric net structure yields symmetric net behaviour. Thus, knowing the symmetries of a net, redundant calculations can be skipped. We present a framework for the calculation of symmetries for several net classes including place/transition nets, timed nets, stochastic nets, self–modifying nets, nets with inhibitor arcs, and many others. Our approach allows the specification of different symmetry groups. Additionally it provides facilities either to calculate symmetries on demand while running the actual analysis algorithm, or to calculate them in advance. For the latter case we define and calculate a ground set of symmetries. Such a set has polynomial size and is sufficient for an efficient implementation of the for all symmetries loop and the partition of net elements into equivalence classes. These two constructions are the usual way to integrate symmetries into an analysis algorithm. Received 7 July 1997 / 10 August 1999     

On intuitionistic proof nets with additional rewrite rules and their approximations

First we present a proof nets system with eight additional rewrite rules, which concerns ordering of introductions of exponential-links and are only applied to normal forms of proof nets in the usual sense. We show that the reduction relation generated by these eight rewrite rules is strong normalizing and confluent. Second we propose an simply judged equality on intuitionistic proof nets based on the notion of the main path of an intuitionistic proof net. The notion is an analogue of Böhm-trees in λ-calculus.     

Commodification of accelerations for the Karp and Miller Construction

Karp and Miller’s algorithm is based on an exploration of the reachability tree of a Petri net where, the sequences of transitions with positive incidence are accelerated. The tree nodes of Karp and Miller are labeled with ω-markings representing (potentially infinite) coverability sets. This set of ω-markings allows us to decide several properties of the Petri net, such as whether a marking is coverable or whether the reachability set is finite. The edges of the Karp and Miller tree are labeled by transitions but the associated semantic is unclear which yields to a complex proof of the algorithm correctness. In this work we introduce three concepts: abstraction, acceleration and exploration sequence. In particular, we generalize the definition of transitions to ω-transitions in order to represent accelerations by such transitions. The notion of abstraction makes it possible to greatly simplify the proof of the correctness. On the other hand, for an additional cost in memory, which we theoretically evaluated, we propose an “accelerated” variant of the Karp and Miller algorithm with an expected gain in execution time. Based on a similar idea we have accelerated (and made complete) the minimal coverability graph construction, implemented it in a tool and performed numerous promising benchmarks issued from realistic case studies and from a random generator of Petri nets.