Application and Theory of Petri Nets 1992

Frontmatter

Performance issues in parallel programming

Abstract

The development of parallel applications requires the availability of tools that support their debugging and tuning. GSPN represent a formalism that is well suited for the construction of formal models of parallel programs that can be used for both validation and evaluation purposes. The analysis of GSPN models of parallel programs provides the information that is needed for deciding whether the objectives contained in the specifications of an application are met and for distributing the computation on a parallel architecture. In this paper we discuss a methodology for directly constructing a GSPN model of an application from its code and for deriving the parameters that are needed for obtaining the optimal allocation of the components of a parallel application on the computational units of a parallel architecture. A simple example is used throughout the paper to illustrate the different steps of the methodology and to show how these GSPN models can be used to check the efficiency of a parallel application.

Gianfranco Balbo

Combining Petri Nets and other formal methods

Abstract

Several practically important concepts, supporting proper treatment of concurrency, have evolved during the recent years. Many of them have been presented in formal settings different from Petri Nets. In this paper we exemplify some of those concepts and relate them to the state-of-the-art in Petri Nets.

W. Reisig

Place bisimulations in Petri nets

Abstract

Place bisimulations are bisimulations between places of Petri nets. We propose a new definition for this basic (new) concept, study several derivatives and classify them.

The main practical application of place bisimulation is as a method for the simplification of nets in a semantically correct way. We show how this simplification can be done in polynomial time.

C. Autant, Ph. Schnoebelen

A polynomial-time graph algorithm to decide liveness of some basic classes of bounded Petri nets

Abstract

This paper is related to structural analysis of Petri nets where liveness and boundedness issues are addressed through the analysis of the combinatorial properties of the underlying graph. We first recall a number of basic results about liveness and boundedness involving combinatorial substructures (deadlocks and traps). It is then shown that testing whether a bounded Extended Free Choice net or a Non Self-Controlling net is structurally live can be reduced to the search for a strongly connected deadlock which is not a trap. This problem, in turn, is shown to be solvable in polynomial time through a purely combinatorial algorithm making combined use of Tarjan's strong connectivity algorithm and Minoux's LTUR algorithm for solving Horn satisfiability problems. Once structural liveness has been proved, testing liveness for a given initial marking is already known to be polynomially solvable.

Kamel Barkaoui, Michel Minoux

Refinement and simulation of nets — a categorical characterisation

Abstract

Category theory has been applied to Petri nets in two distinct ways. The first approach is to define a category whose objects are Petri nets and whose morphisms represent the refinement of one net by another. The second approach is to define a category whose objects are themselves categories representing the possible computations of the net.

We establish a close connection between these two approaches by exhibiting a reflection between a category of nets and a category of behaviour categories. The morphisms in our categories have an appealing computational interpretation in terms of simulation, which is closely related to the notion of simulation in process algebra.

Carolyn Brown, Doug Gurr

Scheduling hard real time systems using high-level Petri nets

Abstract

Hard real time systems need schedulability analysis to check that timing constraints are met before the actual application is run. In the literature, schedulability analysis is tackled by assuming that the real-time system is described by concurrent processes. However, high level Petri nets, such as those used in Protob, provide a more conceptual representation than concurrent processes.

This paper illustrates the computation of schedules of activities from Protob nets with different execution policies (one processor without preemption, one processor with preemption) and the translation of such schedules into concurrent processes for which optimal scheduling algorithms, such as [1], exist.

Giorgio Bruno, Andrea Castella, Gianpaolo Macario, Marco P. Pescarmona

Towards a modular analysis of coloured Petri nets

Abstract

The use of different High-level Petri net formalisms has made it possible to create Petri net models of large systems. Even though the use of such models allows the modeller to create compact representations of data and action, the size of models has been increasing. A large model can make it difficult to handle the complexity of the modelling as well as the analysis of the total model. It is well-known that the use of a modular approach to modelling has a lot of advantages. A modular approach allows the modeller to consider different parts of the system independently of one another and also to reuse the same module in different systems. A modular approach to analysis is also attractive. It often dramatically decreases the complexity of the analysis task.

In this paper, we present modular CP-nets. They are not intended to be used for practical modelling purposes, but they constitute a formal and general framework for discussing different ways of composing individual CP-nets called modules. Modular CP-nets allow us to study composition without restricting the structure of the individual modules. Modular CP-nets are quite simple and do not include syntactical sugar which is convenient and often necessary when modelling in practice. Instead, they have only a few but very general composition constructs.

