First-Order Automata
Authors: Luca Geatti, Alessandro Gianola, Nicola Gigante
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | 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 FOLTL 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 FOLTL, a classic result known in the literature, with a simpler and direct proof. |
| Researcher Affiliation | Academia | 1Dipartimento di Scienze Matematiche, Informatiche e Fisiche, University of Udine, Udine, Italy 2INESC-ID/Instituto Superior T ecnico, Universidade de Lisboa, Lisbon, Portugal 3Faculty of Engineering, Free University of Bozen-Bolzano, Bolzano, Italy |
| Pseudocode | Yes | Algorithm 1: Non-emptiness semi-decision 1: procedure NONEMPTY(A) 2: for k 0 . . . + do 3: if JAKF k is T 0...k-satisfiable then 4: return not empty 5: end if 6: end for 7: end procedure |
| Open Source Code | No | The paper discusses existing tools like "BLACK temporal reasoning framework" and "modern SMT solvers" but does not state that the authors are releasing code for the first-order automata model described in this paper. There is no mention of a code repository, supplementary materials containing code, or an explicit statement of code release. |
| Open Datasets | No | This is a theoretical paper that defines a new model of automata and proves its properties. It does not conduct empirical studies using datasets. The paper does not mention or use any datasets in its work. |
| Dataset Splits | No | This paper is theoretical and does not involve experiments or the use of datasets, therefore, there is no discussion of dataset splits. |
| Hardware Specification | No | This paper is theoretical and does not describe any experimental setup involving specific hardware. |
| Software Dependencies | No | This paper is theoretical and does not describe specific software dependencies with version numbers for experimental reproducibility. It mentions using "modern SMT solvers" and the "BLACK temporal reasoning framework" in related work but not as dependencies for the described theoretical contributions. |
| Experiment Setup | No | This is a theoretical paper presenting definitions, theorems, and proofs. It does not include any experimental setup details, hyperparameters, or training configurations. |