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

Die Komplexitat der Synthese von Petrinetzen ist zwar polynomiell, aber mit einem hohen Exponenten. Viele strukturelle Eigenschaften von Petrinetzen sind hingegen lokal und können mit Hilfe des Erreichbarkeitsgraphen in höchstens quadratischer Zeit geprüft werden.

ASYST verfolgt die Idee einer Phase der Präsynthese, die vor der eigentlichen Synthese stattfindet. In Abhängigkeit von der Zielklasse der Petrinetze kann ein gegebenes Transitionssystem zu dieser Zeit auf verschiedene notwendige Eigenschaften geprüft werden. Gilt eine solche Eigenschaft nicht, kann die eigentliche Synthese komplett vermieden werden.

Darüber hinaus liefert dieser Test oft einen nachvollziehbaren Grund, warum die Synthese nicht möglich ist. Innerhalb der Synthese würde man dagegen meist lediglich die Information erhalten, dass ein komplexes Ungleichungssystem nicht lösbar ist.

Ist die Präsynthese erfolgreich, kann sie Informationen liefern, die die Problemstellung und damit die Eingabe für die Synthese vereinfachen, z. B. indem Variablen und Ungleichungen aus einem Ungleichungssystem entfernt werden bevor versucht wird, es zu lösen.

Für eine stark eingeschränkte Klasse von Petrinetzen, die Marked Graphs, konnte gezeigt werden, dass eine Synthese-Phase vollständig unnötig ist [BD14e]. Für die (größere) Klasse „choice-free“ wurde bereits ein schöner Präsynthese-Algorithmus entwickelt [BDS17b]. Jede Klasse von Petrinetzen muss allerdings unabhängig betrachtet werden, da die geltenden strukturellen Eigenschaften jeweils verschieden sein können. Zudem können Eigenschaften auseinander ableitbar sein, so dass die Prüfung mancher Eigenschaften überflüssig sein kann. Die einfache Übernahme der Präsynthese-Phase von einer anderen Netzklasse ist daher nicht unbedingt sinnvoll, für jede Klasse sollten die möglichen Optimierungen getrennt untersucht werden.

[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.