Generalized stuttering equivalence

Two sequences are stuttering equivalent when they differ only by the number of consecutive repetition of elements. Specification of concurrent systems are often closed under stuttering. A qualitative argument for using stuttering closed specifications is that they are robust to same implementation changes such as using processes with different granularity of instructions. Perhaps more importantly, such specifications allow the benefit of using compositional verification and partial order reduction. In this paper we generalize the definition of stuttering equivalence. We consider alphabets that can be partitioned into several components, e.g., one alphabet for the local memory of each process, and one alphabet for each shared memory unit. We define the projections of each execution over some subsets of these components, e.g., the projection. over the local memory of a process and the set of shared memories it can access. Generalized stuttering equivalence relates sequences such that their various projections are stuttering equivalent.