The main result of the paper is the possibility of composing analysis results of the individual modules, in order to obtain results which are valid for the entire modular CP-net. For this purpose, we introduce place invariants at the level of modular CP-nets and we show how such place invariants can be obtained from those of the individual modules.

The reader of this paper is assumed to be familiar with the basic definitions of CP-nets and the concept of place invariants. But it is not necessary to be familiar with hierarchical CP-nets.

Søren Christensen, Laure Petrucci

A proof of the Rank Theorem for extended free choice nets

Abstract

A net is called well-formed if it can be marked with a live and bounded marking. The Rank Theorem characterises well-formed extended free choice nets, employing only the linear algebraic representation of a net. The paper presents a proof of the Rank Theorem which is based on the characterisation of liveness by deadlocks and traps and the coverability of well-formed extended free choice nets by S- and T-components. Consequences of the Rank Theorem include the Duality Theorem, a polynomial algorithm for deciding wellformedness, and simple proofs of other results concerning extended free choice nets. Moreover, the Rank Theorem implies a sufficient condition for liveness which applies to arbitrary nets.

Jörg Desel

On the product form solution for Stochastic Petri Nets

Abstract

The combinatorial explosion of the state space of Stochastic Petri Nets (SPNs) is a well known problem that inhibits the exact solution of large SPNs, and therefore a broad use of this kind of Petri Nets as a modelling tool. The same problem exists also for other modelling formalisms like for example Queueing Networks (QNs). In [13, 3] a class of QNs whose solution can be computed in an easy way was defined. For this class of models the solution can be factorized into terms that refer to each single queue of the network. This solution is known as Product Form Solution (PFS).

In this paper we compare two different approaches to PFS for SPNs. In both proposals the solution is obtained as a product form of terms, each term corresponding to a place in the SPN.

The first approach (by Lazar and Robertazzi) allows the PFS to be detected at state space level by inspecting the structure of the reachability graph. The second one (by Henderson, Lucic and Taylor) allows the PFS to be detected at structural level, that is to say without inspection of the reachability graph. In this paper we try to put the two approaches into a common framework and to show the important role played by T-invariants.

Susanna Donatelli, Matteo Sereno

Obtaining deadlock-preserving skeletons for coloured nets

Abstract

We extend Vautherin's work on behavioural relationships between coloured nets and their skeletons, which are ordinary Petri nets. A desirable property for a coloured net to have is that a marking is dead if and only if the corresponding skeletal marking is dead. This guarantees that for each deadlock (i.e. reachable dead marking) of the coloured net, the corresponding skeletal marking is a deadlock, so coloured deadlocks are ‘preserved’ in the skeleton. Vautherin gave a rather restrictive sufficient condition for the aforementioned property. We formulate two necessary and sufficient conditions, thus identifying the class of coloured nets with ‘deadlockpreserving skeletons’. We then show how any coloured net may be ‘refolded’ to obtain one with the same behaviour as the original and with a deadlock-preserving skeleton. Consequently, all deadlocks of the original net may be detected via this skeleton. Moreover, the refolding transformation is optimal, in the sense that this skeleton is as small as possible.

Greg Findlow

P-superfairness in nets

Abstract

The notion of polynomial superfaimess, which is an extension of strong fairness, is introduced for Petri nets. Superfair sequences automatically have a lot of properties which are not implied by strong fairness. Nevertheless — under reasonable circumstances — almost all infinite occurrence sequences are superfair and there are recursive — in fact exponential — such sequences. The concept of superfaimess is compared to other fairness notions. Possible extensions are suggested.

Hans Fleischhack

Formal verification of an arbiter cascade

Abstract

The asynchronous access of a group of users (e.g. processors) to a single resource (e.g. bus) is regulated by a cascade of arbiters. A single arbiter circuit handles two users. The cascade permits any number of users to be serviced. We use a hierarchical Colored Petri Net to describe the arbiter circuit and the protocol for using it. We also describe the layout of a 2d input cascade of (2^d-1) arbiters, d≥1 being the depth of the cascade. We verify the proper functioning of the cascade, first for depth d=1 using an occurrence graph analyzer to prove crucial invariants and confonmance to the protocol; then for arbitrary depth using mathematical induction. As an alternative proof, we develop equivalent Petri net substitutes for the building blocks of the design and verify the resultant special net using classical net theoretic methods. Based on the verification we propose a change of the arbiter to speed-up the cascade.

