Bisimulation

In theoretical computer science , a bis-simulation is a relation between the states of a transition system that relates those states that behave in the same way . This means that one state can simulate the transitions of the other and vice versa.

Clearly speaking, two states are bisimilar if their possible traits match. In this sense they cannot be distinguished from one another by an outside observer.

Formal definition

An edge-labeled transition system (S, Λ, →) is given. A bisimulation is a binary relation R over S (i.e. R ⊆ S × S) with:

For every pair of states p, q ∈ S: If (p, q) ∈ R, then for all α ∈ Λ: If there is a p '∈ S with

${\displaystyle p\longrightarrow ^{\alpha }p',}$

so there is a q '∈ S with

${\displaystyle q\longrightarrow ^{\alpha }q'}$

and (p ', q') ∈ R. Analogously, for every q '∈ S with

${\displaystyle q\longrightarrow ^{\alpha }q'}$

a p '∈ S with

${\displaystyle p\longrightarrow ^{\alpha }p'}$

and (p ', q') ∈ R.

Equivalent to this is: Both R and R ⁻¹ are simulation quasi-orders .

Given two states p and q in S, then p is bisimilar to q, written p ~ q, if there is a bisimulation R with (p, q) ∈ R.

The bisimilarity relation ~ is an equivalence relation. It is also the largest bis-simulation over a given transition system.

Variants of bisimulations

In special situations, the concept of bis-simulation is sometimes refined by adding further conditions. Does the transition system contain e.g. B. a silent transition , often characterized by τ, i.e. a transition that is not visible to an outside observer, then the bisimulation can be weakened to a weak bisimulation that ignores silent transitions.