-Kann mir einer Sagen, warum man bei der Lebendigkeits-Invarianzeigenschaft nur die Terminalen SZKs untersucht?
Die Lebendigkeitsinvarianz sagt ja aus, dass jede Markierung (d.h. Knoten) m1 des Erreichbarkeitsgraphen RS(N, m0) einen weiteren Knoten m2 in seinem Erreichbarkeitsgraphen RS(N, m1) enthält, für den das Markierungsprädikat \PI(m2) gilt.
Die Markierung m1 kann nun in einer terminalen oder nicht-terminalen SZK liegen.
Wenn sich nun m1 in einer terminalen SZK befindet, muss sich m2 ja auch darin befinden; m2 kann nicht in eine anderen SZK sich befinden. Das besondere an den terminalen SZKs ist, dass es keinen Pfad gibt, um diese SZK zu verlassen: Eine Markierung ist quasi gefangen. Also suchen wir in diesem Fall nur in einer terminalen SZK nach einer Markierungen, die \PI() erfüllt.
Wenn m1 nicht in einer terminalen SZK liegt (sondern in einer ``normalen'' SZK), dann gibt es entweder in dieser nicht-terminalen SZK ein m2, dass \PI(m2) wahr macht, oder man gelangt von m1 durch einen Pfad in eine terminale SZK (nennen wir diese mal tszk1) - ansonsten wäre m1 ja schon Bestandteil einer terminalen SZK [img]
http://www.fb18.de/gfx/22.gif[/img]. In tszk1 muss es aber einen Knoten m2 geben, der \PI(m2) erfüllt, um die Lebendigkeitsinvarianzeigenschaft zu erfüllen. Auch hier suchen wir nur in einer terminalen SZK nach einer Markierung, die \PI() wahr macht.
Kurz gesagt: Man sucht nur in terminalen SZK, weil es in diesen Markierungen geben muss, die \PI() erfüllen (ansonsten nicht lebendig) - aus terminalen SZKs kommt man halt nicht heraus.
Zumindest habe ich das so verstanden…
Wie kann man das Zurücksetzzustand anhand der Terminalen überprüfen?
Um zu prüfen, ob man von jeder Markierung in den Rücksetzzustand m0 gelangen kann, muss man gucken, ob jede terminale SZK m0 enthält - es darf also nur eine einzige SZK geben. (Seite 144 im Skript)
