Petri Net Synthesis | springerprofessional.de

Springer Professional

nach oben

2015 | Buch

Kapitel lesen Erstes Kapitel lesen

Petri Net Synthesis

verfasst von: Eric Badouel, Luca Bernardinello, Philippe Darondeau

Verlag: Springer Berlin Heidelberg

Buchreihe : Texts in Theoretical Computer Science. An EATCS Series

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book is a comprehensive, systematic survey of the synthesis problem, and of region theory which underlies its solution, covering the related theory, algorithms, and applications. The authors focus on safe Petri nets and place/transition nets (P/T-nets), treating synthesis as an automated process which, given behavioural specifications or partial specifications of a system to be realized, decides whether the specifications are feasible, and then produces a Petri net realizing them exactly, or if this is not possible produces a Petri net realizing an optimal approximation of the specifications.

In Part I the authors introduce elementary net synthesis. In Part II they explain variations of elementary net synthesis and the unified theory of net synthesis. The first three chapters of Part III address the linear algebraic structure of regions, synthesis of P/T-nets from finite initialized transition systems, and the synthesis of unbounded P/T-nets. Finally, the last chapter in Part III and the chapters in Part IV cover more advanced topics and applications: P/T-net with the step firing rule, extracting concurrency from transition systems, process discovery, supervisory control, and the design of speed-independent circuits.

Most chapters conclude with exercises, and the book is a valuable reference for both graduate students of computer science and electrical engineering and researchers and engineers in this domain.

Anzeige

Inhaltsverzeichnis

Frontmatter

0. Introduction

Abstract

Petri nets are a well-established model of concurrent systems, with a rich and strong, yet still growing, theory. Petri nets are intensively used in the design, verification, analysis, and prototyping of software systems, control systems and hardware systems. Different dialects or extensions of Petri nets serve in the different fields, e.g. safe Petri nets for hardware design, place/transition nets and high-level nets for software design, timed and stochastic Petri nets for performance evaluation.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

Elementary Net Synthesis

Frontmatter

1. Introduction to Elementary Net Synthesis

Abstract

This chapter aims at giving, for the particular class of elementary net systems, a first account of the principles of region-based net synthesis. The next section introduces elementary nets in an informal way. Section 1.2 recalls the corresponding formal definitions needed in this book. Section 1.3 presents the construction of the saturated net version of a transition system, as proposed by Ehrenfeucht and Rozenberg, while Section 1.4 recalls their characterization of net realizable transition systems by the regional axioms. Sections 1.5 and 1.6 focus on admissible sets of regions, namely sets of regions which are sufficient to solve the synthesis problem. The interest is to reduce significantly the search space for admissible sets of regions, which has a direct impact on the efficiency of net synthesis algorithms. Section 1.7 explores the relation between regional partitions of a transition system and sequential components of elementary net systems. We finally explain in Section 1.8 the context of Labelled Partial 2-Structures in which regions were discovered and first applied to elementary net synthesis. The chapter is completed by a series of exercises.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

2. Other Forms of the Synthesis Problem

Abstract

The canonical form of the synthesis problem asks for exact realizations of transition systems. In this chapter we study some variations on that theme. In one case, we relax the constraint that the reachability graph of the synthesized net be isomorphic to the initial transition system, and allow it to be a quotient.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

3. Algorithms of Elementary Net Synthesis

Abstract

In this chapter, we consider finite transition systems exclusively. The chapter contains two sections. The first section shows that the net synthesis problem is NP-complete, hence one cannot construct very efficient synthesis algorithms. The second section constructs a flexible algorithm, based on minimal regions, that can be tailored to all forms of the net synthesis problem by selecting the relevant separation axioms. Most developments presented in the chapter, in spite of the title, are independent of elementary nets and valid in the larger framework of quasi-elementary nets. By nets and net systems, to restate the convention adopted in Chapter 1, we always mean quasi-elementary nets and quasi-elementary net systems, thus elementary is never meant unless it is explicit.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

Types of Nets

Frontmatter

4. Variations of Elementary Net Synthesis

Abstract

Many variations of the notion of regions in transition systems, introduced by Ehrenfeucht and Rozenberg in the context of Elementary Net Systems, were proposed later in order to synthesize other classes of net systems and to establish corresponding representation theorems for initialized transition systems. Many striking similarities appear in the technical developments of those similar studies. The goal of this chapter is to provide a uniform theory of net system synthesis based on regions, such that all the considered variations may be retrieved as specific instantiations of this general scheme. In the uniform theory, each class of nets comes equipped with a deterministic transition system t, called a type of nets, which induces a net firing rule and hence captures the dynamic evolution of all nets in the class. The type of nets describes the behaviour of an archetypical (atomic) net of the considered class. We can then use the type of nets as a parameter to define the notions of t-nets (and t-net systems) and their marking (and reachability) graphs. The t-regions of an initialized transition system A are the morphisms from A into t; they define the places of the t-net synthesized from A. In the last section of the chapter, we pay specific attention to the types of Boolean nets, where markings are sets of places.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

5. A Unified Theory of Net Synthesis

Abstract

