Applications and Theory of Petri Nets

We present a framework for the component-based construction of real-time systems. The framework is based on the BIP (Behaviour, Interaction, Priority) semantic model, characterized by a layered representation of components. Compound components are obtained as the composition of atomic components specified by their behaviour and interface, by using connectors and dynamic priorities. Connectors describe structured interactions between atomic components, in terms of two basic protocols: rendezvous and broadcast. Dynamic priorities are used to select amongst possible interactions - in particular, to express scheduling policies.

The BIP framework has been implemented in a language and a toolset. The BIP language offers primitives and constructs for modelling and composing atomic components described as state machines, extended with data and functions in C. The BIP toolset includes an editor and a compiler for generating from BIP programs, C++ code executable on a dedicated platform. It also allows simulation and verification of BIP programs by using model checking techniques.

BIP supports a model-based design methodology involving three steps:

We provide two examples illustrating the methodology.

Further information is available at:

http://www-verimag.imag.fr/~async/bip.php

In this paper we advocate a unifying technique for description of Petri net semantics. Semantics, i.e. a possible behaviour, is basically a set of node-labelled and arc-labelled directed acyclic graphs, called token flows, where the graphs are distinguished up to isomorphism. The nodes of a token flow represent occurrences of transitions of the underlying net, so they are labelled by transitions. Arcs are labelled by multisets of places. Namelly, an arc between an occurrence x of a transition a and an occurrence y of a transition b is labelled by a multiset of places, saying how many tokens produced by the occurrence x of the transition a is consumed by the occurrence y of the transition b. The variants of Petri net behaviour are given by different interpretation of arcs and different structure of token flows, resulting in different sets of labelled directed acyclic graphs accepted by the net. We show that the most prominent semantics of Petri nets, namely processes of Goltz and Reisig, partial languages of Petri nets introduced by Grabowski, rewriting terms of Meseguer and Montanari, step sequences as well as classical occurrence (firing) sequences correspond to different subsets of token flows. Finally, we discuss several results achieved using token flows during the last four years, including polynomial test for the acceptance of a partial word by a Petri net, synthesis of Petri nets from partial languages and token flow unfolding.

The functioning of a living cell consists of a huge number of individual reactions that interact with each other. These reactions are regulated, and the two main regulation mechanisms are facilitation/acceleration and inhibition/retardation. The interaction between individual biochemical reactions takes place through their influence on each other, and this influence happens through the two mechanisms mentioned above.

In our lecture we present a formal framework for the investigation of biochemical reactions - it is based on reaction systems. We motivate this framework by explicitely stating a number of assumptions/axioms that (we believe) hold for a great number of biochemical reactions - we point out that these assumptions are very different from the ones underlying traditional models of computation such as Petri Nets. We discuss some basic properties of reaction systems, and demonstrate how to capture and analyze, in our formal framework, some biochemistry related notions.

The lecture is of a tutorial character and self-contained.

Petri nets are frequently composed of given nets. Literature suggests a lot of different composition operators, for different purposes and different classes of Petri nets. Formal definitions are frequently surprisingly technical, not matching the intuitive elegance of their graphical counterpart.

We provide the formal framework for a simple composition operator, adequate for many classes of Petri net applications. It requires a minimum of fairly intuitive technicalities from its users and readers. The operator furthermore is associative, thus meeting the minimal algebraic requirements when composing a large system out of several smaller ones.

When designing complex systems, mechanisms for structuring, composing, and reusing system components are crucial. Today, there are many approaches for equipping Petri nets with such mechanisms. In the context of defining a standard interchange format for Petri nets, modular PNML was defined as a mechanism for modules in Petri nets that is independent from a particular version of Petri nets and that can mimic many composition mechanisms by a simple import and export concept.

Due to its generality, the semantics of modular PNML was only informally defined. Moreover, modular PNML did not define which concepts could or should be subject to import and export in high-level Petri nets.

In this paper, we formalise a minimal version of modular high-level Petri nets, which is based on the concepts of modular PNML. This shows that modular PNML can be formalised once a specific version of Petri net is fixed. Moreover, we present and discuss some more advanced features of modular Petri nets that could be included in the standard. This way, we provide a formal foundation and a basis for a discussion of features to be included in the upcoming standard of a module concept for Petri nets in general and for high-level nets in particular.

