B\"uchi automata recognizing sets of reals definable in first-order logic with addition and order

TL;DR

This paper presents methods to decide definability of real sets recognized by weak deterministic B"uchi automata using first-order logic with addition and order, with efficient algorithms for formula construction.

Contribution

It introduces linear-time decision procedures and quasi-quadratic algorithms for computing defining formulas for sets of reals recognized by automata, extending techniques to real numbers.

Findings

Decidability of FO-definability for recognized real sets.

Efficient algorithms for formula construction.

Extension of automata techniques to vector of reals.

Abstract

This work considers weak deterministic B\"uchi automata reading encodings of non-negative reals in a fixed base. A Real Number Automaton is an automaton which recognizes all encoding of elements of a set of reals. It is explained how to decide in linear time whether a set of reals recognized by a given minimal weak deterministic RNA is ${FO}[\mathbb R;+,<,1]$-definable. Furthermore, it is explained how to compute in quasi-quadratic (respectively, quasi-linear) time an existential (respectively, existential-universal) ${FO}[\mathbb R;+,<,1]$-formula which defines the set of reals recognized by the automaton. It is also shown that techniques given by Muchnik and by Honkala for automata over vector of natural numbers also works on vector of real numbers. It implies that some problems such as deciding whether a set of tuples of reals $R\subseteq\mathbb R^{d}$ is a subsemigroup of $(\mathbb R^{d},+)$ or is ${FO}[\mathbb R;+,<,1]$-definable is decidable.