Application and Theory of Petri Nets and Concurrency

In this paper we discuss several approaches to time in Petri nets. If time is considered for performance analysis, probability distributions for choices should be included into the model and thus we need Petri nets with time and stochastics. In literature, most attention is paid to models where the time is expressed by delaying transitions and for the stochastic case to continuous time models with exponential enabling distributions, known by its software tools as GSPN. Here we focus on discrete models where the time is expressed by delaying tokens and the probability distributions are discrete, because this model class has some advantages. We show how model checking methods can be applied for the non-stochastic case. For the stochastic case we show how Markov techniques can be used. We also consider structural analysis techniques, which do not need the state space.

We describe the Gadara project, a research effort whose goal is to eliminate certain classes of concurrency bugs in multithreaded software by controlling the execution of programs at run-time. The Gadara process involves three stages: modeling of the source code at compile time in the form of a Petri net, feedback control synthesis, and control logic implementation into the source code. The feedback control logic is synthesized using techniques from supervisory control of discrete event systems, where the specification captures the avoidance of certain types of concurrency bugs, such as deadlocks. We focus on the case of circular-wait deadlocks in multithreaded programs employing mutual exclusion locks for shared data. The application of the Gadara methodology to other classes of concurrency bugs is briefly discussed.

We introduce ω-Petri nets (ωPN), an extension of plain Petri nets with ω-labeled input and output arcs, that is well-suited to analyse parametric concurrent systems with dynamic thread creation. Most techniques (such as the Karp and Miller tree or the Rackoff technique) that have been proposed in the setting of plain Petri nets do not apply directly to ωPN because ωPN define transition systems that have infinite branching. This motivates a thorough analysis of the computational aspects of ωPN. We show that an ωPN can be turned into a plain Petri net that allows to recover the reachability set of the ωPN, but that does not preserve termination. This yields complexity bounds for the reachability, (place) boundedness and coverability problems on ωPN. We provide a practical algorithm to compute a coverability set of the ωPN and to decide termination by adapting the classical Karp and Miller tree construction. We also adapt the Rackoff technique to ωPN, to obtain the exact complexity of the termination problem. Finally, we consider the extension of ωPN with reset and transfer arcs, and show how this extension impacts the decidability and complexity of the aforementioned problems.

Yen proposed a construction for a semilinear representation of the reachability set of BPP-Petri nets which can be used to decide the equivalence problem of two BPP-PNs in doubly exponential time. We first address a gap in this construction which therefore does not always represent the reachability set. We propose a solution which is formulated in such a way that a large portion of Yen’s construction and proof can be retained, preserving the size of the semilinear representation and the double exponential time bound (except for possibly larger values of some constants). In the second part of the paper, we propose very efficient algorithms for several variations of the boundedness and liveness problems of BPP-PNs. For several more complex notions of boundedness, as well as for the covering problem, we show NP-completeness. To demonstrate the contrast between BPP-PNs and a slight generalization regarding edge multiplicities, we show that the complexity of the classical boundedness problem increases from linear time to coNP-hardness. Our results also imply corresponding complexity bounds for related problems for process algebras and (commutative) context-free grammars.

Generalised Stochastic Petri Nets (GSPNs) are a popular modelling formalism for performance and dependability analysis. Their semantics is traditionally associated to continuous-time Markov chains (CTMCs), enabling the use of standard CTMC analysis algorithms and software tools. Due to ambiguities in the semantic interpretation of confused GSPNs, this analysis strand is however restricted to nets that do not exhibit non-determinism, the so-called well-defined nets. This paper defines a simple semantics for every GSPN. No restrictions are imposed on the presence of confusions. Immediate transitions may be weighted but are not required to be. Cycles of immediate transitions are admitted too. The semantics is defined using a non-deterministic variant of CTMCs, referred to as Markov automata. We prove that for well-defined bounded nets, our semantics is weak bisimulation equivalent to the existing CTMC semantics. Finally, we briefly indicate how every bounded GSPN can be quantitatively assessed.

