Technical Reports

The report FIMU-RS-2004-04

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.