Invariance Under Stuttering in a Temporal Logic without the "Until" Operator

Abstract

We show that a stutter-invariant property is expressible in propositional temporal logic without the "until" operator if and only if it is expressible in the Generalized Temporal Logic of Actions.