TU Braunschweig

Symbolfoto

Müller, J. R.:
Dualität und Analyse von Formalen Modellen - Prädikat/Transitions-Netze und ihr Bezug zur Linearen Algebra.
Dissertation, Universität Koblenz-Landau, 2004.

Kurzfassung:

Gegenstand dieser Arbeit ist die Dualität und Analyse von höheren Petri-Netzen. Für (niedrige) Stellen/Transitions-Netze ist der Bezug zur linearen Algebra gut bekannt, so dass für diese Netzklasse strukturelle Analyseverfahren existieren und zu (primalen) Netzen auf einfache Weise die dualen berechnet werden können.

In dieser Dissertation wird gezeigt, dass man Kantenanschriften in höheren Netzen (wir beschränken uns bei unseren Betrachtungen exemplarisch auf Prädikat/Transitions- Netze (Pr/T-Netze)) als lineare Abbildungen in Tupelschreibweise auffassen kann. Durch diese Verankerung von Pr/T-Netzen mit der Theorie der linearen Algebra ist es möglich, auch für höhere Netze sowohl strukturelle Analyseverfahren auszuarbeiten als auch zu primalen Netzen die dualen zu bestimmen.

Von "struktureller" Analyse sprechen wir, wenn lediglich der Netzgraph zur Herleitung von Netzeigenschaften herangezogen wird – Markierungen fließen nicht in die strukturelle Analyse ein. Das bedeutet, dass mittels struktureller Eigenschaften unabhängig von konkreten Markierungen Aussagen über dynamische Netzeigenschaften gemacht werden können. Invarianten, Traps und CoTraps (auch bekannt unter "Deadlocks" oder "Siphons") bilden das Herzstück solcher Analyseverfahren. Im Wesentlichen handelt es sich bei diesen Konzepten um Lösungen nicht-negativer, ganzzahliger und homogener Gleichungssysteme. In dieser Arbeit stellen wir Algorithmen vor, durch die wenigstens eine Teilmenge aller Lösungen berechnet und mittels "variabler Vektoren" kompakt dargestellt werden können.

Wenn man in einem (primalen) Petri-Netz die Richtung aller Kanten wechselt und Stellen und Transitionen vertauscht, erhält man als Resultat wieder ein Netz, das als "duales Netz" bezeichnet wird. Dieses Dualisieren der Struktur wirft im Kontext höherer Petri-Netze die Frage auf, wie Kantenanschriften zu behandeln sind. Unter Rückgriff auf die Dualraumtheorie der linearen Algebra wird in dieser Arbeit gezeigt, dass zu linearen Abbildungen an Kanten eines primalen Netzes, im dualen Netz die jeweils adjungierten gebildet werden müssen.

Zu einer sinnvollen Dualisierung des Verhaltens kommt man, indem man nicht nur Netze, sondern auch die Markierung dualisiert, d.h. aus markierten Stellen im primalen Netz werden im dualen Netz markierte Transitionen. Um nicht lediglich eine neue Interpretation der Netzdynamik zu erhalten, sondern tatsächlich eine neue Dynamik entstehen zu lassen, erlauben wir beide Tokensorten im gleichen Netz und erweitern die Schaltregeln derart, dass beide Knotensorten schalten können.


http://www.iva.ing.tu-bs.de?iT=27_815&id_select=571