Buchi Automata Recognizing Sets of Reals Definable in First-Order Logic with Addition and Order

摘要

This work considers encodings of non-negative reals in a fixed base, and their encoding by weak deterministic Biichi automata. A Real Number Automaton is an automaton which recognizes all encodings of elements of a set of reals. We explain in this paper how to decide in linear time whether a set of reals recognized by a given minimal weak deterministic RNA is FO[IR;+,<, 1]-dennable. Furthermore, it is explained how to compute in quasi-quadratic (respectively, quasi-linear) time an existential (respectively, existential-universal) FO[IR; +, <, 1]-formula which defines the set of reals recognized by the automaton. As an additional contribution, the techniques used for obtaining our main result lead to a characterization of minimal deterministic Biichi automata accepting FO[IR; +, <, 1]-defmable set.