Skip to main content
main-content

Über dieses Buch

Concurrency and Nets is a special volume in the series "Advances in Petri Nets". Prepared as a tribute to Carl Adam Petri on the occasion of his 60th birthday, it is devoted to an outstanding personality and his pioneering and fruitful scientific work. Part I (70 pages of over 600) presents the congratulatory addresses and invited talks that were given at an Anniversary Colloquium. The contributions of this part honor Carl Adam Petri and his work from many different perspectives. Part II is a collection of invited papers discussing various aspects of the theme Concurrency and Nets. These papers are contributed partly by researchers that were or are still associated with the Petri Institute at GMD and partly by researchers whose scientific work deals with Net Theory or related system models. The topics range from basic theoretical aspects to application oriented methods.

Inhaltsverzeichnis

Frontmatter

Addresses and Talks Given at the Colloquium

Congratulatory Address

Friedrich Winkelhage

Congratulatory Address

Wilfried Brauer

Congratulatory Address

Grzegorz Rozenberg

Congratulatory Address

Fritz Krückeberg

Congratulatory Address

Hartmann J. Genrich

Carl Adam Petri and Informatics

Wilfried Brauer

Applying Petri Net Based Models in the Design of Systems

Many approaches are being developed for handling the different phases in the design of complex information systems, namely specification, verification, evaluation, implementation and testing. These approaches are more or less applicable to the various specific aspects of the design phases and partially supported by efficient tools. This paper deals with one of the most important approaches used in the design of information systems, i. e., the Petri net based models approach, which proves particularly interesting. It is indicated how Petri net based models are used to represent systems behavior and then some of the resulting advantages are given. Furthermore, it is emphasized why and how a Petri net based approach can support all the design phases and it is made clear for which purposes and in which applications Petri net based designs are important. A few illustrative examples are also given.

Michel Diaz

Contributed Papers

Frontmatter

Some Classes of Live and Safe Petri Nets

We study a series of structural restrictions which gives rise to a set of classes of marked nets: S-systems, T-systems, free choice systems and asymmetric choice systems. This series of restrictions corresponds to a series of behavioural properties of marked nets first introduced by C.A.Petri — sequentially, determinacy and confusion-freeness.For each one of these restrictions, we address the question to what extent the behaviour of a marked net is determined by the structure of the underlying net. In particular, we study the characterisation of liveness and the characterisation of safeness in the presence of liveness. The paper presents strengthened, streamlined and elementary proofs of some important results.

Eike Best, Pazhamaneri S. Thiagarajan

A model of cooperation and its specification with nets

Cooperation is an essential element in human social life. More and more, traditional forms of human cooperation are supported or even substituted by cooperating computer systems. Nevertheless, the realization of cooperating computer systems as well as their embedding in existing organisational structures is to a far extent a not understood process.To move the realization of cooperating computer systems towards a well understood engineering discipline, a constructive approach is urgently needed.This approach has to cover the design of cooperating systems — comprising the global modelling and formal specification of their cooperation — as well as their realization — comprising the derivation of implementations and tests from global specifications of cooperation.Modelling of cooperation and the method for its formal description determine the practicability and usefulness of such an approach. In this paper, some basic concepts of the modelling of cooperation and its formal specification with a tailored form of PETRI nets are outlined, which have proven within the work of the GMD Institut for System Technology to be well suited.Acknowledgements: Our thanks are due to our colleagues Dr. B. Baumgarten and Dr. P. Ochsenschläger for helpful discussions, and to D. Kunert and U. Vollhardt for typing the manuscript.

H.-J. Burkhardt, H. Eckert, R. Prinoth, E. Raubold

The Communication Disciplines of CHAOS

Although Petri’s Communication Disciplines have little influenced the scientific community till now, they offer a powerful theoretical framework for dealing with the pragmatics of human communication.In particular theoretically founded Communication Disciplines can be effectively embodied in Office Computer-Based Tools improving the flexibility of the communication protocols and their adaptability to changes in the off ice structure.The paper discusses this claim by presenting CHAOS (Commitment Handling Active Office System), an ‘intelligent’ system supporting the coordination of activities inside the office, and its Communication Disciplines.

