Project ASYST (Algorithms for Synthesis and Pre-Synthesis Based on Petri Net Structure Theory), 2017–2020, supported by DFG (Deutsche Forschungsgemeinschaft), Geschäftszeichen Be 1267/16-1.

• Prof. Dr. Eike Best, Principal Investigator
• Dr. habil. Harro Wimmel, Senior Researcher (part time)
• M.Sc. Evgeny Erofeev, Research Associate

Petri net synthesis is of polynomial time complexity, but with a rather high exponent. Many structural properties of Petri nets, on the other hand, are local and can be computed via the reachability graph in at most quadratic time.

The idea of ASYST is to introduce a pre-synthesis stage before the synthesis. Depending on the class of Petri nets we aim at, a given transition system may be checked for different necessary properties during this phase. If such a property fails to hold, a full synthesis can be avoided at all, and we usually even get an understandable explanation why the synthesis is impossible. In contrast, if the synthesis fails, we normally just get the information that some complex inequation was unsolvable.

If the pre-synthesis is successful, we might derive information that can reduce the input for the synthesis, e.g. by removing variables and whole inequations from a system of inequations before a solver is called.

For a very restricted class of Petri nets, the class of marked graphs, it was shown that the synthesis can be completely omitted [BD14e]. For the (larger) class of choice-free Petri nets, a nice pre-synthesis algorithm has been found [BDS17b]. Each class needs to be handled separately, though, since its structural properties may be different. Also, some properties may be derivable from combinations of others, so not all of them need to be checked. Copying a pre-synthesis stage from another class is thus difficult, classes should to be investigated largely independently.

[BHW18] Eike Best, Thomas Hujsa, Harro Wimmel: Sufficient conditions for the marked graph realisability of labelled transition systems. Theoretical Computer Science Vol. 750, pp. 101-116 (2018), DOI: 10.1016/j.tcs.2017.10.006.

[EW17] Evgeny Erofeev, Harro Wimmel: Reachability Graphs of Two-Transition Petri Nets, ATAED 2017 (Algorithms & Theories for the Analysis of Event Data), Zaragoza, Spain, June 26–27, 2017, W. van der Aalst, R. Bergenthum, J. Carmona (eds.), CEUR workshop proceedings Vol. 1847, ISSN 1613-0073.

[BDS17b] Eike Best, Raymond Devillers, Uli Schlachter: Bounded Choice-Free Petri Net Synthesis: Algorithmic Issues. Extended version of [BD15d], accepted for publication in Acta Informatica (2017).

[SW17]

Uli Schlachter, Harro Wimmel: k-Bounded Petri Net Synthesis from Modal Transition Systems. In 28th International Conference on Concurrency Theory, CONCUR 2017, Berlin, Germany, September 5-8, 2017, Proceedings, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, DOI: 10.4230/LIPIcs.CONCUR.2017.6