An Alternating Automaton for First-Order Linear Temporal Logic--Tech Report

TL;DR

This paper introduces an automata-based method for representing LTL-FO+ properties, extending linear temporal logic with first-order quantification, enabling easier manipulation and analysis of complex temporal properties.

Contribution

It provides a finite automata representation for LTL-FO+ formulas with linear state complexity, enhancing the expressiveness and manipulability of temporal logic properties.

Findings

Automata representation has finite size regardless of variable domain.

Number of automata states is linear in property size.

Facilitates easier negation and emptiness checking.

Abstract

In this paper we give automata-based representation of LTL-FO$^+$ properties. LTL-FO$^+$ is an extension of LTL that includes first-order quantification over bounded variable, thus greatly increasing the expressivity of the language. An automata representation of this formalism allows greater ease in writing and understanding properties, as well as in performing manipulations, such as negation or emptiness checking. The automata representation of an LTL-FO$^+$ formula has finite size regardless of the domain of quantified variables, and the number of states that is linear in the size of the property.