Skip to main content
main-content

Über dieses Buch

This book constitutes the proceedings of the 37th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2016, held in Toruń, Poland, in June 2016. Petri Nets 2016 was co-located with the Application of Concurrency to System Design Conference, ACSD 2016.

The 16 papers including 3 tool papers with 4 invited talks presented together in this volume were carefully reviewed and selected from 42 submissions.

Papers presenting original research on application or theory of Petri nets, as well as contributions addressing topics relevant to the general field of distributed and concurrent systems are presented within this volume.

Inhaltsverzeichnis

Frontmatter

Distinguished Carl Adam Petri Lecture

Frontmatter

Reasoning About Discovery Clouds

Abstract
A discovery cloud is a set of automated, cloud-hosted services to which individuals may outsource their routine and not-so-routine research tasks: finding relevant data, inferring links between data, running computational experiments, inferring new knowledge claims, evaluating the credibility of knowledge claims produced by others, designing experiments, and so on. If developed successfully, a discovery cloud can accelerate and democratize access to data and knowledge tools and the collaborative construction of new knowledge. Such systems are also fascinating to consider from a reasoning perspective because they integrate great complexity at multiple levels: the underlying cloud-based hardware and software, for which issues of reliability and responsiveness may be paramount; the knowledge bases and inference engines that sit on that cloud substrate, for which issues of correctness may be less well defined; and the human communities that form around the discovery clouds, and that arguably form as much as part of the cloud as the hardware, software, and data. I raise questions here about what it might mean to reason about such systems. I do not provide any answers.
Ian Foster

Invited Talks

Frontmatter

From Actions, Transactions, and Processes to Services

Abstract
For the problem domain of business process engineering we introduce, model, and formalize notions of business processes such as action, actor, event, business process, and business transaction. In addition, for the solution domain of service-oriented architectures (SOA) we introduce, model, and formalize notions of service, service composition, service-oriented architecture, and layered SOA in a systematic way. We do that by a rigorous mathematical system model. For that purpose, we first develop a basic mathematical system model for formalizing fundamental concepts of processes and services. The goal is to provide a minimal set of formal modeling concepts, nevertheless expressive enough to formalize key notions and concepts in business process engineering and service-oriented architectures capturing also their mutual relationships. This way, the relationship between central notions in business process models is captured formally, which provides a basis for a methodology for deriving the systematic specification and design of service-oriented architectures from business process modeling. The purpose of the approach is manifold; one goal is a clear definition of terminology, concepts, terms, and models in business process modeling and SOA; another goal is a rigorous formal basis for the specification, design, and development of business processes and, in particular, SOAs. We end up with a strictly formal concept for the development steps from business process models to services as part of a SOA-oriented development process.
Manfred Broy

Decidability Border for Petri Nets with Data: WQO Dichotomy Conjecture

Abstract
In Petri nets with data, every token carries a data value, and executability of a transition is conditioned by a relation between data values involved. Decidability status of various decision problems for Petri nets with data may depend on the structure of data domain. For instance, if data values are only tested for equality, decidability status of the reachability problem is unknown (but decidability is conjectured). On the other hand, the reachability problem is undecidable if data values are additionally equipped with a total ordering.
We investigate the frontiers of decidability for Petri nets with various data, and formulate the WQO Dichotomy Conjecture: under a mild assumption, either a data domain exhibits a well quasi-order (in which case one can apply the general setting of well-structured transition systems to solve problems like coverability or boundedness), or essentially all the decision problems are undecidable for Petri nets over that data domain.
Sławomir Lasota

Petri Net Synthesis

Frontmatter

Characterising Petri Net Solvable Binary Words

Abstract
A word is called Petri net solvable if it is isomorphic to the reachability graph of an unlabelled Petri net. In this paper, the class of finite, two-letter, Petri net solvable words is studied. A linear time, necessary condition allows for an educated guess at which words are solvable and which are not. A full decision procedure with a time complexity of \(O(n^2)\) can be built based on letter counting. The procedure is fully constructive and can either yield a Petri net solving a given word or determine why this fails. Algorithms solving the same problem based on systems of integer inequalities reflecting the potential Petri net structure are only known to be in \(O(n^3)\). Finally, the decision procedure can be adapted from finite to cyclic words.
Eike Best, Evgeny Erofeev, Uli Schlachter, Harro Wimmel

The Power of Prime Cycles