Passage time measures specification and computation for Generalized Stochastic Petri Net models have been faced in the literature from different points of view. In particular three aspects have been developed: (1) how to select a specific token (called the tagged token) and measure the distribution of the time employed from an entry to an exit point in a subnet; (2) how to specify in a flexible way any condition on the paths of interest to be measured, (3) how to efficiently compute the required distribution. In this paper we focus on the last two points: the specification and computation of complex passage time measures in (Tagged) GSPNs using the Hybrid Automata Stochastic Logic (HASL) and the statistical model checker COSMOS. By considering GSPN models of two different systems (a flexible manufacturing system and a workflow), we identify a number of relevant performance measures (mainly passage-time distributions), formally express them in HASL terms and assess them by means of simulation in the COSMOS tool. The interest from the measures specification point of view is provided by the possibility of setting one or more timers along the paths, and setting the conditions for the paths selection, based on the measured values of such timers. With respect to other specification languages allowing to use timers in the specification of performance measures, HASL provides timers suspension, reactivation, and rate change along a path.

We consider time Petri nets with multiple-server semantics. We first prove that this setting is strictly more expressive, in terms of timed bisimulation, than its single-server counterpart. We then focus on two choices for the firing of multiple instances of the same transition: the more conservative safety-wise non deterministic choice, where all firable instances may fire in any order, and a simpler alternative, First Enabled First Fired (FEFF), where only the oldest instance may fire, obviously leading to a much more compact state-space. We prove that both semantics are not bisimilar but actually simulate each other with strong timed simulations, which in particular implies that they generate the same timed traces. FEFF is then very appropriate to deal with linear timed properties of time Petri nets.

In this paper we study the complexity of Hornets, an algebraic extension of object nets. We define a restricted class: safe, elementary Hornets, to guarantee finite state spaces.

We have shown previously that the reachability problem for this class requires at least exponential space, which is a major increase when compared to safe, elementary object nets, which require polynomial space.

Here, we show how a safe, elementary Hornets can be simulated by a safe Eos, which establishes an upper bound for the complexity, since we know that that the reachability problem for safe Eos is PSpace-complete.

At the end of the eighties, continuous Petri nets were introduced for: (1) alleviating the combinatory explosion triggered by discrete Petri nets and, (2) modelling the behaviour of physical systems whose state is composed of continuous variables. Since then several works have established that the computational complexity of deciding some standard behavioural properties of Petri nets is reduced in this framework. Here we first establish the decidability of additional properties like boundedness and reachability set inclusion. We also design new decision procedures for the reachability and lim-reachability problems with a better computational complexity. Finally we provide lower bounds characterising the exact complexity class of the boundedness, the reachability, the deadlock freeness and the liveness problems.

In this paper we investigate the behaviour of GALS (Globally Asynchronous Locally Synchronous) systems in the context of VLSI circuits. The specification of a system is given in the form of a Petri net. Our aim is to re-design the system to optimise signal management, by grouping together concurrent events. Looking at the concurrent reachability graph of the given Petri net, we are interested in discovering events that appear in ‘bundles’, so that they all can be executed in one clock tick. The best candidates for bundles are sets of events that appear and re-appear over and over again in the same configurations, forming ‘persistent’ sets of events. Persistence was considered so far only in the context of sequential semantics. Here we introduce a notion of persistent steps and discuss their basic properties. We then introduce a formal definition of a bundle and propose an algorithm to prune the behaviour of a system, so that only bundle steps remain. The pruned reachability graph represents the behaviour of a re-engineered system, which in turn can be implemented in a new Petri net using the standard techniques of net synthesis. The proposed algorithm prunes reachability graphs of persistent and safe nets leaving bundles that represent maximally concurrent steps.

In this paper we introduce a technique to encode spatial attributes of dynamic systems using coloured Petri nets and show how it can be applied to biological systems within the spirit of BioModel Engineering. Our approach can be equally applied to qualitative, stochastic, continuous or hybrid models of the same physical system, and can be used as the basis for multiscale modelling. We illustrate our approach with two case studies, one from the continuous and one from the stochastic paradigm. In this paper we only discuss the case of finite colours, and by unfolding our method can take advantage of all the analytical machinery and simulation techniques that have been developed for the uncoloured family of Petri net classes.

The paper proposes an user-based solution for the vehicle relocation problem in car sharing systems. In particular, the impact of a mechanism of economic incentives based on a real time monitoring of vehicles distribution among the parking areas is assessed. We consider three different operative conditions that are described by the Unified Modeling Language and modeled in a Timed Petri Net (TPN) framework. In order to show and compare the effectiveness of the adopted management strategies, the real case study of an electric-car sharing system is evaluated and simulated in the TPN environment. The results underline how the proposed solution leads to an improvement of the overall system performances, by highlighting at the same time the limits of such a strategy.

