I would like to proof transitivity of simulation in Kripke Structures.
Proof Sketch:
Let A, B, C be Kripke Structures, with A=(Sa,S0a,Ra,AP,La) B=(Sb,S0b,Rb,AP,Lb) C=(Sc,S0c,Rc,AP,Lc)
H ⊆ S × S′ is simulation relation between M and M′ iff for every (s, s′) ∈ H: s and s′ satisfy the same propositions For every successor t such that (s, t) ∈ R, there is a corresponding successor t such that(s’,t’) ∈ R’ and(t,t’)∈H For every initial state s ∈ S0 there is a corresponding initial state s′ ∈ S′0 such that (s, s′) ∈ H
Let R be the simulation relation (A is simulated by B), show that A R B ^ B R C => A R C
Assume A R B, by definition A and B satisfy the same propositions, then for each transition (sa,ta) ∈ Ra, there is a corresponding state (sb,tb) ∈ Rb and for each initial state sa ∈ S0a, there is an initial state sb ∈ S0b.
Assume B R C, by definition A and B satisfy the same propositions, then for each transition (sb,tb) ∈ Ra, there is a corresponding state (sc,tc) ∈ Rb and for each initial state sb ∈ S0b, there is an initial state sc ∈ S0c.
Then continue by contraposition, but I don't know how to proceed. Any hints are appreciated.