The stuttering principle revisited

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

KUČERA Antonín STREJČEK Jan

Year of publication 2005
Type Article in Periodical
Magazine / Source Acta informatica
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords linear temporal logic; stuttering
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.