Hartmann J. Genrich, Robert M. Shapiro

Constructs for modeling information systems with Petri nets

Abstract

This paper is concerned with elementary and high-level Petri nets (coloured Petri nets and predicate/transition nets) and their utility for conceptual modeling of information systems. Particular features of existing net classes are discussed and additional net constructs are proposed for that purpose. Adequate conceptual models, i.e., models which reflect an intended view of an information system without any strange or artifical elements are best obtained if the following features are available to the modeler: (i) places have finite capacities (bounded places), (ii) arc expressions denote sets of variable cardinality, (iii) exclusive and shared use of side-conditions can be specified, (iv) terms denoting the set of all entities of a current marking or a specified subset thereof can be used in transition expressions, (v) static properties can be specified in state-oriented terms and impose restrictions on the dynamic properties specified in transition-oriented terms. The paper presents examples of each one of these desirables features and discusses them against the existing high-level Petri net classes or shows how they can be provided without resorting to so-called extensions.

Carlos A. Heuser, Gernot Richter

Construction of a class of safe Petri nets by presenting firing sequences

Abstract

An algorithm is proposed for constructing a Petti net model from a finite set of firing sequences. The algorithm consists of two phases. In the first phase, a language is identified in the form of a finite state automaton from given firing sequences. In the second phase, the dependency relation is extracted from the language, and the structure of a Petri net is guessed. The algorithm is for a class of safe Petri nets, and its running time is bounded by a polynomial function of given inputs.

Kunihiko Hiraishi

An efficient polynomial-time algorithm to decide liveness and boundedness of free-choice nets

Abstract

In [3] J. Esparza presented an interesting characterization of structurally live and structurally bounded Free-Choice Nets (LBFC-Nets). Exploiting this characterization in combination with new results and refined algorithms the authors formulate an O(¦P∥T∥F¦) algorithm deciding whether a Free-Choice Net is a LBFC-Net or not. Furthermore the algorithm contains a simple and efficient test to ensure that the initial marking of a LBFC-Net is live. This test is based on a simplified characterization of liveness for LBFC-Nets.

Peter Kemper, Falko Bause

Hierarchical solution of generalized Stochastic Petri Nets by means of traffic processes

Abstract

A methodology is presented for the approximate solution of large Stochastic Petri Nets that are structured into independent submodels. These subnets are aggregated to substitute nets of lower complexity to achieve a state space reduction. This is based on the estimated traffic process at a submodel's input in steady state and on a token's residence time distribution in the original submodel as equivalence criterion for matching the substitute network to the submodel. The Markov renewal process at the input of the submodel is approximated by a renewal process. Its moments and the arrival instant probabilities at the submodel are computed by means of a traffic set approach. The technique is applied to Generalized Stochastic Petri Nets and compared to Flow Equivalent Aggregation.

Guenter Klas

Concurrency relations and the safety problem for Petri nets

Abstract

A new concurrency relation for ordinary Petri nets is introduced. It gives the necessary condition for every pair of places to be marked at some marking. Irreflexiveness of this relation proves to be the sufficient condition of safety of ordinary Petri nets and necessary and sufficient condition of safety of live EFC nets. The complexity of this relation computing has a polynomial upper bound of O(X^S), where X is the number of vertices of a net.

A. V. Kovalyov

High-level nets and linear logic

Abstract

We show how algebraic high-level nets give rise to a model of intuitionistic predicate linear logic. This construction extends the correspondence between intuitionistic linear logic (ILL) and Petri nets. The model is constructed in several steps. First it is shown how a Petri net gives rise to a model of ILL. This construction is proved to be functorial. Then we show how an algebraic high-level net gives rise to a Petri net and prove that the construction is functorial. The wanted model is then arrived at through the composition of the two functors. Finally we show as an example how to express an algebraic high-level net as a set of intuitionistic predicate linear logic formulas.

Johan Lilius

Liveness and boundedness analysis for Petri nets with event graph modules

Abstract