In previous works we defined ν-APNs, an extension of P/T nets with the capability of creating and managing pure names. We proved that, though reachability is undecidable, coverability remains decidable for them. We also extended P/T nets with the capability of nets to replicate themselves, creating a new component, initially marked in some fixed way, obtaining g-RN systems. We proved that these two extensions of P/T nets are equivalent, so that g-RN systems have undecidable reachability and decidable coverability. Finally, for the class of the so called ν-RN systems, P/T nets with both name creation and replication, we proved that they are Turing complete, so that also coverability turns out to be undecidable. In this paper we study how can we restrict the models of ν-APNs (and, therefore, g-RN systems) and ν-RN systems in order to keep decidability of reachability and coverability, respectively. We prove that if we forbid synchronizations between the different components in a g-RN system, then reachability is still decidable. The proof is done by reducing it to reachability in a class of multiset rewriting systems, similar to Recursive Petri Nets. Analogously, if we forbid name communication between the different components in a ν-RN system, or restrict communication to happen only for a given finite set of names, we obtain decidability of coverability.

Step transition systems form a powerful model to describe the concurrent behaviors of distributed or parallel systems. They offer also a general framework for the study of marking graphs of Petri nets [22]. In this paper we investigate a natural labeled partial order semantics for step transition systems. As opposed to [19] we allow for autoconcurrency by considering steps that are multisets of actions. First we prove that the languages of step transition systems are precisely the width-bounded languages that are step-closed and quasi-consistent. Extending results from [19] we focus next on finite step transition systems and characterize their languages in the line of Buchi’s theorem. Our main result present six equivalent conditions in terms of regularity and MSO-definability for a set of labeled partial orders to be recognized by some finite step transition system.

Consider a Markovian Petri net with race policy. The marking process has a “product form” stationary distribution if the probability of viewing a given marking can be decomposed as the product over places of terms depending only on the local marking. First we observe that the Deficiency Zero Theorem of Feinberg, developped for chemical reaction networks, provides a structural and simple sufficient condition for the existence of a product form. In view of this, we study the classical subclass of bounded free-choice nets. Roughly, we show that the only such Petri nets having a product form are the state machines which can alternatively be viewed as Jackson networks.

A new algorithm for bisimilarity minimization of labelled directed graphs is presented. Its time consumption is O(m logn), where n is the number of states and m is the number of transitions. Unlike earlier algorithms, it meets this bound even if the number of different labels of transitions is not fixed. It is based on refining a partition on states with respect to the labelled transitions. A splitter is a pair consisting of a set in the partition and a label. Earlier algorithms consume lots of time in scanning splitters that have no corresponding relevant transitions. The new algorithm avoids this by maintaining the sets of the corresponding transitions. To facilitate this, a refinable partition data structure with amortized constant time operations is introduced. Detailed pseudocode and correctness proof are presented, as well as some measurements.

We present a symbolic method for p-semiflow computation, based on zero-suppressed decision diagrams. Both the traditional explicit methods and our new symbolic method rely on Farkas’ algorithm, and compute a generator set from which any p-semiflow for the Petri net can be derived through a linear combination. We demonstrate the effectiveness of four variants of our algorithm by applying them on a suite of Petri net models, showing that our symbolic approach can produce results in cases where the explicit approach is infeasible.

In this paper, we study partially ordered structures associated to occurrence nets. An occurrence net is endowed with a symmetric, but in general non transitive, concurrency relation. By applying known techniques in lattice theory, from any such relation one can derive a closure operator, and then an orthocomplemented lattice. We prove that, for a general class of occurrence nets, those lattices, formed by closed subsets of net elements, are orthomodular. A similar result was shown starting from a simultaneity relation defined, in the context of special relativity theory, on Minkowski spacetime. We characterize the closed sets, and study several properties of lattices derived from occurrence nets; in particular we focus on properties related to K-density. We briefly discuss some variants of the construction, showing that, if we discard conditions, and only keep the partial order on events, the corresponding lattice is not, in general, orthomodular.

In [LJ06] Lorenz and Juhás raised the question of whether there exists a suitable formalism for the representation of infinite families of partial orders generated by Petri nets. Restricting ourselves to bounded p/t-nets, we propose Hasse diagram generators as an answer. We show that Hasse diagram generators are expressive enough to represent the partial order language of any bounded p/t net. We prove as well that it is decidable both whether the (possible infinite) family of partial orders represented by a given Hasse diagram generator is included on the partial order language of a given p/t-net and whether their intersection is empty. Based on this decidability result, we prove that the partial order languages of two given Petri nets can be effectively compared with respect to inclusion. Finally we address the synthesis of k-safe p/t-nets from Hasse diagram generators.

In road transportation networks, such as freeways, motorways or highways, variable speed limit (VSL) control is one of the most efficient strategies to substantially improve traffic flow and solve or reduce the congestion problem. One way to design control strategies applicable in real time is to represent the vehicle flows with a hybrid dynamic model. In this context, Batches Petri Nets (BPN) and their extensions, are well adapted for the modeling of such systems as they intend to model variable delays on continuous flows by adding special nodes, called batch nodes, to the continuous and hybrid Petri nets. Using BPN with controllable batch speed, this paper studies a portion of the A12 highway in The Netherlands. This hybrid representation leads to the evaluation of several real time VSL control laws in accordance with the accumulation front of vehicles.

