Target-oriented Petri Net Synthesis

• Autorzy: Best Eike , Devillers Raymond , Erofeev Evgeny , Wimmel Harro

Identyfikatory

DOI

10.3233/FI-2020-1949

• Języki publikacji: EN

Abstrakty

EN

When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors’ and their groups’ work over the past few years.

Słowa kluczowe

EN

choice-freeness; persistence; Petri nets; synthesis

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 175, nr 1-4
• Strony: 97--122
• Opis fizyczny: Bibliogr. 52 poz., rys.

Twórcy

autor

Best Eike

• Parallel Systems, Department of Computing Science, Carl von Ossietzky Universität Oldenburg, D-26111 Oldenburg, Germany

autor

Devillers Raymond

• Département d'Informatique, Université Libre de Bruxelles, Boulevard du Triomphe, C.P. 212, B-1050 Bruxelles, Belgium

autor

Erofeev Evgeny

• Parallel Systems, Department of Computing Science, Carl von Ossietzky Universität Oldenburg, D-26111 Oldenburg, Germany

autor

Wimmel Harro

• Parallel Systems, Department of Computing Science, Carl von Ossietzky Universität Oldenburg, D-26111 Oldenburg, Germany

Bibliografia

• [1] Badouel E, Bernardinello L, Darondeau P. Polynomial Algorithms for the Synthesis of Bounded Nets. In: Proc. TAPSOFT’95, P.D. Mosses, M. Nielsen, M.I. Schwartzbach (eds). vol. 915 Lecture Notes in Computer Science 1995 pp. 364-378. doi:10.1007/3-540-59293-8_207.
• [2] Badouel E, Bernardinello L, Darondeau P. Petri Net Synthesis. Texts in Theoretical Computer Science, Springer, 2015 pp. 339. ISBN:978-3-662-47967-4.
• [3] Ehrenfeucht A, Rozenberg G. Partial 2-structures, Part I: Basic Notions and the Representation Problem, and Part II: State Spaces of Concurrent Systems. Acta Informatica 1990. 27(4):315-368.
• [4] Kleijn J, Koutny M, Pietkiewicz-Koutny M, Rozenberg G. Applying Regions. Theoretical Computer Science 2017. 658:205-215. doi:10.1016/j.tcs.2016.01.040.
• [5] Reisig W. Petri Nets. EATCS Monographs on Theoretical Computer Science 4. Springer-Verlag 1985.
• [6] Cortadella J, Kishinevsky M, Kondratyev A, Lavagno L, Yakovlev A. Logic Synthesis for Asynchronous Controllers and Interfaces. Springer-Verlag Berlin Heidelberg, Advanced Microelectronics. 2002. ISBN:978-3-540-43152-7. doi:10.1007/978-3-642-55989-1.
• [7] Carmona J, Cortadella J, Khomenko V, Yakovlev A. Synthesis of Asynchronous Hardware from Petri Nets. In: Lectures on Concurrency and Petri Nets, J. Desel, W. Reisig, G. Rozenberg (eds). Advances in Petri Nets, vol. 3098. Lecture Notes in Computer Science. 2004 pp. 345-401. doi:10.1007/978-3-540-27755-2_9.
• [8] Lavagno L, Moon CW, Brayton RK, Sangiovanni-Vincentelli A. A Novel Framework for Solving the State Assignment Problem for Event-Based Specifications. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 02, 1992/1995 pp. 24.
• [9] Badouel E, Caillaud B, Darondeau P. Distributing Finite Automata through Petri Net Synthesis. Journal on Formal Aspects of Computing 2002.13:447-470. doi:10.1007/s001650200022.
• [10] Schlachter U. Petri Net Synthesis for Restricted Classes of Nets. In: Application and Theory of Petri Nets and Concurrency 2016, F. Kordon, D. Moldt (eds). vol. 9698 Lecture Notes in Computer Science. 2016 pp. 79-97. doi:10.1007/978-3-319-39086-4_6.
• [11] Best E, Darondeau P. A Decomposition Theorem for Finite Persistent Transition Systems. Acta Informatica 2009. 46:237-254. doi:10.1007/s00236-009-0095-6.
• [12] Best E, Devillers R. Synthesis of Persistent Systems. In: Application and Theory of Petri Nets and Concurrency 2014, G. Ciardo, E. Kindler (eds). vol. 8489 Lecture Notes in Computer Science 2014 pp. 111-129. doi:10.1007/978-3-319-07734-5_7.
• [13] Best E, Devillers R. Synthesis and Reengineering of Persistent Systems. In: Special volume on the occasion of the 25’th anniversary of Combining Compositionality and Concurrency workshops, R. van Glabbeek, U. Goltz, E.-R. Olderog (eds). Acta Informatica 2015. 52(1):35-60.
• [14] Best E, Devillers R, Schlachter U. Bounded choice-free Petri net synthesis: algorithmic issues. Acta Informatica 2018. 55(7):575-611. doi:10.1007/s00236-017-0310-9.
• [15] Wimmel H. Presynthesis of Bounded Choice-Free or Fork-Attribution Nets. Information and Computation, 2019. doi:10.1016/j.ic.2019.104482.
• [16] Badouel E, Bernardinello L, Darondeau P. The Synthesis Problem for Elementary Net Systems is NP-Complete. Theoretical Computer Science 1997. 186(1-2):107-134. doi:10.1016/S0304-3975(96)00219-8.
• [17] Best E, Devillers R, Schlachter U. A Graph-Theoretical Characterisation of State Separation. SOFSEM 2017, vol. 10139 Lecture Notes in Computer Science 2017 pp. 163-175. doi:10.1007/978-3-319-51963-0_13.
• [18] Schlachter U, Wimmel H. A Geometric Characterisation of Event/State Separation. In: Application and Theory of Petri Nets and Concurrency 2018, V. Khomenko, O.H. Roux (eds). vol. 10877 Lecture Notes in Computer Science 2018 pp. 99-116. doi:10.1007/978-3-319-91268-4_6.
• [19] U. Schlachter et al.: APT: Analysis of Petri nets and Transition systems, https://github.com/CvO-Theory/apt.
• [20] Christ J, Hoenicke J, Nutz A. Proof Tree Preserving Interpolation. Proc. TACAS 2013, N. Piterman, S.A. Smolka (eds). vol. 7795 Lecture Notes in Computer Science 2013 pp. 124-138. doi:10.1007/978-3-642-36742-7_9.
• [21] Karmarkar N. A new polynomial-time algorithm for linear programming. Combinatorica 4, Springer 1984 pp. 373-395. doi:10.1007/BF02579150.
• [22] Schlachter U. Petri Net Synthesis and Modal Specifications. PhD Thesis, Carl von Ossietzky Universität Oldenburg 2018.
• [23] Erofeev E. Characterisation of a Class of Petri Net Solvable Transition Systems. PhD Thesis, Carl von Ossietzky Universität Oldenburg 2018.
• [24] de Berg M, van Kreveld M, Overmars M, Schwarzkopf o. Computational Geometry: Algorithms and Applications. Springer, 2000. ISBN:978-3-662-04245-8.
• [25] Teruel E, Colom JM, Silva M. Choice-Free Petri Nets: a model for deterministic concurrent systems with bulk services and arrivals. IEEE Transactions on Systems, Man and Cybernetics (Part A), 1997. 27(1):73-83. doi:10.1109/3468.553226.
• [26] Landweber LH, Robertson EL. Properties of Conflict-Free and Persistent Petri Nets. JACM 1978. 25(3):352-364. doi:10.1145/322077.322079.
• [27] Devillers R. Articulation of Transition Systems and Its Application to Petri Net Synthesis. In: Application and Theory of Petri Nets and Concurrency 2019, S. Donatelli, S. Haar (eds). vol. 11522 Lecture Notes in Computer Science, 2019 pp. 113-129. doi:10.1007/978-3-030-21571-2_8.
• [28] Devillers R, Schlachter U. Factorisation of Petri Net Solvable Transition Systems. In: Application and Theory of Petri Nets and Concurrency 2018, V. Khomenko, O.H. Roux (eds). vol. 10877 Lecture Notes in Computer Science, 2018 pp. 82-98.
• [29] Best E, Devillers R. Pre-synthesis of Petri nets based on prime cycles and distance paths. Sci. Comput. Program. 2018. 157:41-55. doi:10.1016/j.scico.2017.07.005.
• [30] Commoner F, Holt AW, Even S, Pnueli A. Marked Directed Graphs. J. Comput. Syst. Sci. 1971. 5(5):511-523. doi:10.1016/S0022-0000(71)80013-2.
• [31] Genrich HJ, Lautenbach K. Synchronisationsgraphen. Acta Informatica 1973. 2:143-161.
• [32] Best E, Devillers R. Characterisation of the state spaces of marked graph Petri nets. Information and Computation 2017. 253(3):399-410. doi:10.1016/j.ic.2016.06.006.
• [33] Best E, Devillers R. State Space Axioms for T-Systems. In: Special volume on the occasion of Walter Vogler’s 60th birthday, G. Lüttgen, F. Corradini (eds). Acta Informatica 2015. 52(2-3):133-152. doi:10.1007/s00236-015-0219-0.
• [34] Barylska K, Best E, Erofeev E, Mikulski Ł, Piątkowski P. Conditions for Petri Net Solvable Binary Words. In: Transactions on Petri Nets and Other Models of Concurrency XI, M. Koutny, J. Desel, J. Kleijn (eds). vol. 9930 Lecture Notes in Computer Science 2016 pp. 137-159.
• [35] Best E, Erofeev E, Schlachter U, Wimmel H. Characterising Petri Net Solvable Binary Words. In: Application and Theory of Petri Nets and Concurrency 2016, F. Kordon, D. Moldt (eds). vol. 9698 Lecture Notes in Computer Science, 2016 pp. 39-58.
• [36] Erofeev E, Barylska K, Mikulski Ł, Piątkowski M. Generating All Minimal Petri Net Unsolvable Binary Words. Discrete Applied Mathematics, 2020. 274:35-53.
• [37] Erofeev E, Wimmel H. Reachability Graphs of Two-Transition Petri Nets. ATAED@Petri Nets/ACSD 2017 pp. 39-54. http://ceur-ws.org/Vol-1847/paper03.pdf.
• [38] de Frutos Escrig D, Koutny M, Mikulski Ł. An Efficient Characterization of Petri Net Solvable Binary Words. In: Application and Theory of Petri Nets and Concurrency 2018, V. Khomenko, O.H. Roux (eds). vol. 10877 Lecture Notes in Computer Science, 2018 pp. 207-226.
• [39] Teruel E, Chrząstowski-Wachtel P, Colom J, Silva M. On Weighted T-systems. Application and Theory of Petri Nets, vol. 616 Lecture Notes in Computer Science, 1992 pp. 348-367.
• [40] Devillers R, Erofeev E, Hujsa T. Synthesis of Weighted Marked Graphs from Circular Labelled Transition Systems. ATAED@Petri Nets/ACSD, 2019 pp. 6-22. URL http://ceur-ws.org/Vol-2371/ATAED2019-6-22.pdf.
• [41] Devillers R, Hujsa T. Analysis and Synthesis of Weighted Marked Graph Petri Nets. In: Application and Theory of Petri Nets and Concurrency 2018, V. Khomenko, O.H. Roux (eds). vol. 10877 Lecture Notes in Computer Science, 2018 pp. 19-39. doi:10.1007/978-3-319-91268-4_2.
• [42] Devillers R, Hujsa T. Analysis and Synthesis of Weighted Marked Graph Petri Nets: Exact and Approximate Methods. Fundamenta Informaticae 2019. 169(1-2):1-30. doi:10.3233/FI-2019-1837.
• [43] Desel J, Esparza J. Free Choice Petri Nets. vol. 40 1995. Cambridge University Press. ISBN: 978-0-521-46519-9.
• [44] Schlachter U, Spreckels V. Synthesis of Labelled Transition Systems into Equal-Conflict Petri Nets. ATAED@Petri Nets/ACSD, 2017 pp. 122-130. URL http://ceur-ws.org/Vol-1847/paper09.pdf.
• [45] Wimmel H. Synthesis of asymmetric choice Petri nets. 2019 p. 27. arXiv:1911.09133 [cs.FL].
• [46] E. Best, R. Devillers, U. Schlachter, H. Wimmel: Simultaneous Petri Net Synthesis. Sci. Ann. Comp. Sci. 2018. 28(2):199-236. doi:10.7561/SACS.2018.2.199.
• [47] Carmona J. The Label Splitting Problem. In: Transactions on Petri Nets and Other Models of Concurrency VI, K. Jensen, W.M.v.d. Aalst, M. Ajmone-Marsan, G. Franceschinis, J. Kleijn, L.M. Kristensen (eds), vol. 7400 Lecture Notes in Computer Science, 2012 pp. 1-23. doi:10.1007/978-3-642-35179-2_1.
• [48] Carmona J, Cortadella J, Kishinevsky M, Kondratyev A, Lavagno L, Yakovlev A. A Symbolic Algorithm for the Synthesis of Bounded Petri Nets. In: Applications and Theory of Petri Nets 2008, K. van Hee, R. Valk (eds). vol. 5062 Lecture Notes in Computer Science, 2008 pp. 92-111. doi:10.1007/978-3-540-68746-7_10.
• [49] Schlachter U, Wimmel H. Optimal Label Splitting for Embedding an LTS into an arbitrary Petri Net Reachability Graph is NP-complete. 2020 p. 18. arXiv:2002.04841 [cs.CC].
• [50] Schlachter U, Wimmel H. Relabeling LTS for Petri Net Synthesis via Solving Separation Problems. In: Transactions on Petri Nets and Other Models of Concurrency XIV, M. Koutny, L. Pomello, L.M. Kristensen (eds). vol. 11790 Lecture Notes in Computer Science, 2019 pp. 222-254. doi:10.1007/978-3-662-60651-3_9.
• [51] K. Barylska, E. Best, U. Schlachter, V. Spreckels: Properties of Plain, Pure, and Safe Petri Nets. In: Transactions on Petri Nets and Other Models of Concurrency XII, M. Koutny, J. Kleijn, W. Penczek, M. Zhang (eds). Lecture Notes in Computer Science 10470, 1-18 (2017).
• [52] Esparza J. Decidability and Complexity of Petri Net Problems - An Introduction. Proc. Advanced Course on Petri Nets, Dagstuhl, W. Reisig, G. Rozenberg (eds), vol. 1491 LNCS, Springer-Verlag, 1996 pp. 374-428. doi:10.1007/3-540-65306-6_20.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).