References & Citations
Computer Science > Logic in Computer Science
Title: Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
(Submitted on 11 Jan 2021 (v1), last revised 21 Mar 2022 (this version, v3))
Abstract: We introduce a model of register automata over infinite trees with extrema constraints. Such an automaton can store elements of a linearly ordered domain in its registers, and can compare those values to the suprema and infima of register values in subtrees. We show that the emptiness problem for these automata is decidable.
As an application, we prove decidability of the countable satisfiability problem for two-variable logic in the presence of a tree order, a linear order, and arbitrary atoms that are MSO definable from the tree order. As a consequence, the satisfiability problem for two-variable logic with arbitrary predicates, two of them interpreted by linear orders, is decidable.
Submission history
From: Thomas Zeume [view email] [via LOGICAL proxy][v1] Mon, 11 Jan 2021 13:26:48 GMT (695kb,D)
[v2] Tue, 5 Oct 2021 10:24:34 GMT (694kb,D)
[v3] Mon, 21 Mar 2022 18:25:20 GMT (169kb,D)
Link back to: arXiv, form interface, contact.