races ■ 1,L2 ¨,1 s a pat th in a labeled transition system, the sequence of actions trace(c)=n(t1) n(t2). is called the trace of the path
Traces ◼ If c = 𝑡1 , 𝑡2 ⋯ , is a path in a labeled transition system, the sequence of actions trace(c) = 𝜆(𝑡1 ), 𝜆(𝑡2 ) ⋯ is called the trace of the path
Relation A relation RsX XX is an equivalence(relation) if and only if Reflexive: for all x∈x:(x,x)∈R Symmetric: for allx,y EX: if(X,y)ER, then(y, x) ∈R Transitive: for allx,y,z∈ⅹ:if(x,y)∈Rand(y,z) ∈ R then(x,z)∈R
Relation ◼ A relation R ⊆ X × X is an equivalence (relation) if and only if ◼ Reflexive: for all x ∈ X : (x, x) ∈ R ◼ Symmetric: for all x, y ∈ X : if (x, y) ∈ R, then (y, x) ∈ R ◼ Transitive: for all x, y, z ∈ X : if (x, y) ∈ R and (y, z) ∈ R then (x, z) ∈ R
There are numerous notions of equivalency for transition systems We consider the following o Strong isomorphism o Weak isomorphism o Bisimulation equivalence Bisimulation Equivalence Weak Isomorphism Equivalence Strong Isomorphism Equivalence
◼ There are numerous notions of equivalency for transition systems ◼ We consider the following: Strong isomorphism Weak isomorphism Bisimulation equivalence
W Transition system homomorphiSm Definition: Let A=<S, So, T,a, B>and A'=< S,So,T,a,B> be two transition systems. A homomorphism h from a to cA is a pair (ha, hr of mappings hx:S→S h-:T→T which satisfies, for every transition t of T' a'(hr(t))=ha(a(t)), BChr(t))=ho(B(t))
Transition system homomorphism ◼ Definition:Let 𝒜= < 𝑆, 𝑆0 , 𝑇, 𝛼, 𝛽 > and 𝒜’ = < 𝑆′ , 𝑆′ 0 ,𝑇′ , 𝛼′ , 𝛽′ > be two transition systems. A homomorphism h from 𝒜 to 𝒜’ is a pair (ℎ𝜎, ℎ𝜏 )of mappings ℎ𝜎: 𝑆 → 𝑆′ ℎ𝜏 :𝑇 → 𝑇′ which satisfies, for every transition t of T: 𝛼′(ℎ𝜏 (𝑡)) = ℎ𝜎 𝛼 𝑡 , 𝛽′(ℎ𝜏 (𝑡)) = ℎ𝜎 𝛽 𝑡
Labeled transition system homomorphism Let cA=<S,So, T,a, B,n>and cA=< S,S′o,T,a,B’,4> be two transition systems labeled by the same alphabet. A labeled transition system homomorphism from a to A'is a homomorphism h which also satisfies the condition (hx(t)=(t)
◼ Labeled transition system homomorphism ◼ Let 𝒜= < 𝑆, 𝑆0 ,𝑇, 𝛼,𝛽, 𝜆 > and 𝒜’ = < 𝑆′, 𝑆′0 ,𝑇′, 𝛼′ , 𝛽′ , 𝜆 ′ >be two transition systems labeled by the same alphabet. A labeled transition system homomorphism from 𝒜 to 𝒜’ is a homomorphism h which also satisfies the condition 𝜆′(ℎ𝜏 (𝑡)) = 𝜆(𝑡)