Die Petri Nets 2024 Konferenz in Genf

Vom 26. bis zum 28. Juni fand der Main-Track der Petri Nets Konferenz in Genf statt. Gemeinsam haben wir auf dem Campus Biotech die neusten Erkenntnisse der Forschung bestaunt, mit Petrinetzen und frischen Ideen im Herzen die Bars der Stadt unsicher gemacht und selbst Wind und Wetter getrotzt, um über unser Lieblingsthema hinaus etwas über den Botanischen Garten von Genf zu erfahren.

Der erste eingeladene Vortrag wurde im Gedenken an Manuel Silva gehalten, der bedauerlicherweise am 28. November 2022 verstarb. Manuel bereicherte die Petrinetz-Welt mit revolutionären Ideen zur Strukturtheorie, die Jose in seinem Vortrag aufzeigte und nutzte, um Event-Systeme zu simulieren. In seinem Vortrag demonstrierte er uns, dass Unbeschränktheit in Petrinetzen auch hier ein Problem darstellen kann, das sich jedoch überwinden lässt, wenn man sich in anderen Disziplinen der Mathematik umschaut. So formulierte er die Vorbedingungen von Transitionen als Funktionen, die entweder lokal oder global auf einem verteilten System ausgewertet werden können, mit denen selbst sehr große Netze in überschaubarer Zeit auf verteilten Systemen simuliert werden können.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_1

Wer schon einmal ein Menü in einer Fast-Food Kette bestellt hat weiß, dass es dafür nicht nur eine Möglichkeit gibt. "Burger, Pommes, Getränk", "Getränk, Pommes, Burger" und "Pommes, Burger, Getränk" sind alles Varianten derselben Bestellung, die in Systemmodellen aber potenziell für viel Komplexität sorgen können. Akio Watanabe definiert aus diesem Grund einen neuen Knoten für Process Trees, der diese sogenannte MIX-Sprache einfach abbilden kann. Aus diesen erweiterten Process Trees gewinnt er eine erweiterte Form kontextfreier Grammatiken, in denen parallele Aktivitäten in einem Wort als Tupel dargestellt werden. Diese Grammatiken nutzt er, um zu zeigen, dass das Wortproblem für MIX-Sprachen entscheidbar ist und seine Erweiterung der Process Trees damit praktisch nutzbar ist.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_3

Conformance Checking für datenorientierte Prozesse erhält in der Forschung immer mehr Aufmerksamkeit, so auch von Dominique Sommers. In seinem Vortrag zeigte er uns, dass existierende Methoden zum Conformance Checking datenbasierte Fehler nicht erkennen können, wie etwa Multitasking oder plötzliche Kontextwechsel einer Ressource. Bisherige Methoden zum datenorientierten Conformance Checking berücksichtigen entweder nur die Schaltfolgen im Netz und können solche Fehler damit nicht erkennen oder haben eine so globale Sicht auf das Modell, dass sie nicht analysieren können, wo genau der Fehler liegt. Dominique stellte uns deshalb ein Verfahren vor, mit dem er das Beste aus beiden Welten erhält: Eine Sicht auf das gesamte Modell, dessen Sicht lokal genug ist, um die Fehler in einem Ablauf genau analysieren zu können.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_4

Tobias Brockhoff beschäftigt sich in seiner Forschung mit einem interessanten Problem: Was kann man tun, wenn man zwei verschiedene Geschäftsprozesse miteinander vergleichen möchte? Mit zwei Petrinetzen und dessen Verhaltensbeschreibungen als Eingabe kann solch ein Vergleich schnell sehr viel Laufzeit kosten -- ganz besonders, wenn man für den Vergleich von nicht exakt gleichem Verhalten Alignments nutzen möchte. Mit dem Kredo "Divide and Conquer" im Hinterkopf partitioniert er daher die Netze und erhält einen Baum, der die Hierarchie der Subnetze repräsentiert. Diese Subnetze sind viel leichter zu analysieren und zu vergleichen als das gesamte Netz, wie er an einem Beispiel demonstriert, das sich mit der Zahlung von Straf-Gebühren in verschiedenen Ländern beschäftigt.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_5

