6.2.2 Weitere Netzeigenschaften

DTP: Deadlock-Falle-Eigenschaft - deadlock-trap-property

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.7 ab Seite .

SMC: Zustandsmaschinenüberdeckbarkeit - state machine coverable

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.7 ab Seite .

SMD: Zustandsmaschinendekomponierbarkeit - state machine decomposable

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.7 ab Seite .

SMA: Zustandsmaschinenauswählbarkeit - state machine allocatable

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.7 ab Seite .

CPI: Platzinvariantenüberdeckbarkeit - covered by place invariants

Ein Netz ist mit Platzinvarianten überdeckt, wenn es eine P-Invariante gibt, die jedem Platz einen positiven Wert zuweist [Sta90, Definition 11.4 (114)].

CTI: Transitionsinvariantenüberdeckbarkeit - covered by transition invariants

Ein Netz ist mit Transitionsinvarianten überdeckt, wenn es eine T-Invariante gibt, die jeder Transition einen positiven Wert zuweist [Sta90, Definition 11.3 (112)].

B : Beschränktheit - bounded

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)].

SB : Strukturelle Beschränktheit - structurally bounded

Ein Netz ist strukturell beschränkt, wenn es bei jeder Anfangsmarkierung beschränkt ist [Sta90, Bemerkung (116)].

REV: Reversibilität - reversible

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.5.4 auf Seite .

DSt: Erreichbarkeit eines toten Zustandes - dead state reachable

Ein toter Zustand ist erreichbar, wenn ein Zustand erreichbar ist, in dem keine Transition mehr schalten kann [Sta90, Definition 6.1.1 (54)].

BSt: Schlechter Zustand erreichbar - bad state reachable

Falls ein sogenanntes ,,bad`` Prädikat (siehe Kapitel 6.5.4 auf Seite ) durch einen Zustand erfüllt wird, wird dieser bei einer Berechnung eines Zustandsgraphen nicht mehr weiter entwickelt. Bei der Graphanalyse wird in diesem Fall die Eigenschaft BSt gesetzt. Nach dem Verlassen der Graphanalyse wird diese Eigenschaft aber wieder auf ? zurückgesetzt.

DTr: Tote Transition bei Anfangsmarkierung - dead transition at initial marking

Hier wird angezeigt, daß das Netz tote Transitionen bei der Anfangsmarkierung hat, d.h. diese Transitionen sind Fakten.

DCF: Dynamische Konfliktfreiheit - dynamically conflictfree

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)].

L : Lebendigkeit - live

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.5.4 auf Seite .

LV : Lebendigkeit (unter Ignorierung toter Trans.) - live if dead trans. ign.

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.

L&S: Lebendig und Sicher - live and safe

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)].

Lebendigkeit für gefärbte Netze

WL : Schwache Lebendigkeit - weakly live

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.5.4).

CL : Kollektive Lebendigkeit - collectively live

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.5.4). Insbesondere ist jede schwach lebendige Transition auch kollektiv lebendig [Sta90, Folgerung 20.3.2 (229)].