← 研踪 PaperTrailarXiv:2405.20057 · v2
A General Automata Model for First-Order Temporal Logics (Extended Version)
首次提交 2024-05-30 21:45
版本更新 2026-11-10 20:23
雷达观测 2026-11-11 13:08
摘要
First-order linear temporal logic (FO-LTL) 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 (of finite words), showing their closure under most language-theoretic operations. We show how they can capture any FO-LTL formula over finite words, 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 FO-LTL, a classic result known in the literature, with a simpler and direct proof.
期刊信息：Luca Geatti, Alessandro Gianola, Nicola Gigante. First-Order Automata. Proceedings of AAAI 2025: 14940-14948
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v2 · 2026-11-10 20:23 · 最新观测版本
A General Automata Model for First-Order Temporal Logics (Extended Version)
First-order linear temporal logic (FO-LTL) 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 (of finite words), showing their closure under most language-theoretic operations. We show how they can capture any FO-LTL formula over finite words, 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 FO-LTL, a classic result known in the literature, with a simpler and direct proof.
查看此版本解读 →查看此版本原文 ↗