Bounded choice-free Petri net synthesis: algorithmic issues. (English) Zbl 1400.68131

Summary: This paper describes a synthesis procedure dedicated to the construction of choice-free Petri nets from finite persistent transition systems, whenever possible. Taking advantage of the properties of choice-free Petri nets, a two-step approach is proposed. A pre-synthesis step checks necessary structural properties of the transition system and constructs some data structures needed for the second step. Then, a minimised set of simplified systems of linear inequalities is distilled from a general region-theoretic approach. This leads to a substantial narrowing of the sets of states for which linear inequalities must be solved, and allows an early detection of failures, supported by constructive error messages. The performance of the resulting algorithm is measured and compared numerically with existing synthesis tools.


68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI


[1] Badouel, É., Bernardinello, L., Darondeau, P.: Petri Net Synthesis. Texts in Theoretical Computer Science, p. 339. Springer, Berlin (2015). ISBN 978-3-662-47967-4 · Zbl 1351.68003
[2] Badouel, É; Bernardinello, L.; Darondeau, P.; Mosses, P. (ed.); Nielsen, M. (ed.); Schwartzbach, M. (ed.), Polynomial algorithms for the synthesis of bounded nets, No. 915, 364-378, (1995), Berlin
[3] Badouel, É; Bernardinello, L.; Darondeau, P., The synthesis problem for elementary net systems is NP-complete, Theor. Comput. Sci., 186, 107-134, (1997) · Zbl 0893.68111
[4] Badouel, É; Darondeau, P.; Reisig, W. (ed.); Rozenberg, G. (ed.), Theory of regions, No. 1491, 529-586, (1999), Berlin
[5] Badouel, É; Caillaud, B.; Darondeau, P., Distributing finite automata through Petri net synthesis, J. Form. Asp. Comput., 13, 447-470, (2002) · Zbl 1017.68062
[6] Best, E.; Darondeau, P., A decomposition theorem for finite persistent transition systems, Acta Inf., 46, 237-254, (2009) · Zbl 1166.68029
[7] Best, E.; Darondeau, P.; Virbitskaite, I. (ed.); Voronkov, A. (ed.), Petri net distributability, No. 7162, 1-18, (2011), Berlin · Zbl 1336.68175
[8] Best, E.; Erofeev, E.; Schlachter, U.; Wimmel, H.; Moldt, D. (ed.); Kordon, F. (ed.), Characterising Petri net solvable binary words, No. 9698, 39-58, (2016), Berlin · Zbl 1346.68127
[9] Best, Eike; Devillers, Raymond, Synthesis of Persistent Systems, 111-129, (2014), Cham · Zbl 1334.68146
[10] Best, E.; Devillers, R., Synthesis and reengineering of persistent systems, Acta Inf., 52, 35-60, (2015) · Zbl 1310.68148
[11] Best, E.; Devillers, R., State space axioms for T-systems, Acta Inf., 52, 133-152, (2015) · Zbl 1317.68129
[12] Best, E.; Devillers, R., Synthesis of live and bounded persistent systems, Fund. Inf., 140, 39-59, (2015) · Zbl 1335.68164
[13] Best, E., Devillers, R.: Synthesis of bounded choice-free Petri nets. In: Aceto, L., Frutos Escrig, D. (eds.) Proc. 26th International Conference on Concurrency Theory (CONCUR 2015), LIPICS, pp. 128-141. Schloss Dagstuhl—Leibniz-Zentrum für Informatik, Dagstuhl. https://doi.org/10.4230/LIPIcs.CONCUR.2015.128 (2015)
[14] Best, E.; Devillers, R., Characterisation of the state spaces of marked graph Petri nets, Inf. Comput., 253, 399-410, (2017) · Zbl 1409.68183
[15] Best, E., Devillers, R.: Petri net pre-synthesis based on prime cycles and distance paths. To appear in Science of Computer Programming (2018). Also: Informatik-Bericht Nr. 3/16, Univ. Oldenburg, 26 pages (2016)
[16] Caillaud, B.: Synet: un outil de synthèse de résaux de Petri bornés, applications. Research Report RR 3155, INRIA (1997). See also: https://hal.inria.fr/inria-00073534. http://www.irisa.fr/s4/tools/synet/
[17] Carmona, J.; Jensen, K. (ed.); Aalst, WMVD (ed.); Ajmone-Marsan, M. (ed.); Franceschinis, G. (ed.); Kleijn, J. (ed.); Kristensen, LM (ed.), The label splitting problem, No. 7400, 1-23, (2012), Berlin · Zbl 1377.68145
[18] Carmona, J.; Cortadella, J.; Kishinevsky, M.; Kondratyev, A.; Lavagno, L.; Yakovlev, A.; Hee, K. (ed.); Valk, R. (ed.), A symbolic algorithm for the synthesis of bounded Petri nets, No. 5062, 92-111, (2008), Berlin · Zbl 1143.68478
[19] Carmona, J.; Cortadella, J.; Kishinevsky, M., New region-based algorithms for deriving bounded Petri nets, IEEE Trans. Comput., 59, 371-384, (2010) · Zbl 1368.68259
[20] Commoner, F.; Holt, AW; Even, S.; Pnueli, A., Marked directed graphs, J. Comput. Syst. Sci., 5, 511-523, (1971) · Zbl 0238.05109
[21] Christ, Jürgen; Hoenicke, Jochen; Nutz, Alexander, SMTInterpol: An Interpolating SMT Solver, 248-254, (2012), Berlin, Heidelberg
[22] Cortadella, J.; Kishinevsky, M.; Kondratyev, A.; Lavagno, L.; Yakovlev, A., Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers, IEICE Trans. Inf. Syst., E80-D, 315-325, (1997)
[23] Cortadella, J.; Kishinevsky, M.; Lavagno, L.; Yakovlev, A., Deriving Petri nets for finite transition systems, IEEE Trans. Comput., 47, 859-882, (1998) · Zbl 1392.68291
[24] Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Logic Synthesis for Asynchronous Controllers and Interfaces, Volume 8 of Advanced Microelectronics. Springer Science & Business Media, Berlin (2012) · Zbl 1013.68273
[25] Crespi-Reghizzi, S.; Mandrioli, D., A decidability theorem for a class of vector-addition systems, Inf. Process. Lett., 3, 78-80, (1975) · Zbl 0302.68065
[26] de San Pedro, J., Cortadella, J.: Mining structured Petri nets for the visualization of process behavior. In: 31st ACM Symposium on Applied Computing, pp. 839-846, Pisa (2016)
[27] Desel, J., Esparza, J.: Free Choice Petri Nets, vol. 40, p. 242. Cambridge Tracts in Theoretical Computer Science, Cambridge (1995) · Zbl 0836.68074
[28] Dijkstra, EW, Hierarchical ordering of sequential processes, Acta Inf., 1, 115-138, (1971)
[29] Ehrenfeucht, A.; Rozenberg, G., Partial 2-structures, part I: basic notions and the representation problem, and part II: state spaces of concurrent systems, Acta Inf., 27, 315-368, (1990) · Zbl 0696.68082
[30] Erofeev, E., Barylska, K., Mikulski, Ł., Piątkowski, M.: Generating all minimal Petri net unsolvable binary words. In: Proceedings of the Prague Stringology Conference, pp. 33-46 (2016). See http://www.stringology.org/event/
[31] Hopkins, RP; Rozenberg, G. (ed.), Distributable nets. Applications and theory of Petri nets 1990, No. 524, 161-187, (1991), Berlin
[32] Keller, Robert M., A fundamental theorem of asynchronous parallel computation, 102-112, (1975), Berlin, Heidelberg · Zbl 0301.68063
[33] Khachiyan, L.: Selected works. Moscow Center for Mathematical Continuous Education. ISBN 978-5-94057-509-2, 519 pages (2009) (in Russian)
[34] Kondratyev, A., Cortadella, J., Kishinevsky, M., Pastor, E., Roig, O., Yakovlev, A.: Checking signal transition graph implementability by symbolic BDD traversal. In: Proc. European Design and Test Conference, pp. 325-332, Paris (1995)
[35] Landweber, LH; Robertson, EL, Properties of conflict-free and persistent Petri nets, JACM, 25, 352-364, (1978) · Zbl 0384.68062
[36] Murata, T., Petri nets: properties, analysis and applications, Proc. IEEE, 77, 541-580, (1989)
[37] Petri, CA; Brauer, W. (ed.), Concurrency, No. 84, 251-260, (1980), Berlin
[38] Reisig, W.: Petri Nets. EATCS Monographs on Theoretical Computer Science, vol. 4. Springer, Berlin (1985) · Zbl 0521.68057
[39] Schlachter, U. et al.: https://github.com/CvO-Theory/apt (2013-2017)
[40] Teruel, E.; Colom, JM; Silva, M., Choice-free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals, IEEE Trans. Syst. Man Cybern. Part A, 27-1, 73-83, (1997)
[41] van Glabbeek, R.J., Goltz, U., Schicke-Uffmann, J.-W.: On distributability of Petri nets—(extended abstract). In: Birkedal, L. (ed.) Proc. FoSSaCS 2012 (Held as Part of ETAPS), LNCS, vol. 7213, pp. 331-345. Springer, Berlin (2012) · Zbl 1352.68192
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.