Lectures on Petri Nets I: Basic Models

This contributions provides an introduction to the theory of place/transition Petri nets. Topics include the sequential and the concurrent behavior of place/ transition Petri nets, marking graphs and coverability trees, and some analysis techniques that are based on the structure of place/transition Petri nets.

The paper gives an introduction to fundamentals and recent trends in the theory of high-level nets. High-level nets are first formally derived from low-level nets by means of a quotient construction. Based on a linear-algebraic representations, we develop an invariant calculus that essentially corresponds to the algebraic core of the well-known coloured nets. We demonstrate that the modelling power of high-level nets stems from the use of expressive symbolic annotation languages, where as a typical model we consider predicate-transition nets, both concrete models and net-schemes. As examples of specific high-level analysis-tools we discuss symbolic place-invariants and reachability-trees.

In this tutorial paper, the authors discuss the motivations that led to the adoption of Petri nets for performance evaluation, define the class of Petri nets that is most frequently used for performance analysis, and present the subclasses that allow a simpler derivation of performance metrics. Definitions and discussions are paralleled with examples, thus visualizing the strong and weak points of the different alternatives.

Linear algebraic techniques for place/transition nets are surveyed. In particular, place and transition invariant vectors and their application to verification, proof and analysis of behavioral properties of marked Petri nets are presented. The considered properties are the non-reachability of a marking and conditions that hold true for all reachable markings. In addition, it is shown how the rank of the incidence matrix implies sufficient criteria and necessary criteria for liveness of bounded marked Petri nets.

The structure theory of Place/Transition net systems is surveyed — incorporating new contributions — in a tutorial style, mainly from a linear algebraic perspective. Topics included are: state equation based analysis of safety properties (e.g., boundedness, mutual exclusion, deadlock-freeness, etc.), linear invariants, siphons and traps, implicit places and their application to improve the accuracy of the state equation, and rank theorems (structural conditions for liveness and boundedness based on the rank of the incidence matrix).

A collection of 10 “rules of thumb” is presented that helps to determine the decidability and complexity of a large number of Petri net problems.

State space methods are one of the most important approaches to computer-aided analysis and verification of the behaviour of concurrent systems. In their basic form, they consist of enumerating and analysing the set of the states the system can ever reach. Unfortunately, the number of states of even a relatively small system is often far greater than can be handled in a realistic computer. The goal of this article is to analyse this state explosion problem from several perspectives. Many advanced state space methods alleviate the problem by using a subset or an abstraction of the set of states. Unfortunately, their use tends to restrict the set of analysis or verification questions that can be answered, making it impossible to discuss the methods without some taxonomy of the questions. Therefore, the article contains a lengthy discussion on alternative ways of stating analysis and verification questions, and algorithms for answering them. After that, many advanced state space methods are briefly described. The state explosion problem is investigated also from the computational complexity point of view.

The synthesis problem for nets consists in deciding whether a given graph is isomorphic to the marking graph of some net and then constructing it. This problem has been solved in the literature for various types of nets ranging from elementary nets to Petri nets. The general principle for the synthesis is to inspect regions of graphs representing extensions of places of the likely generating nets. We follow in this survey the gradual development of the theory of regions from its foundation by Ehrenfeucht and Rozenberg, with a particular insistence on the abstract meaning of the theory, which is a general product decomposition of graphs into atomic components determined by a parameter called a type of nets, and on the derivation of efficient algorithms for net synthesis based on linear algebra.

This paper retraces, collects, and summarises contributions of the authors — in collaboration with others — on the theme of Petri nets and their categorical relationships to other models of concurrency.

In this paper we have attempted an overview of linear time temporal logics interpreted over traces. We have mainly concentrated on the satisfiability and model checking problems as well as expressiveness issues. The problem of axiomatizing these logics seems to be a non-trivial task. Some partial results may be found in [39]. In [34] the authors present proof rules for the logic ISTL with a trace semantics together with a relative expressive completeness result. Reisig has also developed a kit of proof rules for a version of UNITY logic [40, 41]. The models of this logic are the non-sequential processes of a net system and the proof rules are mainly designed to help reason about distributed algorithms modelled using net systems.

At present not much is known about corresponding logics in a branching time setting. Most of the attemtps in this direction have lead to logics whose satisfiability problems are undedicable [5,25,36]. It is however the case that the model checking problem often remains tractable [5,36]. We do not know at present whether the properties expressible in such logics have any type of “all-or-none” flavour and if so whether one can develop some reduction techniques for verifying such properties. Some preliminar attempts in this direction have been made in [16,54].