Petrinetze, Lineare Algebra Und Lineare Programmierung: Analyse, Verifikation Und Korrektheitsbeweise Von Systemmodellen

ISBN-13: 9783815423127 / Niemiecki / Miękka / 1998 / 133 str.

Jorg Desel; Jorg Desel

Opis

Der Titel dieser Arbeit ist bereits ei ne kurze Inhaltsangabe. Es geht darum, die Matrixreprasentation von Petrinetzen in Gleichungs- und Ungleichungs systemen auszunutzen, urn Aussagen uber das Verhalten eines Netzmodells gewinnen oder beweisen zu konnen. Die Motivation fur die Verwendung linear-algebraischer Verfahren liegt in der Komplexitat des Verhaltens von Petrinetzen. So explodiert die Anzahl erreich barer Markierungen eines markierten Petrinetzes sowohl mit wachsender GroBe des Netzes als auch mit wachsender Zahl anfangs verteilter Marken. Eine di rekte Aufzahlung aller erreichbarer Markierungen ist deshalb praktisch nicht moglich. Mit Hilfe von Gleichungs- und Ungleichungssystemen lassen sich aber haufig wenigstens hinreichende oder notwendige Bedingungen fur dynamische Eigenschaften ei nes markierten Netzes formulieren; ei ne linear-algebraische Analyse erlaubt so, Informationen uber das Verhalten eines markierten Netzes zu gewinnen. Zur Uberprufung der Gultigkeit derartiger linear-algebraischer Bedingungen existieren effiziente Algorithmen. Ihre Komplexitat hangt we sentlich davon ab, ob rationale, ganzzahlige oder naturlichzahlige Losungen gesucht werden. Oftmals gibt es einen Trade-off: Alle Losungen haben ei ne Bedeutung, aber die effizienteren Algorithmen haben ei ne geringere Aussage kraft als die komplexeren. Optimierte Routinen fur Matrixoperationen konnen mit proprietaren Analyseverfahren fur Petrinetze kombiniert werden. Das Thema dieser Arbeit ist annahernd so alt wie Petrinetze selbst. Schon Mitte der siebziger Jahre wurden erste einschlagige Arbeiten veroffentlicht. 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 Veroffentlichungen auf eingeschrankte Netzklassen.

Spis treści

1 Einleitung.- 2 Definitionen und elementare Ergebnisse.- 2.1 Ungleichungssysteme.- 2.2 Petrinetze und Markierungen.- 2.3 Schaltfolgen.- 2.4 Die Inzidenzmatrix und die Markierungsgleichung.- 2.5 Markierte Netze und ihre Eigenschaften.- 2.6 Stelleninvarianten.- 2.7 Transitionsinvarianten.- 3 Erreichbarkeit von Markierungen.- 3.1 Entscheidung, Beweis und Widerlegung notwendiger Bedingungen.- 3.2 Lösbarkeit der Markierungsgleichung über ?.- 3.3 Lösbarkeit der Markierungsgleichung über ?.- 3.4 Lösbarkeit der Markierungsgleichung über ?+.- 3.5 Lösbarkeit der Markierungsgleichung über ?.- 3.6 Berechnung von Modulo-Stelleninvarianten.- 4 Fakten.- 4.1 Lineare Prädikate.- 4.2 Implikationen linearer Prädikate.- 4.3 Beweise von Fakten.- 4.4 Lebendigkeit und Verklemmungen.- 5 Fallen und Co-Fallen.- 5.1 Fallen und Erreichbarkeit.- 5.2 Fallen und lineare Prädikate.- 5.3 Co-Fallen.- 6 Ziele.- 6.1 Interne und externe Transitionen.- 6.2 Verifikation von Zielen.- 6.3 Verifikation bedingter Ziele.- 7 Die Rangbedingungen.- 7.1 Starke Schaltfolgen und stark lebendige Markierungen.- 7.2 Eine hinreichende Bedingung für die Existenz stark lebendiger Markierungen.- 7.3 Charakterisierung stark lebendiger Markierungen.- 7.4 Eine notwendige Bedingung für die Lebendigkeit von Markierungen.- 8 Anwendungen von Farkas Lemma.- 8.1 Analyse der Beschränktheit von Stellen.- 8.2 Überdeckbarkeit von Markierungen.- 8.3 Schalthäufigkeiten.- 8.4 Terminierung und Lebendigkeit.- 8.5 Abhängigkeit und Synchronieabstand.- Literatur.- Stichwortverzeichnis.

Blurb

Sehr viele Analyseverfahren für Petrinetze verwenden die Inzidenzmatrix eines Netzes, die eine Verhaltensbeschreibung durch linear-algebraische Verfahren erlaubt. Das Buch gibt eine Einführung in derartige Verfahren und beschreibt vollständig und übersichtlich den State-of-the-art in diesem Bereich. Neben einer neuen systematischen Darstellung bekannter Konzepte runden etliche neue Ergebnisse das Thema ab. Es wird deutlich, daß dynamische Eigenschaften eines netzmodellierten Systems eng zusammenhängen mit der Lösbarkeit bzw. mit Lösungen von Gleichungs- und Ungleichungssystemen.Dabei werden sowohl ganzzahlige als auch rationale Lösungen betrachtet. Eine Differenzierung von Analyse, Verifikation und Beweis führt zu entsprechenden Verfahren, die sich sowohl im Algorithmentyp als auch in ihrer Komplexität unterscheiden. - Zum Verständnis des Buches sind außer Kenntnissen der üblichen mathematischen Terminologie keine Voraussetzungen notwendig. Ein Grundverständnis der Petrinetze ist jedoch hilfreich. Alle im Buch verwendeten Konzepte werden sorgfältig motiviert und mit Hilfe von Beispielen illustriert.