The stuttering principle revisited
| Authors | |
|---|---|
| Year of publication | 2005 |
| Type | Article in Periodical |
| Magazine / Source | Acta informatica |
| MU Faculty or unit | |
| 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: |