In theoretical computer science, stuttering equivalence, a relation written as
π
∼
s
t
π
′
,
can be seen as a partitioning of path
π
and
π
′
into blocks, so that states in the
k
t
h
block of one path are labeled (
L
(
⋅
)
) the same as states in the
k
t
h
block of the other path. Corresponding blocks may have different lengths.
Formally, this can be expressed as two infinite paths
π
=
s
0
,
s
1
,
…
and
π
′
=
r
0
,
r
1
,
…
which are stuttering equivalent (
π
∼
s
t
π
′
) if there are two infinite sequences of integers
0
=
i
0
<
i
1
<
i
2
<
…
and
0
=
j
0
<
j
1
<
j
2
<
…
such that for every block
k
≥
0
holds
L
(
s
i
k
)
=
L
(
s
i
k
+
1
)
=
…
=
L
(
s
i
k
+
1
−
1
)
=
L
(
r
j
k
)
=
L
(
r
j
k
+
1
)
=
…
=
L
(
r
j
k
+
1
−
1
)
.
Stuttering equivalence is not the same as bisimulation, since bisimulation cannot capture the semantics of the 'eventually' (or 'finally') operator found in linear temporal/computation tree logic(branching time logic)(modal logic). So-called branching bisimulation has to be used.