F. De Cindio, G. De Michelis, C. Simone

On the Structure of Dependence Graphs

Dependence graphs (which are special kinds of acyclic directed node labeled graphs) are very fundamental objects in the theory of traces approach to concurrent systems and in the theory of graph grammars.In this paper we characterize dependence graphs and naked dependence graphs — where a naked dependence graph is the unlabeled graph obtained from a dependence graph by removing its node labels.

A. Ehrenfeucht, G. Rozenberg

Some Remarks on D-Continuity

One afternoon in 1978 (or was it in 1977 ?), C.A. Petri called one of the authors of this paper to his room. He wanted to talk about some “axioms of concurrency”. By that time, we knew already that a non-sequential process -viewed as a record of conditions-holdings and events-occurrences of a system- could be modelled using a special type of net called occurrence net, [7], [6]. Since at the behavior level, cycles are unrolled, one may associate to each occurrence net a partially ordered set, poset for short, which is an appropriate mathematical machinery to study non-sequential processes.

César Fernández, Agathe Merceron

Numerical Simulations with Place/Transactor-Nets

Place/Transactor nets, or P/Ta-nets for short, are a special development of Petri nets. Their prominent feature is a change of second order: The token flow as the change of the contents of places (first order change of states) is well-known from other net models; in P/Ta-nets we have on top of that a variation of the intensity of every flow (a change of second order), depending on the contents of some selected Places. Such Places, so-called K-Places, are adjoined like an inscription to every flow arc. P/Ta-nets are described in detail, as well as their (historical) background, and their significance for numerical simulations. Some examples of programming with P/Ta-nets in the field of applications are given. Relations to other types of nets are sketched, and some general causal features in simulation, especially on the use of random numbers, are reflected.

Hans Fuss

Net Models of Dynamically Evolving Data Structures

An asynchronous push-down stack designed by Petri [6] is revisited and used as a basis for constructing two registers that can be used as a queue and a double-ended queue, respectively. These registers show several appealing features. They are highly concurrent arrays of processor elements and storage cells. Their size is unbounded; they can be repeatedly extended at their front end without affecting their internal structure or operation. Their latency is independent of the size. Their internal processor elements perform reversable operations; the implementation would not depend on energy dissipation.

Hartmann J. Genrich

On Condition/Event Representations of Place/Transition Systems

One of the fundamental principles in Net Theory is that each representation of a system as a marked net should be traced back to a common basic interpretation — nets of conditions and events ([Pe]). However, this immediately implies a number of questions.

Ursula Goltz

Finite Conjunctive Nondeterminism (Extended Abstract)

In process description languages such as CCS, [M], processes correspond to terms over a given signature. Each operator of the signature, or combinator, corresponds to a method for constructing new processes from existing ones. In this paper we suggest that the choice of combinators should be governed by the logical properties they induce. Specifically they should be chosen so that the logical properties of the constructed process are easily inferred from those of its constituents. Of course we must ensure that these operators also have an acceptable operational and denotational semantics. In other words, we would like to develop an approach to the semantics of processes which reconciles the more usual denotational and operational semantics with logic. In such a framework we would expect the logic to determine the denotational semantics. More specifically, if ∥p∥ represents the denotation of p then we would expect ∥p∥ = ∥q∥ iff (for every φ, p ⊧ φ <=< q ⊧ φ) (*) where φ ranges over formulae from some suitable assertio n or property language.

M. Hennessy, G. Plotkin

Petri Net Languages and One-Sided Dyck-Reductions On Context-Free Sets

In [2, 6, 8, 9] cancellation grammars (or grammars related to them) are defined and their relation to well-known families of languages are studied. Savitch showed in [9] that the class of EOL languages can be obtained from the context-free sets (CF) by iteratively and completely cancelling one matching pair xx̄ of parenthesis x and x̄. This type of reduction is here called a Dyck1-reduction on a set L which can be taken from any family of languages — not only the context-free sets — and thus need not be definable by certain restricted classes of grammars as in [2, 9]. In this short note we will show that we get all (free) terminal Petri net languages and all transition sequences from the context-free sets by Dyck1-reductions and, moreover, each non-erasing homomorphic image thereof, the corresponding families denoted by L and P as in [7].

