Stuttering equivalence

In theoretical computer science, stuttering equivalence, a relation written as

π

∼

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.