Effective Characterizations of Simple Fragments of Temporal Logic Using Carton--Michel Automata

We present a framework for obtaining effective characterizations of simplefragments of future temporal logic (LTL) with the natural numbers as timedomain. The framework is based on a form of strongly unambiguous automata, alsoknown as prophetic automata or complete unambiguous B\"uchi automata andreferred to as Carton-Michel automata in this paper. These automata enjoystrong structural properties, in particular, they separate the "finitaryfraction" of a regular language of infinite words from its "infinitaryfraction" in a natural fashion. Within our framework, we providecharacterizations of several natural fragments of temporal logic, where, insome cases, no effective characterization had been known previously, and givelower and upper bounds for their computational complexity.Comment: 22 pages, to appear in LMCS Special Issue: Selected papers of the conference on "Foundations of Software Science and Computation Structures": FOSSACS 201