The stuttering principle revisited

It is known that LTL formulae without the ‘next’ operator are invariant under the so-called stutter equivalence of words. In this paper we extend this principle to general LTL formulae with given nesting depths of both ‘next’ and ‘until’ operators. This allows us to prove the semantical strictness of three natural hierarchies of LTL formulae, which are parametrized either by the nesting depth of just one of the two operators, or by both of them. Further, we provide an effective characterization of languages definable by LTL formulae with a bounded nesting depth of the ‘next’ operator.This paper is a revised and extended version of 6].