Abstract
In this paper, we shall examine properties of labelled transition systems which are motivated by system synthesis. Most of them are necessary conditions for synthesis by Petri nets to be successful. They can be checked in a pre-synthesis phase, allowing the immediate rejection of transition systems not satisfying them as non-synthesisable. The order of checking such conditions plays an important role in pre-synthesis optimisation. It is particularly desirable to know which conditions are implied by others, especially if the latter can be machine-verified more simply than the former. The purpose of this paper is to describe some mathematical results exhibiting a number of such implications.
Two properties called strong cycle-consistency and full backward determinism, respectively, are particularly hard to check. They are generalised counterparts of the marking equation of Petri net theory. We show that under some circumstances, they may be deduced from other properties which are easier to check. Amongst these other properties, the prime cycle property plays a particularly important role, not just because it is strong enough to imply others, but also because it is interesting to be checked on its own, if synthesis is targetted towards choice-free Petri nets.
Eike Best, Raymond Devillers

Petri Net Synthesis for Restricted Classes of Nets

Abstract
This paper first recapitulates an algorithm for Petri net synthesis. Then, this algorithm is extended to special classes of Petri nets. For this purpose, any combination of the properties plain, pure, conflict-free, homogeneous, k-bounded, generalized T-net, generalized marked graph, place-output-nonbranching and distributed can be specified. Finally, a fast heuristic and an algorithm for minimizing the number of places in the synthesized Petri net is presented and evaluated experimentally.
Uli Schlachter

Tools

Frontmatter

Renew 2.5 – Towards a Comprehensive Integrated Development Environment for Petri Net-Based Applications

Abstract
Renew (The Reference Net Workshop) is an extensible Petri net IDE that supports the development and execution of high-level Petri nets and other modeling techniques. The Reference net formalism – the major formalism for Renew – includes concepts such as net instances, synchronous channels and seamless Java integration. It combines the advantages of Petri nets and object-oriented programming for the development of concurrent and distributed software systems. Modeling support of Renew focuses on convenience and ease for Petri net development. An outstanding feature is the support for multi-formalism simulation. The plugin architecture of Renew enables the developers to extend the IDE for instance with additional formalisms. Alternatively to the inline mode – within the graphical user interface – the Simulator can also be run in a headless server fashion. Several configurations of Renew are available, which are constituted through selections of plugins providing specialized functionality for multiple platforms. In this manner the Renew family constitutes a product line architecture. Renew is available free of charge including the Java source code. In this contribution we provide information about Renew’s functionality and architecture as well as the development of the tool set over the last decade.
Lawrence Cabac, Michael Haustermann, David Mosteller

AB-QSSPN: Integration of Agent-Based Simulation of Cellular Populations with Quasi-Steady State Simulation of Genome Scale Intracellular Networks

Abstract
We present a tool for simulation of populations of living cells interacting in spatial structures. Each cell is modelled with the Quasi-Steady Petri Net that integrates dynamic regulatory network expressed with a Petri Net (PN) and Genome Scale Metabolic Networks (GSMN) where linear programming is used to explore the steady-state metabolic flux distributions in the whole-cell model.
Similar simulations have already been conducted for single cells, but we present an architecture to simulate populations of millions of interacting cells organized in spatial structures which can be used to model tumour growth or formation of tuberculosis lesions. For that we use the Spark framework and organize the computation in an agent based “think like a vertex” fashion as in Pregel like systems. In the cluster we introduce a special kind of per node caching to speed up computation of the steady-state metabolic flux.
Our tool can be used to provide a mechanistic link between genotype and behaviour of multicellular system.
Wojciech Ptak, Andrzej M. Kierzek, Jacek Sroka

PetriDotNet 1.5: Extensible Petri Net Editor and Analyser for Education and Research

Abstract
PetriDotNet is an extensible Petri net editor and analysis tool originally developed to support the education of formal methods. The ease of use and simple extensibility fostered more and more algorithmic developments. Thanks to the continuous interest of developers (especially M.Sc. and Ph.D. students who choose PetriDotNet as the framework of their thesis project), by now PetriDotNet became an analysis platform, providing various cutting-edge model checking algorithms and stochastic analysis algorithms. As a result, industrial application of the tool also emerged in recent years. In this paper we overview the main features and the architecture of PetriDotNet, and compare it with other available tools.
András Vörös, Dániel Darvas, Vince Molnár, Attila Klenik, Ákos Hajdu, Attila Jámbor, Tamás Bartha, István Majzik

Applications

Frontmatter

Transforming CPN Models into Code for TinyOS: A Case Study of the RPL Protocol

Abstract
TinyOS is a widely used platform for the development of networked embedded systems offering a programming model targeting resource constrained devices. We present a semi-automatic software engineering approach where Coloured Petri Net (CPNs) models are used as a starting point for developing protocol software for the TinyOS platform. The approach consists of five refinement steps that allow a developer to gradually transform a platform-independent CPN model into a platform-specific model that enables automatic code generation. To evaluate our approach, we use it to obtain an implementation of the IETF RPL routing protocol for sensor networks.
Lars Michael Kristensen, Vegard Veiset

