First-order linear temporal logic (FOLTL) is a flexible and expressive formalism capable of naturally describing complex behaviors and properties. Although the logic is in general highly undecidable, the idea of using it as a specification language for the verification of complex infinite-state systems is appealing. However, a missing piece, which has proved to be an invaluable tool in dealing with other temporal logics, is an automaton model capable of capturing the logic. In this paper we address this issue, by defining and studying such a model, which we call first-order automaton. We define this very general class of automata, and the corresponding notion of regular first-order language, showing their closure under most common language-theoretic operations. We show how they can capture any FOLTL formula over any signature and theory, and provide sufficient conditions for the semi-decidability of their non-emptiness problem. Then, to show the usefulness of the formalism, we prove the decidability of monodic FOLTL, a classic result known in the literature, with a simpler and direct proof.

翻译：一阶线性时序逻辑是一种灵活且富有表达力的形式化方法，能够自然地描述复杂行为与性质。尽管该逻辑通常具有高度不可判定性，但将其用作验证复杂无限状态系统的规约语言这一思路仍颇具吸引力。然而，当前尚缺一种能够刻画该逻辑的自动机模型——这类模型在处理其他时序逻辑时已被证明是不可或缺的工具。本文通过定义并研究一种称为一阶自动机的新模型来解决这一问题。我们定义了这类非常通用的自动机类别及其对应的一阶正则语言概念，证明了它们在大多数常见语言理论运算下的封闭性。我们展示了该模型如何能够刻画任意签名和理论上的所有一阶线性时序逻辑公式，并为其非空性问题的半可判定性提供了充分条件。最后，为说明该形式化方法的实用性，我们以更简洁直接的方式证明了文献中已知的经典结果——单子一阶线性时序逻辑的可判定性。