Algorithmen für Synthese und Präsynthese auf Grundlage der Strukturtheorie von Petrinetzen (ASYST)
Zusammenfassung der Projektergebnisse
Zielsetzung des Projekts war die Entdeckung von möglichst effizienten Synthese-Algorithmen und -Methoden, wenn verteilte Systeme durch verschiedene Typen von Petrinetzen dargestellt werden und Spezifikationen durch beschriftete Transitionssysteme oder durch Verallgemeinerungen davon (modale Transitionssysteme). Ergebnisse des Projekts sind: • Ein Spektrum effizienter und getesteter Algorithmen für Spezialfälle der Anwendungsbereiche Entwurf asynchroner Hardware und Geschäftsprozessmodellierung. • Eine Systematik zur Integration von Quick Fail in einer zweiphasigen (Prä-)Synthese, wodurch sich widersprüchliche Spezifikationen frühzeitig erkennen und verbessern lassen. • Eine Methode zur Auswahl verschiedener Synthesealgorithmen in Abhängigkeit von einer gewünschten Zielklasse von Systemen. • Eine Methode der Erzeugung von optimalen (d.h. minimalen) Erweiterungen der Aktionsmenge eines Systems, um alle (auch nichtdeterministische) Spezifikationen implementieren zu können. Diese Methode leitet sich aus einer systematischen Untersuchung von nicht direkt implementierbaren Separationsproblemen in gewissen lokalen Teilen eines Systems her. • Die Erweiterung der Methode auf die mächtige Spezifikationssprache der (hyper-)modalen Transitionssysteme und auf die simultane Synthese, d.h. die gleichzeitige Nutzung ähnlicher Hardware durch verschiedene Protokolle, die sich in ihren Anfangszuständen unterscheiden. • Theoretische Neuentwicklungen inklusive der Benutzung von Näherungsmethoden und inklusive der Beantwortung mehrerer offener Fragen aus der bekannten Literatur. Das unmittelbarste Anwendungspotential liegt in den beiden oben genannten Bereichen, vor allem im asynchronen Hardware-Entwurf. Weitere Anwendungsbereiche erschließen sich voraussichtlich durch die Erweiterung auf modale Transitionssysteme, insbesondere da die Übertragung von Ergebnissen auf beschriftete (statt unbeschriftete) Petrinetze gelungen ist. Für eine ganze Reihe von (teils anwendungsrelevanten) Spezialfällen ist eine exakte graphentheoretische Charakterisierung der Zustandsmenge gelungen. Frühere und neue Ergebnisse und Algorithmen für unbeschriftete Petrinetze ließen sich zwar nichttrivial, aber reibungsloser als erwartet auf beschriftete Netze übertragen. Diese Netzklasse spielt eine überragende Rolle beim Entwurf asynchroner, zeitunabhängiger Schaltkreise. Eine große Herausforderung bei der Erstellung komplexer verteilter Systeme ist deren Korrektheit. In solchen System gibt es keine zentrale Einheit, die die Gesamtsituation kennt, sondern jede Komponente muss eigenständig agieren. Hierdurch wird es umso schwerer, Probleme zu diagnostizieren. Daher ist es sinnvoll, ein System zum Beispiel formal mit Petrinetzen zu modellieren, rigoros zu analysieren und seine Korrektheit zu beweisen. Es ist jedoch aufwändig, ein passendes Petrinetz mit den gewünschten Eigenschaften zu erzeugen. Daher wird die Synthese betrachtet: Anstatt ein Modell per Hand zu generieren und anschließend zu prüfen, ob es sich korrekt verhält, wird das gewünschte Verhalten an einen Algorithmus übergeben, der automatisch ein passendes Modell erzeugt. Dieses Modell ist dann per Konstruktion fehlerfrei und muss nicht näher untersucht werden. Ein solcher Algorithmus ist zeitkritisch, und deshalb ist es wichtig, ihn möglichst gut zu optimieren. Im Projekt ASYST wurden verschiedene Arten und Aspekte von Petrinetz-Synthese untersucht. Einerseits wurde untersucht, auf welche Weise das gewünschte Verhalten beschrieben werden kann. Anstatt explizit einen Zustandsraum oder eine formale Sprache anzugeben, ist es jetzt auch möglich, Petrinetze aus modalen Spezifikationen zu synthetisieren. Diese erlauben es, ein Verhalten flexibel zu beschreiben, ohne dass alles schon genau festgelegt ist. Ein anderer Vorschlag von ASYST ist die Prä-Synthese. Manche Spezifikationen sind widersprüchlich und beschreiben kein mögliches System. In der Prä-Synthese wurden Ansätze entwickelt, um solche unlösbaren Eingaben effizient zu erkennen und früh ablehnen zu können, ohne dass bereits die gesamte Synthese durchgeführt werden muss. Die bei der Prä-Synthese gewonnenen Erkenntnisse erlauben anschließend eine schnellere Synthese. Ein dritter Ansatz ist die systematische Aktionserweiterung durch die Betrachtung von lokalen Systemteilen, die sich einer direkten Implementierung widersetzen. Diese Methode ist besonders relevant beim Entwurf digitaler Schaltkreise, wo Hardware eingespart werden muss.
Projektbezogene Publikationen (Auswahl)
- k-Bounded Petri Net Synthesis from Modal Transition Systems. In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 6:1– 6:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017
Uli Schlachter and Harro Wimmel
(Siehe online unter https://doi.org/10.4230/LIPIcs.CONCUR.2017.6) - Simultaneous Petri Net Synthesis. Sci. Ann. Comp. Sci., 28(2):199–236, 2018
Eike Best, Raymond R. Devillers, Uli Schlachter, and Harro Wimmel
(Siehe online unter https://doi.org/10.7561/SACS.2018.2.199) - Efficient Synthesis of Weighted Marked Graphs with Circular Reachability Graph, and Beyond. Accepted for publication in ToP- NoC, CoRR, abs/1910.14387, 2019
Raymond R. Devillers, Evgeny Erofeev, and Thomas Hujsa
(Siehe online unter https://doi.org/10.48550/arXiv.1910.14387) - Relabelling LTS for Petri Net Synthesis via Solving Separation Problems. Trans. Petri Nets Other Model. Concurr., 14:222–254, 2019
Uli Schlachter and Harro Wimmel
(Siehe online unter https://doi.org/10.1007/978-3-662-60651-3_9) - Synthesis of Reduced Asymmetric Choice Petri Nets
Harro Wimmel
(Siehe online unter https://doi.org/10.48550/arXiv.1911.09133) - Presynthesis of Bounded Choice-Free or Fork-Attribution nets. Inf. Comput., 271:104482, 2020
Harro Wimmel
(Siehe online unter https://doi.org/10.1016/j.ic.2019.104482)
