Automata and temporal logic over arbitrary linear time

TL;DR

This paper explores the relationship between linear temporal logic and automata on arbitrary linear orderings, providing a doubly exponential procedure to decide satisfiability for formulas with advanced connectives.

Contribution

It introduces a doubly exponential algorithm to convert LTL formulas with complex connectives into automata over arbitrary linear orderings, enabling satisfiability checking.

Findings

Automata construction for LTL with advanced connectives is decidable.

The transformation from formulas to automata is doubly exponential in complexity.

Decidability of the emptiness problem leads to a decision procedure for satisfiability.

Abstract

Linear temporal logic was introduced in order to reason about reactive systems. It is often considered with respect to infinite words, to specify the behaviour of long-running systems. One can consider more general models for linear time, using words indexed by arbitrary linear orderings. We investigate the connections between temporal logic and automata on linear orderings, as introduced by Bruy\`ere and Carton. We provide a doubly exponential procedure to compute from any LTL formula with Until, Since, and the Stavi connectives an automaton that decides whether that formula holds on the input word. In particular, since the emptiness problem for these automata is decidable, this transformation gives a decision procedure for the satisfiability of the logic.