What is a bisimulation relation?
It is a a formal way to relate transition systems and states that have the same properties.
R ⊆ S × S′
What is bisimulation equivalence?
It is the most precise
bisimulation relation. In other words, the maximal bisimulation relation is the bisimulation equivalence of that system, also corresponding to the minimized equivalent transition system.
What is a bisimulation quotient?
It is the smallest “reduced”
transition system equivalent to a given one.
It is denoted as M/∼ where
M/∼=(S/∼,→∼,[s0],AP,L∼)
with
S/~ = S/R (the set of equivalence classes)
L′ ([s]) = L(s)
transitions are lifted to equivalence classes:
s → s′
[s] →′ [s′ ]
Initial states:
I′ = {[s] ∣ s′ ∈ I and s′ ∈ [s]}
When is a relation a bisimulation relation? (between two trnasition systems, T1 and T2)
- Each initial state is related to at least another initial state
∀s ∈ I . ∃s′ ∈ I′. (s, s′ ) ∈ R
and
∀s′ ∈ I′ . ∃s ∈ I . (s, s′ ) ∈ R
- Related states have the same labels
(s, s′ ) ∈ R ⇒ L(s) = L(s′ )
- If T and T’ are in related states, then T’ can mimic T
(s, s′ ) ∈ R ⇒ ∀s → t. ∃s′ → t′ . (t, t′ ) ∈ R
- and vice versa
(s, s′ ) ∈ R ⇒ ∀s′ → t′ . ∃s → t. (t, t′ ) ∈ R
When is a relation a bisimulation relation? (For a single transition system)
A relation R ⊆ S × S
is a bisimulation relation iff
1) Related states have the same labels
(s, s′ ) ∈ R ⇒ L(s) = L(s′ )
2) Related states can mimic each other
(s, s′ ) ∈ R ⇒ ∀s → t. ∃s′ → t′ . (t, t′ ) ∈ R
(s, s′ ) ∈ R ⇒ ∀s′ → t′ . ∃s → t. (t, t′ ) ∈ R
How do we denote that two transition systems are bisimilar?
T1 ~ T2
What are the properties of bisimilarity?
Reflexivity
T∼ T
Symmetric
T∼ T′ implies T′ ∼ T
Transitive
T∼ T′ and T′ ∼ T′ ′ implies T∼ T′ ′
Does bisimilarity coincide with anything?
Yes! It coincides with equivalence of CTL* and CTL formulas
