Characterization and Verification of Stuttering Equivalence

Stuttering equivalence is an important equivalence relation on Kripke structures. It is the equivalence which preserves all CTL*-X properties. Two key issues concerning this equivalence are how to characterize it and how to verify whether two given states are equivalent with respect to it. For this purpose, we propose two bisimulation style definitions, one called \(\omega \)-bisimulation which provides a concise characterization of the equality and one called stuttering bisimulation with induction which provides a verification method for establishing the equality. We also show that stuttering bisimulation with induction coincides with well-founded bisimulation, a notion introduced by Namjoshi for verifying stuttering equivalence.