Ein Netz erfüllt die Deadlock-Falle-Eigenschaft, wenn die maximale Falle in jedem minimalen Deadlock ausreichend markiert ist [Sta90, Kapitel 15 (162-175),]. Eine Falle ist eine Menge von Plätzen, die nicht sauber werden kann, wenn sie Marken enthält, weil jede Transition, die Marken von einem Platz dieser Menge entfernt, einen Nachplatz in dieser Menge hat, also Marken in diese Menge zurückgibt. Die leere Menge ist also eine Falle. Eine Falle ist maximal, wenn sie nicht eine echte Teilmenge einer Falle ist. Ein Deadlock ist eine nichtleere Menge von Plätzen, die nicht wieder markiert werden kann, wenn sie einmal sauber ist, weil jede Transition, die Marken auf einen Platz aus dieser Menge schalten würde, einen Vorplatz in dieser Menge hat (also nicht schalten kann). Ein Deadlock ist minimal, wenn er keinen Deadlock echt enthält. Eine Platzmenge ist ausreichend markiert, wenn sie einen Platz enthält, der genügend Marken enthält, um alle seine Nachtransitionen zu konzessionieren.
Weiteres finden Sie im Kapitel 6.6 ab Seite
.
Eine Komponente eines Netzes ist eine Platzmenge, die Deadlock und Falle zugleich ist. Durch diese Platzmenge wird ein Teilnetz mit diesen Plätzen und den anhängenden Transitionen bestimmt. Ist eine Reihe von Komponenten gegeben, die als Teilnetze Zustandsmaschinen bestimmen und ihre Vereinigung ist gleich der Platzmenge des Netzes, so wird dieses Netz zustandsmaschinenüberdeckbar genannt [Sta90, Definition 16.2.2 (180),].
Weiteres finden Sie im Kapitel 6.6 ab Seite
.
Ist eine Reihe von Komponenten gegeben, die als Teilnetze stark zusammenhängende Zustandsmaschinen bestimmen und ihre Vereinigung ist gleich der Platzmenge des Netzes, so wird dieses Netz zustandsmaschinendekomponierbar genannt [Sta90, Definition 16.2.3. (180),].
Weiteres finden Sie im Kapitel 6.6 ab Seite
.
In einem zustandsmaschinendekomponierbaren Netz hat jede Transition einen Vorplatz; eine Vorplatzauswahl ist eine Abbildung, die jeder Transition einen ihrer Vorplätze zuordnet. Eine Komponente heißt ausgewählt bei einer Vorplatzauswahl, wenn diese allen Transitionen, die einen Vorplatz in der Komponente haben, einen Vorplatz aus der Komponente zuordnet. Das Netz wird zustandsmaschinenauswählbar genannt, wenn jede Vorplatzauswahl eine stark zusammenhängende Zustandsmaschinenkomponente auswählt [Sta90, Definition 16.3 (182),]
Weiteres finden Sie im Kapitel 6.6 ab Seite
.
Ein Netz ist mit Platzinvarianten überdeckt, wenn es eine P-Invariante gibt, die jedem Platz einen positiven Wert zuweist [Sta90, Definition 11.4 (114),].
Ein Netz ist mit Transitionsinvarianten überdeckt, wenn es eine T-Invariante gibt, die jeder Transition einen positiven Wert zuweist [Sta90, Definition 11.3 (112),].
Ein Netz ist beschränkt, wenn es eine Zahl k so gibt, daß bei keiner erreichbaren Markierung auf einem Platz mehr als k Marken liegen [Sta90, Definition 14.1 (38),].
Ein Netz ist strukturell beschränkt, wenn es bei jeder Anfangsmarkierung beschränkt ist [Sta90, Bemerkung (116),].
Ein Netz ist reversibel (rücksetzbar), wenn von jedem erreichbaren Zustand der Anfangszustand erreicht werden kann [Sta90, Definition 6.2 (59),].
Eine Beschreibung des Rücksetzbarkeitstests finden Sie im Kapitel
6.4.4 auf Seite .
Ein toter Zustand ist erreichbar, wenn ein Zustand erreichbar ist, in dem keine Transition mehr schalten kann [Sta90, Definition 6.1.1 (54),].
Hier wird angezeigt, daß das Netz tote Transitionen bei der Anfangsmarkierung hat, d.h. diese Transitionen sind Fakten.
Ein Netz heißt dynamisch konfliktfrei, wenn kein Zustand erreichbar ist, bei dem zwei Transitionen schalten können und die eine durch das Schalten der anderen die Konzession verliert [Sta90, Definition 3.4.3 (35),].
Ein Netz ist lebendig, wenn alle seine Transitionen bei der Anfangsmarkierung lebendig sind, d.h. kein Zustand erreichbar ist, bei dem eine Transition tot ist. Fakten werden dabei ignoriert [Sta90, Definition 6.1.5 (55),].
Eine Beschreibung des Lebendigkeitstests finden Sie im Kapitel 6.4.4
auf Seite .
Ein Netz ist lebendig unter Ignorierung toter Transitionen, wenn alle seine Transitionen, die nicht schon bei der Anfangsmarkierung tot sind, lebendig sind. Die dabei ignorierten Transitionen können als nicht gekennzeichnete Fakten betrachtet werden.
Ein Netz ist lebendig und sicher, wenn es lebendig ist und bei keiner erreichbaren Markierung mehr als eine Marke auf einem Platz liegt [Sta90, Definition 4.1 (39),].
Ein gefärbtes Netz ist schwach lebendig, wenn alle Transitionen schwach
lebendig sind, d.h. alle Transitionen sind in der Anfangsmarkierung bei
einer Farbe lebendig [Sta90, Definition 20.6.1 (228),] (siehe auch
Seite im Kapitel 6.4.4).
Ein gefärbtes Netz ist kollektiv lebendig, wenn alle Transitionen kollektiv
lebendig sind. Eine Transition ist kollektiv lebendig, wenn es für jeden
erreichbaren Zustand eine Farbe gibt, so daß die Transition in dieser Farbe
in einem von dieser Markierung erreichbaren Zustand schalten kann
[Sta90, Definition 20.6.2 (228),] (siehe auch Seite
im Kapitel 6.4.4).
Insbesondere ist jede schwach lebendige Transition auch kollektiv lebendig
[Sta90, Folgerung 20.3.2 (229),].
Zuletzt geändert am: Thu Apr 10 15:08:18 MET DST 1997