Lebendige beschränkte EFC-Systeme

Zusammenfassung

Gegenstand dieses Teils ist die strukturelle Charakterisierung lebendig und beschränkt markierter EFC-Systeme. Wir werden dafür zunächst die Klasse wohlgeformter EFC-Netze charakterisieren und anschließend eine Charakterisierung der lebendigen und beschränkten Markierungen eines wohlgeformten EFC-Netzes angeben. Beide Charakterisierungen sind mit polynomiellem Zeitaufwand in der Netzgröße überprüfbar. Zusammen erhalten wir einen effizienten Algorithmus zur Entscheidung der Klasse lebendiger und beschränkter EFC-Systeme:

• (i) Überprüfe die EFC-Eigenschaft des Netzes.

  Dies ist leicht mit polynomiellem Aufwand möglich.

• (ii) Entscheide, ob das Netz wohlgeformt ist.

  Die Ergebnisse dieses Teils liefern eine Charakterisierung, die mit polynomiellem Aufwand überprüft werden kann.

• (iii) Entscheide, ob die Markierung lebendig und beschränkt ist.

  Wir zeigen, daß jede Markierung eines wohlgeformten EFC-Netzes be-schränkt ist und daß eine Markierung eines wohlgeformten EFC-Netzes genau dann lebendig ist, wenn sie jeden nichtleeren Deadlock markiert. Diese Bedingung ist mit polynomiellem Aufwand überprüfbar.