Petrinetze, lineare Algebra und lineare Programmierung : Analyse, Verifikation und Korrektheitsbeweise von Systemmodellen

Der Titel dieser Arbeit ist bereits ei ne kurze Inhaltsangabe. Es geht darum, die Matrixrepräsentation von Petrinetzen in Gleichungs- und Ungleichungs­ systemen auszunutzen, urn Aussagen über das Verhalten eines Netzmodells gewinnen oder beweisen zu können. Die Motivation für die Verwendung linear-algebraischer Verfahren liegt in der Komplexität des Verhaltens von Petrinetzen. So explodiert die Anzahl erreich­ barer Markierungen eines markierten Petrinetzes sowohl mit wachsender GröBe des Netzes als auch mit wachsender Zahl anfangs verteilter Marken. Eine di­ rekte Aufzählung aller erreichbarer Markierungen ist deshalb praktisch nicht möglich. Mit Hilfe von Gleichungs- und Ungleichungssystemen lassen sich aber häufig wenigstens hinreichende oder notwendige Bedingungen für dynamische Eigenschaften ei nes markierten Netzes formulieren; ei ne linear-algebraische Analyse erlaubt so, Informationen über das Verhalten eines markierten Netzes zu gewinnen. Zur Überprüfung der Gültigkeit derartiger linear-algebraischer Bedingungen existieren effiziente Algorithmen. Ihre Komplexität hängt we­ sentlich davon ab, ob rationale, ganzzahlige oder natürlichzahlige Lösungen gesucht werden. Oftmals gibt es einen Trade-off: Alle Lösungen haben ei ne Bedeutung, aber die effizienteren Algorithmen haben ei ne geringere Aussage­ kraft als die komplexeren. Optimierte Routinen für Matrixoperationen können mit proprietären Analyseverfahren für Petrinetze kombiniert werden. Das Thema dieser Arbeit ist annähernd so alt wie Petrinetze selbst. Schon Mitte der siebziger Jahre wurden erste einschlägige Arbeiten veröffentlicht. Leider verwenden Autoren seitdem immer wieder neue Notationen, so daB ein einheitliches Bild des State-of-the-art nur schwer zu bekommen ist. Auch be­ ziehen sich viele Veröffentlichungen auf eingeschränkte Netzklassen.