Beachte: Trace-Äquivalenz und Simulationsäquivalenz zu vergleichen macht nur auf Transitionsystemen mit einer einzigen Aktion Sinn, da Traces Aktionen vollkommen ausblenden. Wir verlangen darüberhinaus, dass diese total sind. Auf nicht-totalen gilt der folgende Satz nämlich nicht. Theorem: Sei T = (S, →, I, L) ein totales LTS mit |Act| = 1. Für alle s, t ∈ S gilt: Falls s ' t, dann s ≡tr t. Beweis: Seien s, t gegeben, so dass s ' t. Wir müssen s ≡tr t zeigen, was laut Definition bedeutet, dass Tr (s) = Tr (t) gilt. Es reicht aus, z.B. nur Tr (s) ⊆ Tr (t) zu zeigen. Wir wissen bereits, dass ' eine Äquivalenzrelation, also insbesondere symmetrisch ist. Das bedeutet, dass aus s ' t auch t ' s folgt. Daraus würde dann wiederum mit demselben Beweis der fehlende zweite Teil, also Tr (t) ⊆ Tr (s) folgen. Sei also ρ ∈ Tr (s), d.h. es gibt eine unendliche Folge von Zuständen s0 , s1 , s2 , . . ., so dass si → si+1 für alle i, s0 = s und ρ = L(s0 ), L(s1 ), L(s2 ), . . .. Wir müssen zeigen, dass auch ρ ∈ Tr (t) gilt. Sei t0 = t. Nach Annahme gilt s ' t, also s t und t s. Letzteres brauchen wir in diesem Beweis aber nicht (jedoch in dem weggelassenen, analogen Teil). Ersteres bedeutet, dass es eine Simulationsrelation R gibt, mit (s, t) ∈ R. Daraus folgt insbesondere L(s) = L(t), also L(s0 ) = L(t0 ). Da s0 → s1 und (s0 , t0 ) ∈ R, muss es auch ein t1 geben, so dass t0 → t1 und (s1 , t1 ) ∈ R. Daraus folgt wiederum L(s1 ) = L(t1 ). Außerdem gilt ja s1 → s2 , also muss es auch wiederum ein t2 geben, so dass t1 → t2 und (s2 , t2 ) ∈ R. Dies lässt sich jetzt ins Unendliche fortsetzen, wodurch ein Pfad t0 , t1 , t2 , . . . von t ausgehend konstruiert wird. Außerdem gilt, dass die Beschriftungen der Zustände entlang dieses Pfades dieselben wie die entlang von s0 , s1 , s2 , . . . sind. Somit ist der Trace entlang dieses Pfades auch ρ und es gilt ρ ∈ Tr (t), was zu zeigen war. 2 1