Next: 6.3 Analysemenü und Voranalyse
Up: 6.2 Analysestatus
Previous: 6.2.1 Elementare Netzeigenschaften
Unterabschnitte
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)].
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)].
Next: 6.3 Analysemenü und Voranalyse
Up: 6.2 Analysestatus
Previous: 6.2.1 Elementare Netzeigenschaften
© 1996-98 Prof. Peter H. Starke (starke@informatik.hu-berlin.de) und Stephan Roch (roch@...)
INA Handbuch Version 2.1 zuletzt geändert: 1998-03-24