Für die Arbeit von Serge Haddad stehen besonders die Transitionen im Vordergrund, die in der Zukunft auftreten können. Für eine Markierung M definiert er deshalb dessen Modus als die Menge der Transitionen, die in einer von M aus erreichbaren Markierung schalten können. Für eine Schaltsequenz definiert er anschließend die Sequenz solcher Modi als Trajectory. Für allgemeine Place/Transition-Netze sind schon einige Eigenschaften für Trajectories bekannt. Für die Klasse der Continuous Petri nets, in denen Transitionen auch zu einem Bruchteil schalten können, wenn für die normale Schaltregel nicht genügend Marken vorhanden sind, wurden sie aber noch nicht näher analysiert. Dies holt Serge nach und erhält einige interessante Ergebnisse.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_6

Die Synchronisation von Aktivitäten ist nicht nur in Petrinetzen, sondern auch anderen Modelltypen ein entscheidender Bestandteil. Elvio Gilberto Amparore hat es sich deshalb zum Ziel gesetzt, ein Petrinetz-Kalkül zu definieren, in dem sich solche Synchronisationen leicht abbilden lassen. Dafür definiert er eine Graver-Basis -- die Vereinigung von Hilbert-Basen passender Monoide -- für Petrinetze und deren Transitionen. Mithilfe solcher Basen gelingt es ihm, verschiedene Eigenschaften, wie Endlichkeit und Eindeutigkeit synchronisierter Events zu zeigen. Zusammen mit dem Synchronisations-Operator, der parallelen Komposition und einem Restriktions-Operator definiert er darüber hinaus ein Synchronisations-Kalkül mit interessanten Eigenschaften.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_7

Wenn wir über nebenläufige Transitionen sprechen, nehmen wir häufig implizit an, dass diese atomar sind -- also keine Zeit verbrauchen, um zu schalten. Diese Annahme ist oft unrealistisch, wie Łukasz Mikulski uns schon mit einem kleinen Computerprogramm demonstrieren konnte: Insbesondere wenn parallele Teile des Programms ohne Synchronisation auf dieselben Daten zugreifen, kann es schnell zu Verschränkungen des Programmablaufs kommen, die zu überraschenden Effekten führen. Mit diesem Hintergrund verabschiedet Łukasz sich deshalb von dieser atomaren Sicht und stellt stattdessen eine Intervall-Semantik für Transitionen vor. Diese stellte er als Graphen mit unterschiedlichen Kanten-Typen dar und zeigte uns daran, wie diese Semantik funktioniert und welche Eigenschaften sie hat.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_8

Was ist eigentlich das Verhalten eines Petrinetzes? Mit dieser Frage beschäftigt sich Jakub Kovář, denn mögliche Antworten gibt es viele: Eine Menge von Wörtern, ein Transitionssystem, eine partielle Ordnung, und noch viele mehr. Im Kern versuchen all diese Strukturen auf unterschiedliche Arten dasselbe zu erreichen, weshalb Jakub sich fragte: Gibt es eine Struktur, die eine globalere Sicht auf das Verhalten eines Netzes zulässt? Hierfür definiert er sogenannte Token-Trails und zeigte uns in seinem Vortrag sehr anschaulich an Beispielen, wie sie das Verhalten eines Netzes beschreiben können, ohne etwas von der Ausdrucksmächtigkeit von Petrinetzen einbüßen zu müssen. Es stellt sich außerdem heraus, dass sich Token Trails aus synchronen Morphismen ableiten lassen.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_9

Hugo Bazille versteht sich sicher gut mit Łukasz Mikulski, denn auch er will sich von der Annahme lösen, dass Transitionen sich atomar verhalten. Stattdessen will er stets ermöglichen, dass sich zwei parallele Transitionen a und b so verhalten können, dass a startet, b in der Zwischenzeit startet und seine Aufgabe beendet, bevor a ebenfalls fertig ist. Solche und andere Verschachtelungen können mit höherdimensionalen Automaten abgebildet werden, die zwischen n parallelen Transitionen nicht nur Kanten ziehen, sondern eine Ebene der Dimension n aufspannen. Diese Automaten erweitert Hugo in seiner Arbeit, indem er sie um die Konzepte von Timed Automatas anreichert. Er betrachtet anschließend Entscheidbarkeits-Eigenschaften von diesem neuen Automaten-Typ und kommt und spannenden Ergebnissen.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_10