We present a novel, operational, formal model for scenario-based modeling with Petri nets. A scenario-based model describes the system behavior in terms of partial runs, called scenarios. This paradigm has been formalized in message sequence charts (MSCs) and live sequence charts (LSCs) which are in industrial and academic use. A particular application for scenarios are process models in disaster management where system behavior has to be adapted frequently, occasionally at run-time. An operational semantics of scenarios would allow to execute and adapt such systems on a formal basis.

In this paper, we present a class of Petri nets for specifying and modeling systems with scenarios and anti-scenarios. We provide an operational semantics allowing to iteratively construct partially ordered runs that satisfy a given specification. We prove the correctness of our results.

In this contribution we propose an algebraic extension of object nets. Object nets, also known as nets within nets, allow nets itself as tokens. The algebraic structure introduced here refers to the topology of these net-tokens, i.e. we have operators which compose nets. Object nets that use net operations in arc expression are called Higher Order Recursive Nets, or short: Hornets.

Web Service orchestrations are compositions of different Web Services to form a new service. The services called during the orchestration guarantee a given Quality of Service (QoS) to the orchestrator, usually in the form of contracts. These contracts can then be used by the orchestrator to deduce the contract it can offer to its own clients, by performing contract composition. An implicit monotonicity assumption in contract based QoS management is: “the better the component services perform, the better the orchestration’s performance will be”.

In some orchestrations, however, monotonicity can be violated, i.e., the performance of the orchestration improves when the performance of a component service degrades. This is highly undesirable since it can render the process of contract composition inconsistent.

In this paper we formally define monotonicity for orchestrations modelled by Colored Occurrence Nets (CO-nets) and we characterize the classes of monotonic orchestrations. Contracts can be formulated as hard, possibly nondeterministic, guarantees, or alternatively as probabilistic guarantees. Our work covers both cases. We show that few orchestrations are indeed monotonic, mostly because of complex interactions between control, data, and timing. We also provide user guidelines to get rid of non-monotonicity when designing orchestrations.

The ASCoVeCo State space Analysis Platform (ASAP) is a tool for performing explicit state space analysis of coloured Petri nets (CPNs) and other formalisms. ASAP supports a wide range of state space reduction techniques and is intended to be easy to extend and to use, making it a suitable tool for students, researchers, and industrial users that would like to analyze protocols and/or experiment with different algorithms. This paper presents ASAP from these two perspectives.

Coloured Petri nets (CP-nets or CPNs) is a widely used formalism for describing concurrent systems. CPN Tools provides a mature environment for constructing, simulating, and performing analysis of CPN models. CPN Tools also has limitations if, for example, one wishes to extend the analysis capabilities or to integrate CPN models into external applications. In this paper we present Access/CPN, a framework that facilitates such extensions. Access/CPN consists of two interfaces: one written in Standard ML, which is very close to the simulator component of CPN Tools, and one written in Java, providing an object-oriented representation of CPN models, a means to load models created using CPN Tools, and an interface to the simulator. We illustrate Access/CPN by providing the complete implementation of a simple command-line state space exploration tool.

DSSZ-MC supports the symbolic analysis of bounded place/ transition Petri nets extended by read, inhibitor, equal, and reset arcs. No previous knowledge of the precise boundedness degree is required. It contains tools for the efficient analysis of standard properties (boundedness, liveness, reversibility) and CTL model checking, built on an object-oriented implementation of Zero-suppressed Binary Decision Diagrams and Interval Decision Diagrams. The main features are saturation-based state space generation, analysis of strongly connected components, dead state analysis with trace generation, and CTL model checking by limited backward reachability analysis. The tool is available for Windows, Linux, and Mac/OS.

Discrete-event systems have gained a lot of interest due to their wide range of applications. SDES is a unified description for stochastic discrete-event systems. The aim is to use this description as a basis of a new multi-formalism modeling framework. In this paper, we introduce PDETool, which is based on SDES description. This modeling tool provides features for construction and translation of models into the XML-based input language of an SDES-based simulation engine that is developed for this purpose. Currently, we have implemented some useful extensions of Petri nets, such as stochastic Petri nets (SPNs), stochastic reward nets (SRNs) and stochastic activity networks (SANs) in this framework. PDETool is easily extensible to support a wide range of graphical and non-graphical formalisms. Furthermore, it facilitates the construction, animation and simulation of models. This tool has some advantages over the existing multi-formalism modeling and simulation tools, which will be mentioned in this paper.