An Effective Characterization of Properties Definable by LTL Formulae with a Bounded Nesting Depth of the Next-Time Operator
by
Antonín Kučera,
Jan Strejček,
May 2004, 11 pages.
FIMU-RS-2004-04.
Available as Postscript,
PDF.
Abstract:
It is known that an LTL property is expressible by an LTL formula
without any next-time operator if and only if the property is
stutter invariant. It is also known that the problem whether a
given LTL property is stutter invariant is PSPACE-complete. We
extend these results to fragments of LTL obtained by restricting the
nesting depth of the next-time operator to a given n.
Some interesting facts about the logic LTL follow as simple
corollaries.