Realizability of Schedules by Stochastic Time Petri Nets with Blocking Semantics

Abstract
This paper considers realizability of schedules by stochastic concurrent timed systems. Schedules are high level views of desired executions represented as partial orders decorated with timing constraints, while systems are represented as elementary stochastic time Petri nets. We first consider logical realizability: a schedule is realizable by a net \(\mathcal {N}\) if it embeds in a time process of \(\mathcal {N}\) that satisfies all its constraints. However, with continuous time domains, the probability of a time process that realizes a schedule is null. We hence consider probabilistic realizability up to \(\alpha \) time units, that holds if the probability that \(\mathcal {N}\) logically realizes S with constraints enlarged by \(\alpha \) is strictly positive. Upon a sensible restriction guaranteeing time progress, logical and probabilistic realizability of a schedule can be checked on the finite set of symbolic prefixes extracted from a bounded unfolding of the net. We give a construction technique for these prefixes and show that they represent all time processes of a net occurring up to a given maximal date. We then show how to verify existence of an embedding and compute the probability of its realization.
Loïc Hélouët, Karim Kecir

ABCD: A User-Friendly Language for Formal Modelling and Analysis

Abstract
This paper presents an algebra of coloured Petri nets called the Asynchronous Box Calculus with Data, or abcd for short. abcd allows to model complex systems using a user-friendly and high-level syntax. In particular, parts of the model can be directly programmed in Python [21], which allows to embed complex computation and data values within a model. A compiler for abcd is shipped with the toolkit snakes [16, 18] and abcd has been used for years, which is quickly surveyed. This paper is the first complete and formal presentation of the language and its semantics. It also presents uses cases of abcd for the modelling and analysis of various systems.
Franck Pommereau

Health Monitoring of a Planetary Rover Using Hybrid Particle Petri Nets

Abstract
This paper focuses on the application of a Petri Net-based diagnosis method on a planetary rover prototype. The diagnosis is performed by using a model-based method in the context of health management of hybrid systems. In system health management, the diagnosis task aims at determining the current health state of a system and the fault occurrences that lead to this state. The Hybrid Particle Petri Nets (HPPN) formalism is used to model hybrid systems behavior and degradation, and to define the generation of diagnosers to monitor the health states of such systems under uncertainty. At any time, the HPPN-based diagnoser provides the current diagnosis represented by a distribution of beliefs over the health states. The health monitoring methodology is demonstrated on the K11 rover. A hybrid model of the K11 is proposed and experimental results show that the approach is robust to real system data and constraints.
Quentin Gaudel, Pauline Ribot, Elodie Chanthery, Matthew J. Daigle

Conformance Checking

Frontmatter

Merging Alignments for Decomposed Replay

Abstract
In the area of process mining, conformance checking aims to find an optimal alignment between an event log (which captures the activities that actually have happened) and a Petri net (which describes expected or normative behavior). Optimal alignments highlight discrepancies between observed and modeled behavior. To find an optimal alignment, a potentially challenging optimization problem needs to be solved based on a predefined cost function for misalignments. Unfortunately, this may be very time consuming for larger logs and models and often intractable. A solution is to decompose the problem of finding an optimal alignment in many smaller problems that are easier to solve. Decomposition can be used to detect conformance problems in less time and provides a lower bound for the costs of an optimal alignment. Although the existing approach is able to decide whether a trace fits or not, it does not provide an overall alignment. In this paper, we provide an algorithm that is able to provide such an optimal alignment from the decomposed alignments if this is possible. Otherwise, the algorithm produces a so-called pseudo-alignment that can still be used to pinpoint non-conforming parts of log and model. The approach has been implemented in ProM and tested on various real-life event logs.
H. M. W. Verbeek, W. M. P. van der Aalst

Anti-alignments in Conformance Checking – The Dark Side of Process Models

Abstract
Conformance checking techniques asses the suitability of a process model in representing an underlying process, observed through a collection of real executions. These techniques suffer from the well-known state space explosion problem, hence handling process models exhibiting large or even infinite state spaces remains a challenge. One important metric in conformance checking is to asses the precision of the model with respect to the observed executions, i.e., characterize the ability of the model to produce behavior unrelated to the one observed. By avoiding the computation of the full state space of a model, current techniques only provide estimations of the precision metric, which in some situations tend to be very optimistic, thus hiding real problems a process model may have. In this paper we present the notion of anti-alignment as a concept to help unveiling traces in the model that may deviate significantly from the observed behavior. Using anti-alignments, current estimations can be improved, e.g., in precision checking. We show how to express the problem of finding anti-alignments as the satisfiability of a Boolean formula, and provide a tool which can deal with large models efficiently.
Thomas Chatain, Josep Carmona

