weak bisimulation

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

  1. 1.

    Let be the reflexiveMathworldPlanetmathPlanetmath and transitive closuresMathworldPlanetmathPlanetmath of τ. In other words, pq 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. 2.

    Next, for any label α that is not the silent step τ in Σ, define


    where denotes the relational compositionPlanetmathPlanetmath operationMathworldPlanetmath. In other words, pαq iff there are states r and s such that pαr, rs, and sαq.

  3. 3.

    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 pq and any labelled transition pα1p, there is a state qS2 such that pq and p(α)2q. is a weak bisimulation if both and its converseMathworldPlanetmath -1 are weak simulations.

Title weak bisimulation
Canonical name WeakBisimulation
Date of creation 2013-03-22 19:30:55
Last modified on 2013-03-22 19:30:55
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 10
Author CWoo (3771)
Entry type Definition
Classification msc 68Q85
Synonym invisible step
Defines silent step
Defines weak simulation