Spur/Ablehnungs-Semantik

Spur:

• Ein-Schritt-Relation: ...
• Mehr-Schritt-Relation: ...

Ablehnung:

• P∈Proc(Σ) heißt stabil, wenn ¬∃Q∈Proc(Σ) : PQ
• stabiler P∈Proc(Σ) lehnt A⊆Σ ab,

  wenn ¬∃a∈A, Q∈Proc(Σ) : PQ

Ablehnungs-Semantik rej(P) Menge aller Paare von Spur und Ablehnungsmenge am Ende der jeweiligen Spur.