Dass Petrinetze in verschiedenen Disziplinen gerne zum Einsatz kommen, mag sich schnell zeigen, wenn man sich etwas intensiver umsieht. Wie viel Gewinn sie aber für Geschäftsprozesse versprechen, zeigte uns Gabriele Taentzer in ihrer Keynote. Da sich in der Firma nicht jeder Entscheidungsträger mit Prorammiersprachen auskennen kann, gibt es einen starken Trend zu Low-Code bzw. No-Code Konzepten. Da Modelle für Geschäftsprozesse sehr oft mit Blick auf Kosten, Zeit und Aktivitäts-Kopplung optimiert werden sollen, stellte sie Evolutionäre Algorithmen zum Finden solcher optimaler Modelle vor. Sie zeigte uns am Beispiel der Software-Entwicklung, wie man leicht die dazu benötigten Funktionen zur Komposition und Mutation von Netzen implementieren kann.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_2

Direkt nach der Keynote zeigte uns Damien Morard, wie man mit unendlichen Mengen von Markierungen umgehen kann. Dazu definierte er Markierungen als Vektoren und konnte so eine Intervall-Semantik für Markierungen aufbauen, die nicht nur intuitiv, sondern auch ausdrucksstark ist. Damit kann er eine starke Alternative zu bereits bekannten Verifikations-Algorithmen für Petrinetze anbieten: Anstatt zu einem markierten Netz und einer Formel in CTL einen Wahrheitsewert zurückzugeben, der repräsentiert ob die Formel erfüllt ist, gibt er zu denselben Eingaben Intervalle von erreichbaren Markerungen zurück, für welche die Formel korrekt ist.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_13

Lucie Guillou abstrahiert von Petrinetzen und betrachtet stattdessen Automaten, die über read-, send- und broadcast-Kanten miteinander kommunizeren können. Bisherige Ergebnisse für solche Automaten nahmen bisher aber immer an, dass die Anzahl der kommunizerenden Agenten bekannt ist – eine starke Voraussetzung, die in der Realität nicht immer gegeben ist. Sie untersuchte deshalb, ob diese Eigenschaft wirklich notwendig ist und konnte neue Erkenntnisse zur Komplexitätsklasse der Verifikationsprobleme state-cover und conf-cover gewinnen.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_14

Die Verifikation von Petrinetzen stößt bei größeren Netzen häufig auf das Problem, dass die Anzahl der Zustände im Netz exponentiell zur Anzahl der Stellen ist. Insbesondere bei komplexeren Algorithmen ist eine Analyse in vertretbarer Zeit damit praktisch unmöglich. Sophie Wallner entwickelte deshalb ein Verfahren, mit dem sie ein Petrinetz in überschaubare Teile partitinonieren kann, deren Zustandsräume wesentlich kleiner und die damit leichter zu analysieren sind als das gesamte Netz. Mit der Definition von Interface-Transitionen, sowie einer spezielle Schaltregel für diese, stellt sie dabei sicher, dass das Verhalten des Netzes dasselbe bleibt. Mit diesem Vorgehen konnte sie zeigen, dass Eigenschaften, die auf dem Reachability Set des Netzes basieren, leicht überprüft werden können. Liveness und Reversibility sind komplexer, doch auch für diese Eigenschaften versprach sie uns in ihrem Paper eine Lösung.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_15

An den vorherigen Vortrag direkt anknüpfend zeigte uns Lukas Zech weitere Möglichkeiten, die Partition von Netzen für Verifikations-Methoden zu nutzen. Im Speziellen demonstrierte er, wie sich LTL und CTL Formeln mit dieser Idee effizienter prüfen lassen. Dafür definiert er eine schwache Bisimulation auf diesen partitionierten Erreichbarkeitsgraphen, die sich sicherlich auch für andere Algorithmen als nützlich erweisen kann.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_16

