Published in Volume XXVIII, Issue 2, 2018, pages 199–236, doi: 10.7561/SACS.2018.2.199
Authors: E. Best, R. Devillers, U. Schlachter, H. Wimmel
Abstract
Petri net synthesis deals with the problem whether, given a labelled transition system TS, one can find a Petri net N with an initial marking M0 such that the reachability graph of (N. M0) is isomorphic to TS. This may be preceded by a pre-synthesis phase that will quickly reject ill-formed transition systems (and give structural reasons for the failure) and otherwise build data structures needed by the proper synthesis. The last phase proceeds by solving systems of linear inequalities, and may still fail but for less transparent reasons. In this paper, we consider an extended problem. A finite set of transition systems {TS1, …,TSm} shall be called simultaneously Petri net solvable if there is a single Petri net N with several initial markings {M01,…,M0m}, such that for every i = 1,…,m, the reachability graph of (N, M0i) is isomorphic to TSi. The focus will be on choice-free nets, that is, nets without structural choices, and we explore how previously published efficient algorithms for the pre-synthesis and proper synthesis of bounded and choice-free Petri nets can be generalised for the simultaneous pre-synthesis and synthesis of such multi-marked nets. At the same time, the choice-free pre-synthesis of a single transition system shall be strengthened by introducing new structural checks.
Full Text (PDF)References
[1] É. Badouel, L. Bernardinello, P. Darondeau: Petri Net Synthesis. Texts in Theoretical Computer Science, Springer-Verlag, ISBN 978-3-662- 47967-4, 339 pages (2015). doi:10.1007/978-3-662-47967-4.
[2] E. Best, P. Darondeau: A Decomposition Theorem for Finite Persistent Transition Systems. Acta Informatica 46: 237–254 (2009). doi:10.1007/ s00236-009-0095-6.
[3] E. Best, R. Devillers: Petri Net Pre-Synthesis Based on Prime Cycles and Distance Paths. Science of Computer Programming 157 (2018), 41–55. doi:10.1016/j.scico.2017.07.005.
[4] E. Best, R. Devillers, U. Schlachter: Bounded Choice-Free Petri Net Synthesis: Algorithmic Issues. Acta Informatica (2017). doi:10.1007/s00236-017-0310-9.
[5] S. Crespi-Reghizzi, D. Mandrioli. A Decidability Theorem for a Class of Vector-Addition Systems. Inf. Process. Lett., 3(3):78–80, 1975. doi:10.1016/0020-0190(75)90020-4.
[6] J. Desel, J. Esparza: Free Choice Petri Nets. Cambridge Tracts in Theoretical Computer Science 40, 242 pages (1995). doi:10.1017/CBO9780511526558.
[7] R. Devillers: Products of Transition Systems and Additions of Petri Nets. Proceedings of the 16th International Conference on Application of Concurrency to System Design, ACSD, 65–73 (2016). doi:10.1109/acsd.2016.10.
[8] R. Devillers: Factorisation of Transition Systems. Acta Informatica (2017). doi:10.1007/s00236-017-0300-y.
[9] R. Devillers, U. Schlachter: Factorisation of Petri Net Solvable Transition Systems. Proceedings of the 39th International Conference on Applications and Theory of Petri Nets and Concurrency (ICATPN 18), LNCS 10877, 82–98 (2018). doi:10.1007/978-3-319-91268-4_5.
[10] A. Ehrenfeucht, G. Rozenberg: Partial 2-Structures, Part I: Basic Notions and the Representation Problem, and Part II: State Spaces of Concurrent Systems. Acta Informatica, Vol. 27(4), 315–368 (1990). doi:10.1007/BF00264611 and doi:10.1007/BF00264612.
[11] R.M. Keller: A Fundamental Theorem of Asynchronous Parallel Computation. Parallel Processing, LNCS Vol. 24, Springer-Verlag, 102–112 (1975). doi:10.1007/3-540-07135-0_113.
[12] A. Kondratyev, J. Cortadella, M. Kishinevsky, E. Pastor, O. Roig, A. Yakovlev: Checking Signal Transition Graph Implementability by Symbolic BDD Traversal. Proc. European Design and Test Conference, 325–332, Paris, France (1995). doi:10.1109/EDTC.1995.470376.
[13] L.H. Landweber, E.L. Robertson: Properties of Conflict-Free and Persistent Petri Nets. JACM 25(3), 352–364 (1978). doi:10.1145/322077.322079.
[14] W. Reisig: Petri Nets. EATCS Monographs on Theoretical Computer Science 4, Springer-Verlag (1985). doi:10.1007/978-3-642-69968-9.
[15] U. Schlachter et al.: https://github.com/CvO-Theory/apt (2013– 2018).
[16] E. Teruel, J.M. Colom, M. Silva: Choice-Free Petri Nets: a Model for Deterministic Concurrent Systems with Bulk Services and Arrivals. IEEE Transactions on Systems, Man and Cybernetics, Part A, 27-1 (1997), 73-83. doi:10.1109/3468.553226.
[17] H. Wimmel: Presynthesis of Bounded Choice-Free or Fork-Attribution Nets. Technical Report No. 01/18 in: Berichte aus dem Department für Informatik, University of Oldenburg, Germany, ISSN 1867-9218, 29 pages (2018).
Bibtex
@article{sacscuza:best2018spns, title={Simultaneous Petri Net Synthesis}, author={E. Best, R. Devillers, U. Schlachter, H. Wimmel}, journal={Scientific Annals of Computer Science}, volume={28}, number={2}, organization={``A.I. Cuza'' University, Ia\c si, Rom\^ania}, year={2018}, pages={199–236}, publisher={``A.I. Cuza'' University Press, Ia\c si} }