M. Jantzen, H. Petersen

From Nets to Logic and Back in the Specification of Processes

Among formal models proposed to specify concurrent systems and processes, three main groups emerged. They can be referred to as net models, algebraic calculi and process logics. Each group supports specific abstraction methodology and possesses different descriptive and analytical power. These two abilities are, to some extent, contradictory and usually are exploited separately in theoretical studies. However, their combination is highly desirable in practical tools for the verification and synthesis of systems. This stimulates the comparative studies of different classes of models with cross-interpretation of their basic notions and primitives. Some efforts to combine their advantages in the framework of unified theories are now in progress. The models based on Petri nets seem to be the most close to the adequate description of “pure” concurrency. As a result, many net- -based models were proposed for the formal specification and validation of concurrent systems: control structures in parallel programs, circuitry design, net protocols, etc. However, these models, providing a good insight into structural properties of designed concurrent systems, do not contain sufficient support for the validation of behavioural properties and equivalencies. This forces to have recources to some “external” formalisms. For example, having a net description of a system, we use firing sequences, traces, net languages, etc. to define and analyze the net properties. It would be more convenient if both descriptive and analytical parts of a modelling theory were based on the same set of basic notions and constructors.

V. E. Kotov, L. A. Cherkasova

Types and Modules for Net Specifications

A specification language for nonsequential systems that unifies algebraic specifications of abstract data types with high-level Petri net specifications of dynamic behavior is presented. The data structure of a system, the information content of local states, and static constraints to state changing operations are specified by sorted Horn clause rules with equality. Behavior is specified by schemes of Predicate-Event nets together with an initial (distributed) state. Many-sorted algebras provide a standard interpretation of such specifications in terms of the initial models satisfying the rules, the flow, and the initial state given. One concern of this paper is to sketch the mathematical semantics of the core language. The other is to define a notion of abstract system that supports modularity and reusability of specifications similar to abstract data types.

Bernd Krämer, Heinz-Wilhelm Schmidt

An Introduction to the Macro Cosy Notation

One of the objections to the use of Petri nets or, equivalently, specifications written in the COSY (Concurrent Systems) notation, for modelling realistic systems is that they would grow too large to be of any practical use. Generators for the concise representation of large (possibly infinite) structures in net theory or specifications in COSY are traced to their origins in Carl Adam Petri’s thesis [P62]. The generators implemented in the current version of COSY and its accompanying simulation and analysis tools are presented in detail together with design decisions which led to their present form.

P. E. Lauer, R. Janicki

Linear Algebraic Calculation of Deadlocks and Traps

It is shown how deadlocks and traps of a class of place/transition-nets can be calculated as S-invariants of marked graphs.

Kurt Lautenbach

On Different Kinds of Frozen Tokens in Petri Nets

Containing a frozen token in a Petri net means that there exists an infinite occurrence sequence in the net such that at least one token in some place is never moved. Frozen tokens are classified here by considering occurrence sequences and processes associated to occurrence sequences. And some applications about frozen tokens are suggested.

Wei-Ming Lu

High Level Petri Nets and Distributed Termination

The paper presents a high level Petri net (HLPN) specification of an algorithm for global termination detection of a system of parallel processes. The correctness is proved using invariants and an assertion system.

Horst Müller

Communication and Database Oriented Modelling of Multilateral Cooperation — A Comparison Based on Petri Nets

The design of distributed sytems requires integrating viewpoints of various disciplines into a common modelling approach. Distributed applications are characterized by the need to correlate different processing states and data, a task which comprises communication and database aspects.The present paper deals with the question of how the modelling of distributed applications is influenced by the viewpoint taken by the modeller. To answer this question we model an example from the area of human cooperation first from the standpoint of a communication systems specialist and then from the standpoint of a database systems expert. In both cases, we begin by identifying substructures and their interrelations as suggested by the respective concepts. Expressing both models as higher level Petri nets we are then able to investigate the relation between the communication and database aspects.Topologically, the two nets differ mainly in their degree of explicitly modelling local states and message passing. The tasks of coordination and synchronization between the participants, however, are so strictly determined by the problem that their net representations are very similar. The major difference lies in the field- specific interpretations of the nets, which induce dissimilar partitions into subnets, namely into participants and message types on one hand and into transactions on the other hand.

