Skip to main content

Über dieses Buch

This book constitutes the refereed proceedings of the 34th International Conference on Applications and Theory of Petri Nets and Concurrency, PETRI NETS 2013, held in Milan, Italy, in June 2013. The 18 regular papers and 2 tool papers presented were carefully reviewed and selected from 56 submissions. The book also contains 2 invited talks. All current issues on research and development in the area of Petri nets and related models of concurrent systems are addressed.



Invited Papers

The Right Timing: Reflections on the Modeling and Analysis of Time

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.
Kees van Hee, Natalia Sidorova

Eliminating Concurrency Bugs in Multithreaded Software: An Approach Based on Control of Petri Nets

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.
Stéphane Lafortune, Yin Wang, Spyros Reveliotis

Regular Papers

Contextual Merged Processes

We integrate two compact data structures for representing state spaces of Petri nets: merged processes and contextual prefixes. The resulting data structure, called contextual merged processes (CMP), combines the advantages of the original ones and copes with several important sources of state space explosion: concurrency, sequences of choices, and concurrent read accesses to shared resources. In particular, we demonstrate on a number of benchmarks that CMPs are more compact than either of the original data structures. Moreover, we sketch a polynomial (in the CMP size) encoding into SAT of the model-checking problem for reachability properties.
César Rodríguez, Stefan Schwoon, Victor Khomenko

ω-Petri Nets

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.
Gilles Geeraerts, Alexander Heussner, M. Praveen, Jean-François Raskin

Results on Equivalence, Boundedness, Liveness, and Covering Problems of BPP-Petri Nets

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.
Ernst W. Mayr, Jeremias Weihmann

A Semantics for Every GSPN

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.
Christian Eisentraut, Holger Hermanns, Joost-Pieter Katoen, Lijun Zhang

Expressing and Computing Passage Time Measures of GSPN Models with HASL

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.
Elvio Gilberto Amparore, Paolo Ballarini, Marco Beccuti, Susanna Donatelli, Giuliana Franceschinis

On Multi-enabledness in Time Petri Nets

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.
Hanifa Boucheneb, Didier Lime, Olivier H. Roux

Complexity Results for Elementary Hornets

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.
Michael Köhler-Bußmeier, Frank Heitmann

Complexity Analysis of Continuous Petri Nets

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.
Estíbaliz Fraca, Serge Haddad

Step Persistence in the Design of GALS Systems

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.
Johnson Fernandes, Maciej Koutny, Marta Pietkiewicz-Koutny, Danil Sokolov, Alex Yakovlev

A Taxonomy of Persistent and Nonviolent Steps

A concurrent system is persistent if throughout its operation no activity which became enabled can subsequently be prevented from being executed by any other activity. This is often a highly desirable (or even necessary) property; in particular, if the system is to be implemented in hardware. Over the past 40 years, persistence has been investigated and applied in practical implementations assuming that each activity is a single atomic action which can be represented, for example, by a single transition of a Petri net. Recently, it turned out that to deal with the synthesis of GALS systems one also needs to consider activities represented by steps, each step being a set of simultaneously executed transitions. Moving into the realm of step based execution, semantics creates a wealth of new fundamental problems and questions. In particular, there are different ways in which the standard notion of persistence could be lifted from the level of sequential semantics to the level of step semantics. Moreover, one may consider steps which are persistent and cannot be disabled by other steps, as well as steps which are nonviolent and cannot disable other steps. In this paper, we provide a classification of different types of persistence and nonviolence, both for steps and markings of pt-nets. We also investigate behavioural and structural properties of such notions.
Maciej Koutny, Łukasz Mikulski, Marta Pietkiewicz-Koutny

Colouring Space - A Coloured Framework for Spatial Modelling in Systems Biology

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.
David Gilbert, Monika Heiner, Fei Liu, Nigel Saunders

The Vehicle Relocation Problem in Car Sharing Systems: Modeling and Simulation in a Petri Net Framework

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.
Monica Clemente, Maria Pia Fanti, Agostino M. Mangini, Walter Ukovich

Net-Based Analysis of Event Processing Networks – The Fast Flower Delivery Case

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.
Matthias Weidlich, Jan Mendling, Avigdor Gal

Hierarchical Conformance Checking of Process Models Based on Event Logs

Process mining techniques aim to extract knowledge from event logs. Conformance checking is one of the hard problems in process mining: it aims to diagnose and quantify the mismatch between observed and modeled behavior. Precise conformance checking implies solving complex optimization problems and is therefore computationally challenging for real-life event logs. In this paper a technique to apply hierarchical conformance checking is presented, based on a state-of-the-art algorithm for deriving the subprocesses structure underlying a process model. Hierarchical conformance checking allows us to decompose problems that would otherwise be intractable. Moreover, users can navigate through conformance results and zoom into parts of the model that have a poor conformance. The technique has been implemented as a ProM plugin and an experimental evaluation showing the significance of the approach is provided.
Jorge Munoz-Gama, Josep Carmona, Wil M. P. van der Aalst

Discovering Block-Structured Process Models from Event Logs - A Constructive Approach

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.
Sander J. J. Leemans, Dirk Fahland, Wil M. P. van der Aalst

Faster Verification of Partially Ordered Runs in Petri Nets Using Compact Tokenflows

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.
Robin Bergenthum

Unifying the Semantics of Modular Extensions of Petri Nets

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.
Alexis Marechal, Didier Buchs

Channel Properties of Asynchronously Composed Petri Nets

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.
Serge Haddad, Rolf Hennicker, Mikael H. Møller

Tool Papers

MARCIE – Model Checking and Reachability Analysis Done Efficiently

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.
Monika Heiner, Christian Rohr, Martin Schwarick

CPN Tools 4: Multi-formalism and Extensibility

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.
Michael Westergaard


Weitere Informationen