weak bisimulation (original) (raw)

Let M=(S,Σ,→) be a labelled state transition system (LTS). Recall that for each label α∈Σ, there is an associated binary relation →α on S. Single out a label τ∈Σ, and call it the silent step. Define the following relations:

1. 1. Let ⇒ be the reflexive and transitive closures of →τ. In other words, p⇒q iff either p=q, or there is a positive integer n>1 and states r1,…,rn such that p=r1 and q=rn and ri→τri+1, where i=1,…,n-1.
2. 1. Next, for any label α that is not the silent step τ in Σ, define
      where ∘ denotes the relational composition operation. In other words, p⇒αq iff there are states r and s such that p→αr, r⇒s, and s→αq.
3. 1. Finally, for any label α∈Σ, let

      ⇒(α):={⇒if ⁢α=τ⇒αotherwise.

Definition. Let M=(S1,Σ,→1) and N=(S2,Σ,→2) be two labelled state transition systems, with τ∈Σ the silent step. A relation ≈⊆S1×S2 is called a weak simulation if whenever p≈q and any labelled transition p→α1p′, there is a state q′∈S2 such that p′≈q′ and p′⇒(α)2q. ≈ is a weak bisimulation if both ≈ and its converse ≈-1 are weak simulations.