Effective characterizations of simple fragments of temporal logic using prophetic automata

Abstract

We present a framework for obtaining effective characterizations of simple fragments of future temporal logic (LTL) with the natural numbers as time domain. The framework is based on prophetic automata (also known as complete unambiguous Büchi automata), which enjoy strong structural properties, in particular, they separate the "finitary fraction" of a regular language of infinite words from its "infinitary fraction" in a natural fashion. Within our framework, we provide characterizations of all natural fragments of temporal logic, where, in some cases, no effective characterization had been known previously, and give lower and upper bounds for their computational complexity. © 2012 Springer-Verlag Berlin Heidelberg.