Stuttering Equivalence

Stephan Merz 1
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Two omega-sequences are stuttering equivalent if they differ only by finite repetitions of elements. Stuttering equivalence is a fundamental concept in the theory of concurrent and distributed systems. Notably, Lamport argues that refinement notions for such systems should be insensitive to finite stuttering. Peled and Wilke show that all LTL (linear-time temporal logic) properties that are insensitive to stuttering equivalence can be expressed without the next-time operator. Stuttering equivalence is also important for certain verification techniques such as partial-order reduction for model checking. We formalize stuttering equivalence in Isabelle/HOL. Our development relies on the notion of a stuttering sampling function that identifies blocks of identical sequence elements.
Type de document :
Rapport
[Research Report] 2012
Liste complète des métadonnées

https://hal.inria.fr/hal-00760690
Contributeur : Stephan Merz <>
Soumis le : mardi 4 décembre 2012 - 11:43:19
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13

Identifiants

  • HAL Id : hal-00760690, version 1

Collections

Citation

Stephan Merz. Stuttering Equivalence. [Research Report] 2012. 〈hal-00760690〉

Partager

Métriques

Consultations de la notice

155