Since the purpose of net synthesis is to construct a finite net system we shall consider a fixed finite set \( E = \left\{ {e_1, \ldots e_n } \right\} \) of events even though all the results presented in this chapter extend without modifications to the case where E is an infinite set.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

P/T-Net Synthesis

Frontmatter

6. The Linear Algebraic Structure of Regions

Abstract

In the third part of this book, we specialize the theory of net synthesis to the type of P/T-nets and show that the specialized theory is effective. For this purpose, we shall essentially use basic linear algebra. In particular, we shall characterize the P/T-regions of an initialized transition system (or a language) by a linear system, and we shall reduce the separation problems to linear problems.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

7. Synthesis of P/T-Nets from Finite Initialized Transition Systems

Abstract

In this chapter, \( A = \left( {S,\,E,\,\Delta,\,s_0 } \right) \) is a finite initialized transition system, reachable and reduced, with set of events \( E = \left\{ {e_1, \ldots e_n } \right\} \). Since the transition relation \( \Delta \subseteq S \times E \times S \) is deterministic it can equivalently be given as a partial map \( \delta :S \times E \to S \) with \( \delta \left( {s,\,e} \right) = s^{\prime} \Leftrightarrow \left( {s,\,e,\,s^{\prime}} \right) \in \Delta \).

Eric Badouel, Luca Bernardinello, Philippe Darondeau

8. Synthesis of Unbounded P/T-Nets

Abstract

In this chapter, \( A = \left( {S,\,E,\,\Delta ,\,s_0 } \right) \) is a possibly infinite initialized transition system, reachable and reduced, and \( E = \left\{ {e_1 , \ldots ,\,e_n } \right\} \). A particular case is when A = L represents an infinite prefix-closed language \( L \subseteq E^* ,\,i.e.\,S = L,\,s_0 = \varepsilon \), and for every \( u \in E^* \) and \( e \in E,\,\delta \left( {u,\,e} \right) \) is defined and equal to ue if and only if \( ue \in L \).

Eric Badouel, Luca Bernardinello, Philippe Darondeau

9. P/T-Nets with the Step Firing Rule

Abstract

In this chapter, P/T-nets are given a concurrent semantics by replacing the usual firing rule with the step firing rule, which allows steps M[e>M’ where e is a multiset of transitions. Concurrent reachability graphs of P/T-nets are a particular case of Mukund’s step transition systems. After reformulating Mukund’s definition of regions in step transition systems, we examine the P/T-net realization problem for step transition systems and for step languages. As an aside, we present two extended forms of the P/T-net realization problem for step transition systems, and an alternative form of the P/T-net realization problem for partially ordered languages.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

Applications of Net Synthesis

Frontmatter

10. Extracting Concurrency from Transition Systems

Abstract

In this chapter, we show that P/T-net synthesis may serve not only to obtain compact representations of initialized transition systems—by making explicit the concurrency of some events—but also to obtain distributed implementations thereof.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

11. Process Discovery

Abstract

One of the purposes of process mining [1] is model discovery, i.e. the ability to construct or reconstruct from an event log a business process model that can generate this event log. The game is to dig out of event logs sufficient information on the structure of their generating model. As a technique for model discovery or model identification, process mining has some connections with machine learning. For instance, after collecting over a long period of time information on the health history of many patients, including diagnosis and treatment steps, one may want to extract from this record an accurate model of the workflow system of a hospital. Another type of application is to try to reconstruct from representative use cases an existing but partially unknown system.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

12. Supervisory Control

Abstract

In this chapter, we present some applications of regions to supervisory control proposed in the literature. First, we give a concise introduction to Ramadge and Wonham’s foundational theory of supervisory control for Discrete Event Systems, which covers both finite transition systems and regular languages (Section 12.1). Second, we present the linear-algebraic techniques classically used for the monitor-based supervision of Petri nets (Section 12.2). Regionbased supervision of Petri nets, which extends their monitor-based supervision, is studied in Section 12.3. Region-based supervisory control is extended to discrete event systems in Section 12.4. The application of regions to the distributed control of discrete event systems, which we feel is a promising direction for research, is hinted at in the final Section 12.5.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

13. Design of Speed Independent Circuits

Abstract

In this chapter, we present applications of regions and elementary (or quasielementary) net synthesis for the design of speed independent circuits. Asynchronous circuit design is a wide and complex field that encompasses other topics than Petri nets. We refer the reader to the book [46] for a complete presentation of this field. We will limit ourselves to assessing the roles played by regions and net synthesis for solving the Complete State Coding problem (CSC). This crucial problem motivated the implementation of a net synthesis procedure in Petrify, a general design tool for asynchronous circuits presented in [46]. It must be acknowledged that different methods based on net unfoldings and SAT solvers are now preferred over net synthesis for solving the CSC problem.

Eric Badouel, Luca Bernardinello, Philippe Darondeau

Backmatter

Titel: Petri Net Synthesis
verfasst von: Eric Badouel
Luca Bernardinello
Philippe Darondeau
Copyright-Jahr: 2015
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-662-47967-4
Print ISBN: 978-3-662-47966-7
DOI: https://doi.org/10.1007/978-3-662-47967-4

Weitere Formate
Fachgebiete
Bücher
Zeitschriften
Themenseiten
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024