Advances in Petri Nets 1992

Frontmatter

Esprit basic research action 3148 DEMON (Design methods based on nets) — Aims, scope and achievements —

Eike Best

The box calculus: A new causal algebra with multi-label communication

Abstract

A new Petri net calculus called the calculus of Petri Boxes is described. It has been designed to allow reasoning about the structure of a net and about the relationship between nets, and to facilitate the compositional semantic translation of high level constructs such as blocks, variables and atomic actions into elementary Petri nets. The calculus is located ‘midway’ in such a translation.

This paper first defines an algebra of Box expressions. A corresponding algebra of Boxes is then defined and used compositionally as a semantic model of Box expressions. The two algebras feature a general asynchronous communication operation extending that of CCS. Synchronisation is defined as a unary operator. The algebras also include refinement, iteration and recursion. It is shown how they can be used to describe data and blocks.

As the main results of this paper, it is proved that the Box algebra satisfies various desirable structural laws and enjoys two important behavioural properties. The paper also contains an example proof of a mutual exclusion protocol.

Eike Best, Raymond Devillers, Jon G. Hall

Modular functional modelling of petri nets with individual tokens

Abstract

A functional semantic modelling of Petri nets with individual tokens also called high level Petri nets is outlined. A denotational semantics for so-called high level Petri net components, i.e. nets that may contain ingoing and outgoing arcs, is given. An abstraction of the semantics is provided in terms of a predicative semantics. This semantics is modular in the sense that high level Petri net components can be composed by parallel composition and feedback in a way that the semantics of the composed net can be derived from the semantics of the net components.

Manfred Broy, Thomas Streicher

Interleaving semantics and action refinement with atomic choice

Abstract

We investigate how to restrict the concept of action refinement such that established interleaving equivalences for concurrent systems are preserved under these restricted refinements. We show that interleaving bisimulation is preserved under refinement if we do not allow to refine action occurrences deciding choices and action occurrences involved in autoconcurrency On the other hand, interleaving trace equivalence is still not preserved under these restricted refinements.

Ingo Czaja, Rob J. van Glabbeek, Ursula Goltz

Maximality preservation and the ST-idea for action refinements

Abstract

The paper shows, in the framework of labelled P/T nets, that strengthening classical bisimulations through a maximality preservation property or through the introduction of ST-configurations leads to equivalent bisimulation notions, that they are preserved by a large class of action refinements, that they may be characterized through specific refinements and that they are the coarsest equivalences preserved by refinements and implying the original bisimulations.

Raymond Devillers

A fifo-net model for processes with asynchronous communication

Abstract

We define net-based formal models for concurrent processes communicating by asynchronous message passing. Programs specified in an abstract language are modelled by fifo-nets with composition operators, and for the first time extended compositionality and partial order semantics are considered in the fifo-net context. This leads to an algebra of fifo-nets, together with different congruences, which extends to the asynchronous communication part of the work on CCS, TCSP and ACP.

J. Fanchon

A basic-net algebra for program semantics and its application to occam

Abstract

We define an algebra comprising a class of basic Petri nets, enhanced with place and transition labels, together with operations of sequence, choice, parallel, iteration, prioritised choice and label hiding. An important characteristic of the algebra is that it combines transition-based composition for modelling synchronous communication, as in Petri net semantics for CCS or TCSP, with place composition for modelling shared variables. We use the algebra to give a family of net semantics for a version of OCCAM, comprising a full semantics, for which we have consistency with the Laws of OCCAM, and a range of semantics for partial data abstraction which give smaller nets (for more practical use of net tools and techniques) with a limited consistency such that safety (but not liveness) properties transfer from more-abstracted to less-abstracted semantics.

Richard Hopkins, Jon Hall, Oliver Botti

The effect of Vector synchronization: Residue and loss

Abstract

In a Vector Controlled Concurrent System (VCCS) a fixed number of sequential processes operate under the control of a vector synchronization mechanism. Thus, the original behaviour of each of the component processes is constrained by the control mechanism. This observation leads to the introduction of the notion of residue (the remaining behaviour possibilities) and the complementary notion of loss (of behaviour possibilities). For various submodels of the general VCCS model obtained by varying the classes of component processes and by varying the synchronization mechanism, we characterize in a language theoretical sense their residue families and their loss families. In addition we establish for these VCCS submodels the borderline between decidable and undecidable emptiness and finiteness problems for the corresponding families of losses and residues.

