Invariance under stuttering in a temporal logic of actions

Michael Kaminski
Department of Computer Science,
Technion

Abstract

A specification of a concurrent system is said to be invariant under
stuttering if it does not distinguish between a sequence of states and
any sequence resulting from it by replicating some of its states.
Invariance under stuttering, apart of being interesting in its own
right, has applications in reasoning about hierarchically constructed
concurrent systems and model checking via partial order reduction.
Also, this property is important for program specification, because
modularization and refinement are natural features of stuttering.

In our talk, using Ehrenfeucht-Fraisse games on temporal
interpretations, we show that some simple and useful stutter-invariant
properties definable in the language of Lamport's Simple Temporal Logic
of Actions (STLA) are not definable in STLA. Then we present a natural
extension of STLA that allows one to express all stutter-invariant
properties definable in the language of STLA.