Volker Obermeit, Ralf Steinmetz, Bernd Baumgarten, Heinz-Jürgen Burkhardt, Peter Ochsenschläger, Rainer Prinoth

The Structure of Facts in Occurrence Nets

A fact in a C/E-system Σ: = (B, E; F, C) is a conceivable “dead” pure transition t which could be added to the system Σ without changing its behaviour. The transition t is completely described by the corresponding pair (·t, t·); and therefore facts are essentially pairs (I, J) with I, J ⊆ B. Facts with minimal (I, J) are called basic facts; and it is immediately clear that a basic fact (I0, J0) implies all facts (I, J) with I0 ⊆ I ^ J0 ⊆ J.Processes of Σ can be conceived as mappings from appropriate occurrence nets into Σ. Then every fact of Σ can be derived from the facts in the corresponding occurrence nets. Therefore, knowledge of the general structural properties of facts in occurrence nets may be helpful to understand how facts can be realized by C/E-systems. The aim of this paper is to show that facts in occurrence nets have a rather simple structure provided some finiteness conditions hold true. Obviously, to this end it is suffucient to investigate the basic facts of occurrence nets; it will turn out that for all basic facts (I0, J0) of an occurrence net we have | I0 | ≤ 2; and that the set of all of these basic facts can be partitioned into six classes each of which contains facts of a special structure.

Helmut Plünnecke

Observing Net Behaviour

Net system models are discussed from the point of view of the observations an observer can make on their behaviour. It is shown that while the behaviour of a contact-free C/E system, that can be considered as a “completely” specified system model, does not exhibit any difference depending on the kind of the observations the observer makes on it, the same is not true for safe net systems and for labelled safe net systems (considered as “incompletely” specified system models).

Lucia Pomello

Algebraic Models of Parallelism and Net Theory

In this note we present a comparison between Net Theory and Algebraic languages such as Milner’s CCS [2]. We argue that a mild generalisation of three postulates from which Condition/Event systems may largely be derived, gives rise to a class of algebraic models at this level of abstraction. As C/E systems provide the basic level of interpretation in Net theory, so too do these C/E algebraic systems provide a level of interpretation for general algebraic models, and one in which concurrency may be formally defined.

M. W. Shields

Towards a Synchrony Theory for P/T Nets

Synchrony theory is a branch of General Net Theory devoted to the study of transition firing dependences. Considering place/transition nets (P/T nets), these dependences will be studied by means of four related kinds of synchronic concepts: synchronic lead (SL), synchronic distance (SD), deviationbound (DB) and fairness bound (FB). The main relations among them are presented, giving an unified view. The boundedness of any synchronic function for two subsets of transitions is characterized by a synchronic relation. Particular attention is given here to algebraic characterizations of synchronic relations.

M. Silva

The Semantics of a Net is a Net

An Exercise in General Net Theory

A core issue of General Net Theory is to relate different net classes by meaning preserving mappings. To do so in a simple and elegant way, some mathematical techniques will be developed in this paper. This includes special net morphisms and equivalence relations on nets. These concepts are applied to study the relationship of (strict) high level nets to condition/event systems. Different classes of high level nets are discriminated.

Einar Smith, Wolfgang Reisig

On the mutual simulatability of different types of Petri nets

In this paper we consider the relative power of different types of Petri nets, namely Place/Transition nets, Coloured nets, Relation nets, Predicate/Event nets, Predicate/Transition nets, Self-modifying nets and Fifo nets. We do this by investigating whether there are possibilities to simulate one type of nets by other ones or not.

Peter H. Starke

Development and Application of Petri Net Based Techniques in Australia

