In theoretical computer science , stuttering equivalence ,[ 1] a relation written as
The paths
π π -->
{\displaystyle \pi }
and
π π -->
′
{\displaystyle \pi '}
are stuttering equivalent.
π π -->
∼ ∼ -->
s
t
π π -->
′
{\displaystyle \pi \sim _{st}\pi '}
,
can be seen as a partitioning of paths
π π -->
{\displaystyle \pi }
and
π π -->
′
{\displaystyle \pi '}
into blocks, so that states in the
k
t
h
{\displaystyle k^{\mathrm {th} }}
block of one path are labeled (
L
(
⋅ ⋅ -->
)
{\displaystyle L(\cdot )}
) the same as states in the
k
t
h
{\displaystyle k^{\mathrm {th} }}
block of the other path. Corresponding blocks may have different lengths.
Formally, this can be expressed as two infinite paths
π π -->
=
s
0
,
s
1
,
… … -->
{\displaystyle \pi =s_{0},s_{1},\ldots }
and
π π -->
′
=
r
0
,
r
1
,
… … -->
{\displaystyle \pi '=r_{0},r_{1},\ldots }
being stuttering equivalent (
π π -->
∼ ∼ -->
s
t
π π -->
′
{\displaystyle \pi \sim _{st}\pi '}
) if there are two infinite sequences of integers
0
=
i
0
<
i
1
<
i
2
<
… … -->
{\displaystyle 0=i_{0}<i_{1}<i_{2}<\ldots }
and
0
=
j
0
<
j
1
<
j
2
<
… … -->
{\displaystyle 0=j_{0}<j_{1}<j_{2}<\ldots }
such that for every block
k
≥ ≥ -->
0
{\displaystyle k\geq 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
)
{\displaystyle L(s_{i_{k}})=L(s_{i_{k}+1})=\ldots =L(s_{i_{k+1}-1})=L(r_{j_{k}})=L(r_{j_{k}+1})=\ldots =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.[citation needed ]
References