Skip to main content
main-content

Über dieses Buch

This volume presents a selection of papers presented at the 3rd European Workshop on Appl ications and Theory of Petri Nets that took place in Villa Monastero, Varenna (Italy) in the period September 27 - September 30, 1982. The I ist of topics included: nets and related models, mathematical analysis of nets, transformations and morphisms of nets, formal languages and nets, parallel program verification and nets, the pro­ blem of time in nets, programming languages based on nets, applications to distributed systems, applications to realtime systems, software ~~gineering, hardware design and its implementation, recoverability problems, nets and formal semantics; net tools. The diversity of topics on this list witnesses the fact that the researchers from very different areas presented their contributions and discussed various research problems during the workshop. This interaction of scientists looking at the area of Petri nets from very different points of view makes this series of workshops interesting and worthwi le. The volume documents the progress of the research concerning Petri nets during a one­ year time from the 2nd European Workshop held in Bad Honnef in 1981. We think that this was a substantial progress indeed. This observation is even more pleasant if one real izes that during the workshop in Varenna we have celebrated 20 years of "existence" of Petri nets (the seminal work by prof. C.A. Petri appeared precisely 20 years ago). We are very proud to present an invited address by prof. C.A. Petri in this volume.

Inhaltsverzeichnis

Frontmatter

Invited address

Some Personal Views of Net Theory

Abstract
Twenty years have passed since the first publication on net theory. I am grateful for the opportunity to speak on a topic of my choice on this occasion.
C. A. Petri

List of contributions

Structural Transformations Giving B-Equivalent PT-Nets

Abstract
In two previous papers, we introduced the notion of the B-equivalence (equivalence of behaviour) of two PT-nets on a common subset of transitions [Andre 80] and we pointed out the interest of the substitution theorem in PT-net analysis [Andre 81-2]. In short, the substitution of a closed subnet by a B-equivalent one doesn’t change the properties (liveness, synchronic relations for transitions; markings for places) on the unmodified part of the net.
C. Andre

Equivalence Notions for Concurrent Systems

Abstract
The classical equivalence notions introduced to compare sequential systems, namely weak equivalence (the computed functions are equal) and strong equivalence (the sets of possible event sequences are equal), are unuseful for comparing concurrent systems. In fact it has been shown (in (1) by Milner) that two strongly (and then also weakly) equivalent concurrent systems can differ w.r.t. the interactions with some other concurrent system.
F. De Cindio, G. De Michelis, L. Pomello, C. Simone

Milner’s Communicating Systems and Petri Nets

Abstract
The comparison between Milner’s CCS and Petri nets leads to prove that CCS defines a subclass of the concurrent systems definable by means of net theory, i.e. the class of systems composed of interacting sequential automata. The proof is based on (the construction of) an isomorphism between Milner’s communicating systems class and a subclass of Petri nets.The paper fully presents the proof for a subclass of communicating systems (where neither value passing nor finite unlimited instances of agents are allowed) and a specific subclass of nets, the SA2 PT class (a restriction of the Superposed Automata nets class). Some hints how to extend the proof to the whole CCS conclude the paper. This result allows to transfer analytic concepts and techniques from a theory to the other, as for example the observation equivalence notion defined inside the CCS. The paper is fully self-consistent.
F. De Cindio, G. De Michelis, L. Pomello, C. Simone

A Matrix-Based Implementation of Generalized Petri Nets

Abstract
Petri nets have been proved to be a useful tool for the specification of parallelism in control systems.
M. Courvoisier

Petri Nets Specification of Virtual Ring Protocols

Abstract
Distributed processing requires the design of reliable and fault tolerent networks. Such mechanisms are difficult to build due to the asynchronous failures detections (sites crashes, logical or physical partings) at each implied site.
P. Estraillier, C. Girault

A Note on D-Continuous Causal Nets