Time and Stochastic Models

Frontmatter

Probabilistic Time Petri Nets

Abstract
We introduce a new model for the design of concurrent stochastic real-time systems. Probabilistic time Petri nets (PTPN) are an extension of time Petri nets in which the output of tokens is randomised. Such a design allows us to elegantly solve the hard problem of combining probabilities and concurrency. This model further benefits from the concision and expressive power of Petri nets. Furthermore, the usual tools for the analysis of time Petri nets can easily be adapted to our probabilistic setting. More precisely, we show how a Markov decision process (MDP) can be derived from the classic atomic state class graph construction. We then establish that the schedulers of the PTPN and the adversaries of the MDP induce the same Markov chains. As a result, this construction notably preserves the lower and upper bounds on the probability of reaching a given target marking. We also prove that the simpler original state class graph construction cannot be adapted in a similar manner for this purpose.
Yrvann Emzivat, Benoît Delahaye, Didier Lime, Olivier H. Roux

Efficient Decomposition Algorithm for Stationary Analysis of Complex Stochastic Petri Net Models

Abstract
Stochastic Petri nets are widely used for the modeling and analysis of non-functional properties of critical systems. The state space explosion problem often inhibits the numerical analysis of such models. Symbolic techniques exist to explore the discrete behavior of even complex models, while block Kronecker decomposition provides memory-efficient representation of the stochastic behavior. However, the combination of these techniques into a stochastic analysis approach is not straightforward. In this paper we integrate saturation-based symbolic techniques and decomposition-based stochastic analysis methods. Saturation-based exploration is used to build the state space representation and a new algorithm is introduced to efficiently build block Kronecker matrix representation to be used by the stochastic analysis algorithms. Measurements confirm that the presented combination of the two representations can expand the limits of previous approaches.
Kristóf Marussy, Attila Klenik, Vince Molnár, András Vörös, István Majzik, Miklós Telek

Decidable Classes of Unbounded Petri Nets with Time and Urgency

Abstract
Adding real time information to Petri net models often leads to undecidability of classical verification problems such as reachability and boundedness. For instance, models such as Timed-Transition Petri nets (TPNs) [22] are intractable except in a bounded setting. On the other hand, the model of Timed-Arc Petri nets [26] enjoys decidability results for boundedness and control-state reachability problems at the cost of disallowing urgency (the ability to enforce actions within a time delay). Our goal is to investigate decidable classes of Petri nets with time that capture some urgency and still allow unbounded behaviors, which go beyond finite state systems.
We present, up to our knowledge, the first decidability results on reachability and boundedness for Petri net variants that combine unbounded places, time, and urgency. For this, we introduce the class of Timed-Arc Petri nets with restricted Urgency, where urgency can be used only on transitions consuming tokens from bounded places. We show that control-state reachability and boundedness are decidable for this new class, by extending results from Timed-Arc Petri nets (without urgency) [2]. Our main result concerns (marking) reachability, which is undecidable for both TPNs (because of unrestricted urgency) [20] and Timed-Arc Petri Nets (because of infinite number of “clocks”) [25]. We obtain decidability of reachability for unbounded TPNs with restricted urgency under a new, yet natural, timed-arc semantics presenting them as Timed-Arc Petri Nets with restricted urgency. Decidability of reachability under the intermediate marking semantics is also obtained for a restricted subclass.
S. Akshay, B. Genest, L. Hélouët

Structural Methods

Frontmatter

Structural Place Invariants for Analyzing the Behavioral Properties of Nested Petri Nets

Abstract
Nested Petri nets (NP-nets) is an extension of the Petri nets formalism within the “nets-within-nets” approach. Due to tokens with individual behavior and the mechanism of synchronization NP-nets are convenient for modeling multi-agent and adaptive systems, flexible workflow nets, and other systems with mobile interacting components and dynamic structure.
In contrast to classical Petri nets, there is still a lack of analysis methods for NP-nets. In this paper we show, that the classical Petri nets analysis technique based on place invariants can be extended to NP-nets. This paper defines place invariants of NP-nets, which link several NP-net components and allow to prove crucial behavioral properties directly from the NP-net structure. An algorithm for computing NP-net invariants is presented and illustrated with an example of EJB system verification.
Leonid W. Dworzanski, Irina A. Lomazova

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise