Preface -- 1 First Steps in Petri Nets -- 2 Languages of Petri Nets -- 3 Reachability and Coverability -- 4 Linear-algebraic Structure of Petri Nets -- 5 Graph-theoretical Structure of Petri Nets -- 6 More Structure Theory -- 7 Program Verification Using Traps -- 8 Fairness, Simulations, and Inhibitor Arcs -- 9 Unfoldings and Reachability Checking -- 10 Petri Net Computers -- 11 Synthesis of Petri Nets from Labelled Transition Systems -- 12 Persistent Transition Systems and Choice-free Petri Nets -- 13 Divide-and-Conquer Methods for Synthesis -- 14 Marked Graph Synthesis -- 15 Bounded Choice-free Net Synthesis -- 16 Model Checking Safe, Strongly Persistent Petri Nets -- 17 Semilinearity -- 18 Decidability of the reachability problem -- 19 The Box Algebra 1/2: Refinement and Recursion -- 20 The Box Algebra 2/2: Iteration and Data -- 21 High-level Petri Nets -- Biblyography -- Index.
Petri nets model concurrent and distributed systems where active components communicate through the production and absorption of various kinds of resources. Although the dynamic properties of such systems may be very complex, they may sometimes be connected to the static structure of a Petri net. Many properties are decidable, but their complexity may be huge. It is often opportune to restrict oneself to classes of systems, to partial algorithms, and to similar but simpler properties. Instead of analysing a given system, it is also possible to search for a system satisfying some desired properties by construction. This comprehensive textbook/reference presents and discusses these issues in-depth in the context of one of the most fundamental Petri net models, called place/transition nets. The presentation is fortified by means of many examples and worked exercises. Among topics addressed: • In which order may actions may be generated and scheduled? • What states and configurations may be reached in a concurrent system? • Which interesting classes of systems can be analysed relatively efficiently? • Is it possible to synthesise a system of some class from its behaviour? • How can systems be represented algebraically, compositionally, and concisely? This unique text, based on introductory as well as on advanced courses on distributed systems, will serve as an invaluable guide for students and (future) researchers interested in theoretical—as well as in practical—aspects of Petri nets and related system models. Eike Best has been a full professor (now retired) affiliated to Carl von Ossietzky Universität Oldenburg, Germany. Raymond Devillers has been a full professor (now retired) affiliated to Université Libre de Bruxelles, Belgium. The authors have a long record as collaborators in the fields of Petri nets and the semantics of concurrency.
Application and Theory of Petri Nets and Concurrency 1st ed. 2020. Cham : Springer International Publishing, 2020 (2020), Seite 89-108 1 Online-Ressource(XI, 437 p. 491 illus., 49 illus. in color.)
Das Problem der Petrinetzsynthese wurde schon weit untersucht und passt in viele Kontexte. Gleichzeitig scheint die Frage nach einer Charakterisierung von synthetisierbaren Zustandsräumen weniger entwickelt zu sein. Die vorliegende Arbeit ist ein Versuch ein besseres Verständnis von letzterem zu erlangen, während ersteres als Hauptziel im Auge behalten wird. Zu den Hauptresultaten der Arbeit gehört eine Graph-theoretische Charakterisierung von synthetisierbaren linearen Transitionssystemen und Kreisen. Auf dieser Charakterisierung basierende Synthesealgorithmen zeigen eine bessere Laufzeit im Vergleich zur Regionen-basierten Synthese. Eine Charakterisierung der Klasse aller minimal-unlösbaren Wörter wird in Form eines erweiterten regulären Ausdrucks vorgeschlagen. Die Zustandsräume von Petrinetzen über der binären Transitionsmenge erwiesen sich als geometrisch konvexe Hüllen. Ein Algorithmus zur Überapproximation einer endlichen Sprache durch eine Petrinetzsprache wird dargestellt. <dt.>
The problem of Petri net synthesis is widely studied in the literature, set in a range of contexts, while the question for characterisation of synthesisable state spaces seems to be less investigated and developed. The current work is an attempt to put more insight into the latter, keeping in mind the former as the main goal. Among the main results of the work, a graph-theoretical characterisation of synthesisable linear transition systems and cycles is presented. Synthesis algorithms, based on the characterisation, demonstrate a better runtime in comparison to the region based synthesis. For the class of minimal unsolvable binary sequences, a characterisation is suggested in the form of extended regular expressions. The state spaces of Petri nets over the binary transition set are proven to be geometrically convex hulls. An algorithm for over-approximating a finite language by a Petri net language is presented. <engl.>
Bei der Petrinetz-Synthese soll ein gegebenes endliches beschriftetes Transitionssystem (labelled transition system; LTS) durch ein injektiv beschriftetes Petrinetz gelöst werden, was bedeutet, dass der Erreichbarkeitsgraph des Petrinetzes isomorph zum gegebenen LTS ist. Petrinetz-Synthese fing mit den Arbeiten von Ehrenfeucht und Rozenberg im Jahr 1990 an und wurde seitdem in verschiedene Richtungen erweitert. In dieser Arbeit wird die Synthese von Petrinetz-Teilklassen untersucht, beispielsweise schlichte und schlingenfreie Petrinetze. Unlösbare LTS werden durch Überapproximation behandelt. Als nächstes wird die Synthese von modalen Transitionssystemen (MTS), dem modalem μ-Kalkül und einer Teilmenge des μ-Kalküls, die konjunktiver ν-Kalkül heißt, behandelt. Das Synthese-Problem für MTS und den ν-Kalkül ist unentscheidbar, aber durch eine Einschränkung der betrachteten Petrinetze wird dieses Problem sogar für den ausdruckmächtigeren μ-Kalküls entscheidbar.
In Petri net synthesis, a given finite labelled transition system (lts) should be solved by an injectively labelled Petri net, which means that the reachability graph of the Petri net is isomorphic to the given lts. Petri net synthesis goes back to the work of Ehrenfeucht and Rozenberg in 1990, and has since then been extended in various directions.In this thesis, synthesis for subclasses of Petri nets is investigated, e.g. plain and pure nets. Unsolvable lts are handled by over-approximation. Next, synthesis from modal transition systems (mts), the modal μ-calculus, and a subset of the μ-calculus, which is called the conjunctive ν-calculus, is considered. We show that that the synthesis problem for mts and the ν-calculus is undecidable, but by restricting the Petri nets considered, the synthesis problem becomes decidable even for the more expressive μ-calculus.
This book constitutes the proceedings of the 38th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2017, held in Zaragoza, Spain, in June 2017. Petri Nets 2017 is co-located with the Application of Concurrency to System Design Conference, ACSD 2017. The 16 papers, 9 theory papers, 4 application papers, and 3 tool papers, with 1 short abstract and 3 extended abstracts of invited talks presented together in this volume were carefully reviewed and selected from 33 submissions. The focus of the conference is on following topics: Simulation of Colored Petri Nets, Petri Net Tools.- Model Checking, Liveness and Opacity, Stochastic Petri Nets, Specific Net Classes, and Petri Nets for Pathways
Distinguished Carl Adam Petri Lecture -- Simulation of Colored Petri Nets -- Petri Net Tools -- Model Checking -- Liveness and Opacity -- Stochastic Petri Nets -- Specific Net Classes -- Petri Nets for Pathways
Lecture Notes in Computer ScienceSpringerLinkSpringer eBook Collection