N. W. Keesmaat, H. C. M. Kleijn

Modelling systems with dynamic priorities

Abstract

In this paper we discuss concurrent systems with dynamic priorities, i.e. we allow the priority relation to change as the system evolves. We identify two classes of such systems, state-controlled and event-controlled priority systems. We define their nonsequential semantics (in terms of step sequences) which reflects both the priority constraints and concurrency specification. It is then shown that for a given prioritised system it is possible to construct an equivalent non-prioritised one. The systems dealt with in this paper are safe Petri nets augmented with a priority specification.

Maciej Koutny

On distributed languages and models for concurrency

Abstract

Event Structures are a poset based model for describing the behaviour of distributed systems. They give rise to a well understood class of Scott domains. Event structures are also related to Petri nets in a fundamental way. Trace monoids are a string-based formalism for describing the behaviour of distributed systems. They have an independent theory rooted in the theory of formal languages, but are too weak to express more general nets and problems, such as the producer and consumer paradigm for example. Thus extensions of original traces have been looked at. In this paper, we describe connections between Partially Ordered Sets and Traces, using a Transition Systems, and in order to allow sound generalizations of finite traces to context-sensitive ones.

We obtain a representation of generalized trace languages in terms of labelled event structures.

Brigitte Rozoy

Partial words versus processes: A short comparison

Abstract

In this note I want to draw attention to partial words, a less known partial order semantics of Petri nets. Partial words have recently proven to be of importance, e.g. in the study of action refinement. An important result of A. Kiehn relates partial words and Petri net processes, and a short proof of this result is given here.

Walter Vogler

A survey of basic net models and modular net classes

Abstract

The paper surveys those net classes which can be called to some extent ‘modular’ and the basic net models used as framework in their definition.

In particular the first part introduces Condition/Event systems, Elementary Net systems, Place/Transition systems and 1-safe systems, adhering as much as possible to the original definitions, with the few modifications consolidated in the literature. Then it discusses and compares the basic net models by considering how each one of them deals with some fundamental properties of a net model, such as simplicity, pureness, backward and forward reachability, liveness, contact-freeness.

The second part surveys the main classes of modular nets defined in the literature, showing that most of them share some basic features, since they typically refer to a common idea of building the overall net by composing the nets modelling its sequential components by means of state machines. The differences are considered from the perspective of the specific goal and field of interest of the various authors, and the technical apparatus associated with the various net classes is briefly referred to and illustrated by examples.

Luca Bernardinello, Fiorella De Cindio

Structural techniques and performance bounds of stochastic Petri net models

Abstract

In this paper we overview some recent results obtained by the authors and collaborators on the performance bounds analysis of some stochastic Petri net systems. The mathematical model can be seen either as a result of the addition of a particular random timing interpretation to an “autonomous” Petri net or as a generalization of classical queueing networks with the addendum of a general synchronization primitive. It constitutes an adequate tool for both the validation of logical properties and the evaluation of performance measures of concurrent and distributed systems.

Qualitative and quantitative understandings of Petri net models are stressed here making special emphasis on structural techniques for the analysis of logical and performance properties. Important aspects from the performance point of view, such as relative throughput of stations (transitions), and number of servers present at them, are related to Petri net concepts like P- or T-semiflows or liveness bounds of transitions. For the particularly interesting case of Markovian Petri net systems, some improvements of the bounds can be achieved. Marked graphs and free choice are net subclasses for which the obtained results have special quality, therefore an additional attention is focussed on them.

Javier Campos, Manuel Silva

A survey of recognizable languages of infinite traces

Abstract

A. Mazurkiewicz [Maz77] defined traces in order to represent non-sequential processes. In order to describe non-sequential processes which never terminate, e.g. distributed operating systems, the notion of infinite traces is needed. The aim of this survey is to present in a uniform way the results on recognizable infinite trace languages stated in [Gas91], [GPZ91] and [DGP91]. The proofs of the presented results are not proposed here but can be found in the original papers.

Paul Gastin, Antoine Petit

A survey of equivalence notions for net based systems

Abstract

This paper surveys various notions of equivalence for concurrent systems in the framework of Elementary Net Systems, a fundamental class in the family of Petri Net models. Two types of equivalences are considered: equivalences based on observations of actions defined in the framework of interleaving, step and partial order semantics; and equivalences based on state spaces and state observability.

L. Pomello, G. Rozenberg, C. Simone

Backmatter