Im ersten Vortrag der Tool-Session präsentierte uns Luis Gomes ein spannendes Tool, mit welchem sich das von einem Petrinetz spezifizierte Verhalten automatisiert in Code übersetzen lässt. Diesen Code kann man anschließend mit einer kurzen Installation auf einem Arduino-Board ausführen. Hierbei legten er und seine Gruppe besonderen Fokus auf Ein- und Ausgaben, wofür sie Input-Output-Place-Transition Netze verwendeten. In dem Tool lassen sich solche Netze umfassend erstellen, die auf Sensordaten reagieren.

Link zum Tool:  http://gres.uninova.pt/IOPT-Tools-V1.2/login.php

Van-François Le stellte während seiner Arbeit mit Petrinetzen schnell fest, dass es viele Tools für Petrinetze gibt. Jedes Tool folgt aber einem speziellen Use-Case und betrachtet daher oft nur eine Klasse von Petrinetzen. Problematisch wird das, wenn man den Algorithmus aus einem Tool gerne auf einem Petrinetz aus einem anderen Tool anwenden möchte. Er und seine Kollegen erkannten dieses Problem und bieten deshalb mit CosyVerif eine einheitliche Plattform an, auf der man sowohl die bereits etablierten Algorithmen verschiedener Tools nutzen, als auch eigene spezifizieren und verwenden kann. Gemeinsam mit der Möglichkeit, das Petrinetz durch “aufmalen” zu spezifzieren entsteht so eine tolle Plattform für Experimente und Analysen.

Link zum Tool:  https://draw.cosyverif.org

Petrinetze haben bereits viele Erweiterungen erfahren, doch eine besonders wichtige mögen Referenz-Netze sein. In dieser Netzklasse können Marken Referenzen zu beliebigen Objekten oder sogar anderen Netzen sein. RENEW bietet speziell für diese Netzklasse eine Plattform zum Ausprobieren, Modellieren und Implementieren ohne mit Java-Code hantieren zu müssen.

Link zum Tool:  http://renew.de

Die Ausdrucksmächtigkeit von Petrinetzen in einer realen Anwendung auszunutzen ist manchmal gar nicht so einfach. Das zeigte uns auch Rob van Glabbeck in seiner Keynote, indem er uns mit leicht zu verstehenden Beispielen demonstrierte, dass es kein gutes Rezept gibt, um solche Netze auf die Akteure eines verteilten Systems aufzuteilen. Direkte Vorgehensweisen haben oft triviale Lösungen, die dem Sinn entbehren. Deshalb verschärfte er seine Voraussetzungen an verteilte Versionen von Petrinetzen und fragte sich: Welche Bedingungen muss eine Systemspezifikation erfüllen, um in einem verteilten System implementiert werden zu können? Er fand heraus, dass es im Wesentlichen drei Dimensionen gibt, die dies beeinflussen und bei denen man immer mindestens von einer abstrahieren muss, um keine triviale Lösung zu erhalten.

Machine Learning hat es längst in die Gesellschaft geschafft, sodass die Forschung in dessen Teilbereichen in letzter Zeit umso intensiver betrieben wird. Das stellte auch Alex Chan fest, der jedoch genauere Informationen darüber erhalten will, wie genau diese Algorithmen funktionieren. Aus diesem Grund hat er sich sogenannte Tsetlin Machines genauer angesehen, deren Funktionsweise zwar wesentlich einsichtiger ist als etwa die von neuronalen Netzen, aber dennoch sehr komplex ist. Er nutzt deshalb die Ausdrucksmächtigkeit von Petrinetzen, um Tsetlin Machines zu modellieren und so mehr Einblicke über die Eigenschaften dieser Form des Machine Learnings zu gewinnen.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_17

