View article

In concurrency theory, there are several examples where the interleaved model of concurrency can distinguish between execution sequences which are not significantly different. One such example is sequences that differ from each other by stuttering, i.e., the number of times a state can adjacently repeat. Another example is executions that differ only by the ordering of independently executed events. Considering these sequences as different is semantically rather meaningless. Nevertheless, specification languages that are based on interleaving semantics, such as linear temporal logic (LTL), can distinguish between them. This situation has led to several attempts to define languages that cannot distinguish between such equivalent sequences. In this paper, we take a different approach to this problem: we develop algorithms for deciding if a property cannot distinguish between equivalent sequences, i. e., is …