Event processing networks emerged as a paradigm to implement applications that interact with distributed, loosely coupled components. Such a network consists of event producers, event consumers, and event processing agents that implement the application logic. Event processing networks are typically intended to process an extensive amount of events. Hence, there is a need for performance and scalability evaluation at design time. In this paper, we take up the challenge of modelling event processing networks using coloured Petri nets. We outline how this type of system is modelled and illustrate the formalisation with the widely used showcase of the Fast Flower Delivery Application (FFDA). Further, we report on the validation of the obtained coloured Petri net with an implementation of the FFDA in the ETALIS framework. Finally, we show how the net of the FFDA is employed for analysis with CPN-Tools.

Process discovery is the problem of, given a log of observed behaviour, finding a process model that ‘best’ describes this behaviour. A large variety of process discovery algorithms has been proposed. However, no existing algorithm guarantees to return a fitting model (i.e., able to reproduce all observed behaviour) that is sound (free of deadlocks and other anomalies) in finite time. We present an extensible framework to discover from any given log a set of block-structured process models that are sound and fit the observed behaviour. In addition we characterise the minimal information required in the log to rediscover a particular process model. We then provide a polynomial-time algorithm for discovering a sound, fitting, block-structured model from any given log; we give sufficient conditions on the log for which our algorithm returns a model that is language-equivalent to the process model underlying the log, including unseen behaviour. The technique is implemented in a prototypical tool.

In this paper we tackle the problem of verifying whether a labeled partial order (LPO) is executable in a Petri net. In contrast to sequentially ordered runs an LPO includes both, information about dependencies and independencies of events. Consequently an LPO allows a precise and intuitive specification of the behavior of a concurrent or distributed system. In this paper we consider Petri nets with arc weights, namely marked place/transition-nets (p/t-nets). Accordingly the question is whether a given LPO is an execution of a given p/t-net.

Different approaches exist to define the partial language (i.e. the set of executions) of a p/t-net. Each definition yields a different verification algorithm, but in terms of runtime all these algorithms perform quite poorly for most examples. In this paper a new compact characterization of the partial language of a p/t-net will be introduced, optimized with respect to the verification problem. The goal is to develop an algorithm to efficiently decide the verification problem.

Modularity is a mandatory principle to apply Petri nets to real world-sized systems. Modular extensions of Petri nets allow to create complex models by combining smaller entities. They facilitate the modeling and verification of large systems by applying a divide and conquer approach and promoting reuse. Modularity includes a wide range of notions such as encapsulation, hierarchy and instantiation. Over the years, Petri nets have been extended to include these mechanisms in many different ways. The heterogeneity of such extensions and their definitions makes it difficult to reason about their common features at a general level. We propose in this article an approach to standardize the semantics of modular Petri nets formalisms, with the objective of gathering even the most complex modular features from the literature. This is achieved with a new Petri nets formalism, called the LLAMAS Language for Advanced Modular Algebraic Nets (LLAMAS). We focus principally on the composition mechanism of LLAMAS, while introducing the rest of the language with an example. Our approach has two positive outcomes. First, the definition of new formalisms is facilitated, by providing common ground for the definition of their semantics. Second, it is possible to reason at a general level on the most advanced verification techniques, such as the recent advances in the domain of decision diagrams.

We consider asynchronously composed I/O-Petri nets (AIOPNs) with built-in communication channels. They are equipped with a compositional semantics in terms of asynchronous I/O-transition systems (AIOTSs) admitting infinite state spaces. We study various channel properties that deal with the production and consumption of messages exchanged via the communication channels and establish useful relationships between them. In order to support incremental design we show that the channel properties considered in this work are preserved by asynchronous composition, i.e. they are compositional. As a crucial result we prove that the channel properties are decidable for AIOPNs.

MARCIE is a tool for the analysis of generalized stochastic Petri nets which can be augmented by rewards. The supported analysis methods range from qualitative and quantitative standard properties to model checking of established temporal logics. MARCIE’s analysis engines for bounded Petri net models are based on Interval Decision Diagrams. They are complemented by simulative and approximative engines to allow for quantitative reasoning on unbounded models. Most of the quantitative analyses benefit from a multi-threaded implementation. This paper gives an overview on MARCIE’s functionality and architecture and reports on the recently added feature of CSRL and PLTLc model checking.

CPN Tools is an advanced tool for editing, simulating, and analyzing colored Petri nets. This paper discusses the fourth major release of the tool, which makes it simple to use the tool for ordinary Petri nets, including adding inhibitor and reset arcs, and PNML export. This version also supports declarative modeling using constraints, and adds an extension framework making it easy for third parties to extend CPN Tools using Java.