Für Forscher und Anwender existieren eine Menge Sammlungen von Petrinetzen, mit denen sich Algorithmen an realen Instanzen ausprobieren lassen. Solche Sammlungen haben aber oft das Problem, dass sie bestimmte Netze mehrfach enthalten, da sie ihre Daten aus mehreren ähnlichen Quellen beziehen. Direkt erkennen kann man solche Duplikate nicht, weshalb sich Hubert Garavel damit beschäftigt, wie man sie dennoch identifizieren und entfernen kann. Dafür nutzt er mehrere Schritte, um die Sammlung in Äquivalenzklassen aufzuteilen und so erkennen zu können, welche Netze definitiv gleich oder definitiv unterschiedlich sind. Einige Sonderfälle fallen zwar noch durch das Raster, jedoch konnte er durch Experimente an existierenden Sammlungen zeigen, dass schon etwa 90% der Duplikate dieser Sammlungen erkannt werden können.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_18

Dass unsere Forschung nicht nur theoretische, sondern auch sehr wichtige praktische Anwendungen hat, zeigte uns Carolina Lagartinho-Oliveira in ihrem Vortrag. Gemeinsam in ihrem Team nutzt sie Petrinetze, um digitale Zwillinge von elektrischen Rollstühlen zu entwickeln. Dadurch kann sie diese digitalen Zwillinge formal analysieren und Eigenschaften über sie nachweisen, die sich in der Entwicklung als sehr nützlich erweisen können. Da die digitalen Rollstühle auf Inputs reagieren, nutzt sie hierfür Input-Output-Place-Transition Netze, die ebenfalls auf Eingaben von außen reagieren können. Wer noch einen Schritt weiter gehen möchte, kann das in diesen Netzen beschriebene Verhalten automatisiert auf dem Rollstuhl deployen und am realen System ausprobieren.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_20

Die klassische Version der Netz-Synthese nimmt einen endlichen Automaten (oder eine Sprache) als Eingabe und findet Stellen in einem Petrinetz, das dieselben Transitionen enthält wie der Automat. Raymond Devillers möchte dies aber umdrehen: Was, wenn wir die Stellen im Petrinetz bereits (in Form von Markierungen) kennen, aber die Transitionen bestimmen müssen? Um aus dieser Frage kein triviales Problem zu machen, will er duplizierte Transitionslabel nach Möglichkeit vermeiden und ausschließlich die Markierungen erlauben, die in der Input-Menge angegeben sind. Besonderes Augenmerk legte er dabei auf Netze, die nicht T-monoton sind, bei denen das Entfernen einer Transition also dazu führt, dass das entstehende Netz eine andere Netzklasse hat als das vorherige.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_11

Im letzten Vortrag der Konferenz stellte uns Loïc Hélouët ein sehr praktisches Problem vor: Er möchte mithilfe von Petrinetzen die Taktung von Zugfahrten modellieren, wobei bestimmte Einschränkungen berücksichtigt werden sollen. Eine solche Einschränkung ist etwa, dass sich nicht zwei Züge gleichzeitig in einem Tunnel befinden sollen. Dazu nutzt er sogenannte Trajectory Nets, bei denen es sich um Timed Petrinetze handelt, die zusätzlich mit Funktionskurven ausgestattet sind, die den Weg eines Zuges beschreiben. Diese erweiterte er um Funktionsbereiche, die auch ausdrücken können, dass ein Zug zu spät oder zu früh ist und zeigte uns, wie man mit diesen etwa prüfen kann, ob sich tatsächlich nur ein Zug gleichzeitig in einem Tunnel befindet.

Link zum Paper:  https://link.springer.com/chapter/10.1007/978-3-031-61433-0_12

Nach dem letzten Vortrag hieß es dann auch schon, Abschied zu nehmen: Von Freunden, Forschungskollegen und natürlich von Genf. Einige mussten sich direkt auf den Weg zum Zug machen, andere nutzten noch den Rest des Tages, um sich die schönsten Stellen der Stadt anzusehen und noch etwas die gemeinsame Zeit ausnutzen. Denn die nächste Petri Nets Konferenz findet wieder erst in einem Jahr statt: Vom 23. bis zum 27. Juni 2025 in Paris.

Ich hoffe, wir sehen uns dort!

Eure Patrizia.