Petrinetze sind ein mathematisches Modell zur Beschreibung diskreter, nebenläufiger und verteilter Systeme. Sie wurden 1962 von Carl Adam Petri in seiner Dissertation „Kommunikation mit Automaten“ eingeführt und sind seitdem ein Standardwerkzeug der Informatik, um parallele Abläufe präzise zu modellieren und zu analysieren.
Aufbau
Ein Petrinetz ist ein gerichteter bipartiter Graph mit zwei Knotenarten:
- Stellen (Places): Kreise, sie repräsentieren Zustände, Ressourcen oder Bedingungen.
- Transitionen (Transitions): Rechtecke, sie repräsentieren Ereignisse oder Aktionen.
- Kanten (Pfeile): verbinden Stellen mit Transitionen und umgekehrt.
- Marken (Tokens): kleine Punkte in den Stellen; die Verteilung der Marken (Markierung) ist der aktuelle Zustand des Systems.
Schaltregel
Eine Transition ist aktiviert, wenn jede Vorstelle mindestens eine Marke enthält. Beim Schalten (Feuern) wird aus jeder Vorstelle eine Marke entnommen und in jede Nachstelle eine Marke gelegt — das System wechselt damit in einen neuen Zustand. Diese Regel macht Nebenläufigkeit sichtbar: Zwei Transitionen mit disjunkten Vorstellen können gleichzeitig schalten.
Eigenschaften und Analyse
Zu den wichtigsten untersuchten Eigenschaften zählen:
- Erreichbarkeit: Ist ein bestimmter Zustand vom Startzustand aus erreichbar?
- Beschränktheit: Bleibt die Markenzahl in jeder Stelle begrenzt?
- Lebendigkeit: Kann jede Transition im weiteren Verlauf wieder schalten?
- Deadlock-Freiheit: Gibt es Zustände, in denen keine Transition mehr aktiviert ist?
Analysiert wird über Erreichbarkeitsgraphen, S- und T-Invarianten oder Werkzeuge wie PIPE und LoLA.
Varianten und Anwendung
Es gibt gefärbte Petrinetze (Coloured Petri Nets, Kurt Jensen), zeitbewertete und stochastische Varianten. Eingesetzt werden Petrinetze zur Verifikation von Kommunikationsprotokollen, in der Workflow-Modellierung, in Fertigungssystemen und im Geschäftsprozessmanagement. Sie erweitern das Konzept des Zustandsautomaten um explizite Nebenläufigkeit — und bilden die theoretische Grundlage der Ablaufsteuerungen GRAFCET und SFC in der Automatisierungstechnik.