An efficient way to cope with the complexity in modelling a large-scale system consists in decomposing it into subsystems called modules, modelling each module using Petri nets and integrating these models together to obtain the model of the whole system. This paper addresses the liveness and boundedness analysis for a Petri net model with event graph modules (also called marked graphs). We prove that each event graph module can be replaced by a simple but still equivalent event graph model called minimal representation in which the internal transitions of the initial module are removed. We also prove some properties of general Petri nets which allow to simplify the liveness and boundedness analysis.

Vanio M. Savi, Xiaolan Xie

On weighted T-systems

Abstract

Structure theory is a branch of net theory devoted to investigate the relationship between the structure and the behaviour of net system models. Many of its powerful results have been derived for some subclasses of ordinary net systems. The aim of this contribution is to draw a general perspective of the structure theory for a subclass with Marked Graph-like underlying graph but allowing weights: weighted T-graphs (WTG). Weights are convenient to properly model systems with bulk services and arrivals. Properties of WTG and the corresponding weighted T-systems (WTS) are presented at three different levels: purely structural (e.g. in consistent WTG conservativeness is equivalent to strong connectedness), inter-relationships between the structure and the behaviour (e.g. structural liveness and boundedness is equivalent to consistency and strong connectedness) and liveness and reachability characterizations (e.g. deciding liveness is linear wrt. the 1-norm of the unique minimal T-semiflow of a consistent, even unbounded, WTS). Classical results for Marked Graphs can be derived as corollaries. Nevertheless, even in live and consistent WTS, important properties of Marked Graphs do not hold (e.g. P-semiflows based characterization of reachability).

E. Teruel, P. Chrzastowski-Wachtel, J. M. Colom, M. Silva

Using Petri Nets to develop programs for PLC systems

Abstract

In this project we examined ways in which systems may be implemented on Programmable Logic Controllers. PLC systems exhibit a number of unique features, our objective was to create a practical approach to modelling systems which would lead towards implementation on PLCs.

Geoff Cutts, Shaun Rattigan

Modelling and control of complex logistic systems for manufacturing

Abstract

Logistic systems combine the different subsystems which are manufacturing processes and its informational control. Its complex system structure and discrete behaviour can be concisely modelled by using timed Petri-Nets with individual tokens. The application of this way of modelling of a complex industrial production plant leads to the investigation of complete logistical units in more detail, for example, the investigation of logistal controlled manufacturing cells.

K. Lemmer, E. Schnieder

Modelling and evaluation of a satellite system using EVAL, a Petri Net based industrial tool

Abstract

This paper reports an experiment conducted with EVAL, a Petri Nets based tool, on a satellite application. The satellite architecture is described, using EVAL specification language which provides powerful communication mechanisms (multi-rendez-vous) along with modular decomposition. In addition to interactive behaviour simulation, the tool supports exhaustive analysis techniques, with respect to logical, temporal or stochastic criteria of the system. Verification results on the satellite application are presented. We stress on the use of a modelling methodology to build analysis models.

J. C. Lloret, J. L. Roux, B. Algayres, M. Chamontin

Analysis of an Ada system using coloured Petri nets and occurrence graphs

Abstract

This paper summarizes a project that used a new prototype occurrence graph (OG) tool to analyze a hierarchical coloured Petri net. The net models the behavior of an example Ada program that controls an interrupt-driven system. Our goals were to verify the results of the prior manual analysis, further examine the Ada program design, and assess the significance of such tool support in the application of Petri net theory to Ada program development. With OG tool support, we were able to identify additional problems with this Ada program that had defied manual analysis. The new insights gained with minimal effort are very encouraging. We believe the approach we have demonstrated can, with further refinements, become a practical means of verifying Ada program designs.

William W. McLendon Jr., Richard F. Vidale

The stubborn set method in practice

Abstract

A project for studying the stubborn set method in practice is described. The stubborn set method has been implemented in PROD, a reachability analysis tool for PrT-nets, and will be studied in practical cases using PROD.

Kimmo Varpaaniemi, Marko Rauhamaa

Modeling fine grain computation via the Fusion of two extended Petri nets

Abstract

We describe an. automated modeling system which uses extended Petri nets to model dataflow programs executing on a dataflow architecture. We independently model both a dataflow algorithm and a dataflow architecture, and describe how these two models are fused. The fused model allows the parallel programmer to maintain a logical connectivity between the dataflow graph and its execution on the machine. The fused net is executed by our software to generate statistics which enable parallel programmers to efficiently map algorithms onto parallel architectures.

Linda Wilkens, James Canning, Patrick Krolak

Backmatter