Petri Net based techniques are currently being used in several organisations in Australia as analytical tools and models for the investigation and solution of practical problems in the specification, verification and implementation of communication and computing systems. Most of the people involved in Australia are using an extension of Petri Nets called Numerical Petri Nets (NPNs), together with a versatile computer based protocol analysis tool called PROTEAN (Protocol Emulation and Analysis).The applications of Petri Net based techniques include the specification of Open Systems Interconnection (OSI) and Integrated Services Digital Network (ISDN) services, protocols and interfaces; the verification of OSI protocol specifications against their service specifications; the analysis of protocols and signalling systems; the generation of test sequences for testing conformance of protocol implementations; as an integral part of a systematic means of producing operational code from high level specifications of services and protocols; the study of computer architectures to enable direct execution of Petri Nets in order to take advantage of concurrency in specifications; and the development of theoretical techniques for the analysis of Petri Nets.An overview is given of the development and application of Petri Net based techniques in Australia over the last ten years, as a tribute to the pioneering work of Dr Carl Adam Petri.

F. J. W. Symons

Quantitative Analysis of a Resource Allocation Problem: A Net Theory Based Proposal

The prevention of deadlocks is studied for a special class of resource allocation problems. A resource decentralization algorithm identifies safe allocation strategies. Given an initial resource availability, each strategy is then quantitatively analysed in order to determine the one that allows a relative maximum for the flow of processes through a system. The structural and dynamic characteristics of the problems suitable for analysis, as well as the proposed solution, are described in terms of place/transition nets.

M. Tazza

Existential Quantifiers in Predicate-Fact-Nets

It is well known that every formula of first-order predicate logic in prenex form can be represented as a strict predicate transition net (PrT-net) in which all transitions are seen to be dead. Nets wherein all predicates can carry only one specimen of an n-tuple are called strict [Ge]. In this net representation of predicate logic Skolem functions are used to get descriptions for existential quantifiers [Th].In PrT-systems given by PrT-nets and an initial marking, the dead transitions specify the facts about that system. S-invariants are a very useful means to prove transitions of a PrT-system to be facts. In those predicate fact nets (PrF-nets) derived from S-invariants, Skolem functions do not occur.The question arises, whether existential quantifiers do not exist in those fact nets, or whether nets carry another more natural representation for them. Sums seem to yield such an appropriate net description for existential quantifiers. But some derivation problems remain, in which sums cannot replace the Skolem functions.

Gerda Thieler-Mevissen

Petri Nets for Sequence Constraint Propagation in Knowledge Based Approaches

This paper deals with the possibilities of the integration of Artificial Intelligence techniques within a Petri net approach for controlling and monitoring Flexible Manufacturing Systems. Section 2 is a short presentation of knowledge representation, then the similarities between Petri nets and these techniques are described in sections 3 (static aspect) and 4 (dynamic aspect). An illustrative example is given in Section 5.

R. Valette, H. Atabakhche

Extension and Intension of Actions

The principle of extensionality in net theory is examined from a new point of view. Including side conditions it becomes possible to describe different intensions of an action.

Rüdiger Valk

Interface as a Basic Concept for Systems Specification and Verification

To specify or to verify a system means to prescribe or to analyze its connections with the environment into which it shall be or in which it is embedded. From this point of view, its internal construction and its internal behaviour are relevant only as far as they determine its communication and cooperation with the outside. Hence, both specification and verification are concerned with a part of the system only, namely its interface with its environment. As a basis to deal with such partially determined systems, an appropriate means to represent them and a suitable equivalence notion are needed. This paper discusses the use of strictly labelled net systems for the representation of system interfaces and the notion of interface equivalence. The latter notion is a generalization of bisimulation and is intended to preserve the most important properties of sytems at the interface with their environment. It can constitute a basis for deriving concepts of compatibility to be used in answering the question whether and to what extent a realized system fulfills a given specification.

Klaus Voss

Specification and Verification of Asynchronous Circuits Using Marked Graphs

This paper deals with the behavioral specification and description of digital circuits operating asynchronously. In particular, it is shown how the behavior of a composite circuit may be derived from the behavioral description of its components. The paper combines the theory of trace structures developed by M. Rem and J.L.A. van de Snepsheut with a suitable extension of the theory of marked graphs. It consequently achieves a considerable simplification of the way composite circuits are modeled and verified.

Michael Yoeli
Weitere Informationen