Register Automata with Extrema Constraints, and an Application to Two-Variable Logic

TL;DR

This paper introduces register automata with extrema constraints over infinite trees, proving their emptiness problem is decidable, and applies this to establish decidability results for two-variable logic with various orderings and predicates.

Contribution

It presents a novel automaton model with extrema constraints and demonstrates its application to decidability in two-variable logic with complex order structures.

Findings

Decidability of emptiness for register automata with extrema constraints.

Decidability of countable satisfiability for two-variable logic with orders.

Applicability to logic with MSO-definable atoms.

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.