Abstract
The aim of this paper is to augment the theory of D-continuous causal nets (CCN’s) initiated in [1]. A CCN is a model of non-sequential processes. Our motivation in formulating the model was to set up a formalism in which the properties of a non-sequential processes [2,3] could be exposed. Among these properties the one called generalized Dedekind continuity (D-continuity) is particularly intriguing in that it points to a way to bridge the gap between discrete and “continuous” modes of descriptions of the same phenomena. Consequently we decided to endow our process model with this property and study the resulting structure. Somewhat to our surprise, we have found that our model exhibits most of the properties that have been proposed by C.A.Petri. In other words, D-continuity not only has an important motivation and interpretation, it also has a variety of attractive mathematical consequences.
C. Fernández, P. S. Thiagarajan

S-invariance in Predicate/Transition Nets

Abstract
In any theory of dynamic systems, the notion of invariance is of central importance. Given a class of processes, the supporting system is determined by what is invariable with respect to the processes.
H. J. Genrich, K. Lautenbach

A Diagram Editor for Line Drawings with Inscriptions

Abstract
A major obstacle to the use of diagrams in system design is the time required to draw and edit such diagrams. The primary purpose of the Diagram Editor is to reduce this time. Initial layout is facilitated by a technique that permits rapid visual evaluation of shape, size and positioning alternatives. Editing is supported in the same sense that a word processor supports the preparation of text. Thus a minor change which might normally require hours of mindless work redrawing an entire diagram can be accomplished in minutes.
The editor works with diagrams that consist of line drawings and text. The line drawings are composed of a relatively small number of basic shapes with connection paths between these shapes. The text is a set of inscriptions associated with the shapes and connectors. The editor produces both hardcopy of a diagram and a data structure which represents its formal and visual content. This can then be used in subsequent sessions by the editor and other programs. Ease of construction and user aesthetics are of paramount importance. User-definable descriptions of diagram elements, default algorithms and user interaction are employed to achieve these objectives.
A simple diagram is represented as a single ‘field’ of diagram elements. Such elements are either ‘node type’ or ‘connector type’ where nodes (shapes) have a position relative to the field center and connectors have a position relative to the two nodes they connect. Associated with both nodes and connectors are ‘regions’ which may contain inscriptions — e.g. text, formulae, or special symbols.
A complicated diagram is represented as a multilevel field structure where the structuring is accomplished by the reversible operations of simplification and elaboration. Petri Nets and related theoretical work have influenced the editor approach. This paper describes key concepts in the editor design.
Hartmann J. Genrich, Robert M. Shapiro

Formal Semantics by a Combination of Denotational Semantics and High-Level Petri Nets

Abstract
The purpose of the paper is to introduce a semantic model based on a combination of denotational semantics [Gordon] and high-level Petri nets [Genrich, Lautenbach], [Jensen]. The basic idea behind our approach is due to Kurt Jensen.
N. D. Hansen, K. H. Madsen

Notions of Computability by Petri Nets

Abstract
Eleven different definitions for functions to be computable by Petri nets are given and compared. For nine of these definitions it was possible to show that they are not powerful enough to describe all the primitive recursive functions.
Matthias Jantzen, Hendrik Bramhoff

High-Level Petri Nets

Abstract
This paper combines two closely related net models, predicate/transition nets and coloured Petri nets, into a new net model called high-level Petri nets. The new model is intended to combine the qualities of the two old models into a single formalism, and we propose in future to use high-level Petri nets instead of both predicate/transition nets and coloured Petri nets.
Kurt Jensen

Specification and Verification of Networks in a Petri Net based Language

