Title: Characterization and Verification of Stuttering Equivalence
Abstract: 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.
Publication Year: 2018
Publication Date: 2018-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot