- Source: Stutter bisimulation
In theoretical computer science, a stutter bisimulation is a relationship between two transition systems, abstract machines that model computation. It is defined coinductively and generalizes the idea of bisimulations. A bisimulation matches up the states of a machine such that transitions correspond; a stutter bisimulation allows transitions to be matched to finite path fragments.
Definition
In Principles of Model Checking, Baier and Katoen define a stutter bisimulation for a single transition system and later adapt it to a relation on two transition systems. A stutter bisimulation for
TS
=
(
S
,
Act
,
→
,
I
,
AP
,
L
)
{\displaystyle {\text{TS}}=(S,{\text{Act}},\to ,I,{\text{AP}},L)}
is a binary relation R on S such that for all (s1,s2) in R:
s
1
,
s
2
{\displaystyle s_{1},s_{2}}
have the same labels
If
s
1
→
s
1
′
{\displaystyle s_{1}\to s_{1}'}
is a valid transition and
(
s
1
′
,
s
2
)
∉
R
{\displaystyle (s_{1}',s_{2})\not \in R}
then there exists a finite path fragment
s
2
u
1
⋯
u
n
s
2
′
{\displaystyle s_{2}u_{1}\cdots u_{n}s_{2}'}
(
n
≥
0
{\displaystyle n\geq 0}
) such that each pair
(
s
1
,
u
i
)
{\displaystyle (s_{1},u_{i})}
is in R and
(
s
1
′
,
s
2
′
)
{\displaystyle (s_{1}',s_{2}')}
is in R
If
s
2
→
s
2
′
{\displaystyle s_{2}\to s_{2}'}
is a valid transition and
(
s
1
,
s
2
′
)
∉
R
{\displaystyle (s_{1},s_{2}')\not \in R}
is not then there exists a finite path fragment
s
1
v
1
⋯
v
n
s
1
′
{\displaystyle s_{1}v_{1}\cdots v_{n}s_{1}'}
(
n
≥
0
{\displaystyle n\geq 0}
) such that each pair
(
v
i
,
s
2
)
{\displaystyle (v_{i},s_{2})}
is in R and
(
s
1
′
,
s
2
′
)
{\displaystyle (s_{1}',s_{2}')}
is in R
Generalizations
A generalization, the divergent stutter bisimulation, can be used to simplify the state space of a system with the tradeoff that statements using the linear temporal logic operator "next" may change truth value. A robust stutter bisimulation allows uncertainty over transitions in the system.
