Generalized Deterministic Languages and their Automata: A Characterization of Restricted Temporal Logic
Heinz Schmitz · 2007
Let TLXF TLF be the class of formulas of temporal logic, where as the only tem-poral operatorsX (next) andF (eventually) are allowed (onlyF is allowed, resp.). For a class TLXF let L be the class of -definable languages. Among others, characteri-zations of LTLXF and LTLF in terms of forbidden patterns in finite automata are known. Here we ask for every bound k on the number of nested uses of the next operator for the expressive power of the respective fragment of TLXF. Denote by TLXkF the class of formulas in TLXF with nesting depth k in the next operator. Obviously,