LTL Semantic Tableaux and Alternating $\omega$-automata via Linear Factors

TL;DR

This paper introduces a novel approach to LTL verification by analyzing linear factors, connecting automata construction and semantic tableaux, and extending concepts from regular expressions to temporal logic.

Contribution

It establishes the concept of linear factors for LTL, linking automata and tableau methods, and provides foundational properties like expansion and finiteness.

Findings

Linear factors for LTL are effectively defined and verified.

Connections between automata construction and semantic tableaux are clarified.

New insights into LTL verification methods are provided.

Abstract

Linear Temporal Logic (LTL) is a widely used specification framework for linear time properties of systems. The standard approach for verifying such properties is by transforming LTL formulae to suitable $\omega$-automata and then applying model checking. We revisit Vardi's transformation of an LTL formula to an alternating $\omega$-automaton and Wolper's LTL tableau method for satisfiability checking. We observe that both constructions effectively rely on a decomposition of formulae into linear factors. Linear factors have been introduced previously by Antimirov in the context of regular expressions. We establish the notion of linear factors for LTL and verify essential properties such as expansion and finiteness. Our results shed new insights on the connection between the construction of alternating $\omega$-automata and semantic tableaux.