Abstract
In this paper we present a system description language and a technique of top-down specification and verification of distributed systems. Our language is called Epsilon, and it has been developed for the description and analysis of systems containing concurrent components. We have used and developed concepts from the Simula [2] and Delta [5] languages and from Petri net theory [1]. A system described in Epsilon consists of a number of concurrent objects. Each object has a set of attributes, e.g. variables and procedures, and executes a sequence of actions. Epsilon includes both normal algorithmic statements and first order predicate logic as description elements.
In the paper we bring out the main features of the language and of our specification and verification technique through an example. We describe a simple ring-structured transport system by a stepwise specification and verification of its properties. Properties of all reachable states (partial correctness) are expressed directly in the Epsilon description by first order predicate logic. Proof of partial correctness is a matter of proving that the Epsilon-description is consistent. Properties concerning progress are not specified directly in the Epsilon description, but stated separately. Proof of total correctness is a matter of proving that the Epsilon description meets the progress specifications.
The semantics of Epsilon is defined by means of a model based on high- level Petri nets, i.e. a model founded on the notion of concurrency. This implies that our proof techniques a priori cover concurrency in the specified systems. The use of high-level Petri nets keeps the size of the nets relatively small. The complexity of the proofs is further reduced by transforming the logic expressions specifying partial correctness into a “local” form. Our technique avoids the “state-space explosion” often encountered in verification based on finite state models With more complicated systems the “factorization” of the proofs becomes increasingly important. However, the proof method works for non-local expressions as well, which gives one the possibility of allowing a few “global” expressions, e.g. if these do not have any natural local counterparts.
An extended version of this paper, including proofs of all theorems, is available as DAIMI PB-153 at the address above. A similar system is analysed by Owicki in [14].
Morten Kyng

Construction of Distributed Systems from Cycle-Free Finite Automata

Abstract
The purpose of this paper is to introduce an algorithm to construct distributed systems from cycle-free finite automata and a partition of the input-alphabet.
Rainer Prinoth

A Graph Theoretical Property for Minimal Deadlock

Abstract
There are at least two main reasons for studying classes of Petri nets. First, many systems are specified as sets of communicating sequential processes, with formal rules of construction which give birth to special kind of structures ([Her 79], [BMR 80] or [LSB 79]). The second is theoretical. Analysis algorithms have an exponential complexity. In assuming some constraints on the structure of the net, one can hope to decrease this complexity substantially.
G. Memmi

Petri Nets With Individual Tokens

Abstract
In the well known model of Petri nets (place/transition-nets), actual system states are represented as distributions of “black” tokens onto the places of the nets. Such tokens can not be identified as individual objects. The introduction of individual objects as tokens increases considerably the descriptive power of nets and allows for small but efficient models of real systems.
This paper presents a calculus of such nets. We introduce its formal basis (a module of multirelations) and derive S- and T-invariants as analysis tools.
Finally we compare our calculus with the predicate/transition-net model of Genrich and Lautenbach and the coloured net model of Jensen.
W. Reisig

Subset Languages of Petri Nets

Abstract
Formal language theory is used to some extent in the investigation of properties of Petri nets (see, e.g. [H], [JV] and [P]). In most applications of language theory for Petri nets one considers completely sequentialized versions of Petri nets only. That is one assumes that a Petri net has one central run place which allows only a single transition to fire at a time; any sequence of such firings is called a firing sequence and the language of a Petri net consists of the set of all firing sequences (or only of those firing sequences that lead to one of the finite number of final markings).
G. Rozenberg, R. Verraedt

Control of Flexible Production Systems and Petri Nets

Abstract
Low production cost requirements have developped a new trend to flexible production system automatization during these last years. Controllers are no longer isolated on a production machine, they are progressively interconnected with a transportation system and merged into an information system.
R. Valette, M. Courvoisier, D. Mayeux

On the Notion of Interface in Condition/Event-Systems

Abstract
In this paper, the notion of equivalent behaviour of condition/event-systems on a common subset of nodes (quasi-interfaces) is defined without imposing any severe restrictions on the CE-system or the chosen subset. This notion is advantageous for the construction and analysis of systems because it can be used as a basis for building systems by composing compatible subsystems as well as for analysis by substituting equivalent subsystems. A method to determine whether two CE-systems behave equivalently on a given quasi-interface is presented, which essentially consists of appropriately reducing the case graphs to graphs which reflect those (parts of) processes which can be observed on the quasi-interface. Finally, definitions of interface and compatibility are introduced which could be a useful starting point for dealing with the design of a system as opposed to its implementation.
Klaus Voss

Behavioral Equivalence of Concurrent Systems

Abstract
Many complex systems involving concurrency are composed of two parts: a control structure and a data processing structure. This paper is concerned with the problem of specifying the input-output behavior of control structures. In particular, it discusses and compares various possible formalizations of the concept of “behavioral equivalence”. Net theory and net languages play an important role in this study.
Michael Yoeli, Tuvi Etzion

Backmatter

Weitere Informationen