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

TL;DR

This paper introduces a framework using Carton-Michel automata to effectively characterize simple fragments of future temporal logic, providing new insights and bounds for their computational complexity.

Contribution

The paper develops a novel automata-based framework for characterizing temporal logic fragments, including cases with previously unknown effective characterizations.

Findings

Effective characterizations for several temporal logic fragments.

Lower and upper bounds for computational complexity.

Structural properties of Carton-Michel automata facilitate separation of language fractions.

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 a form of strongly unambiguous automata, also known as prophetic automata or complete unambiguous B\"uchi automata and referred to as Carton-Michel automata in this paper. These automata 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 several 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.