Sciweavers

CADE
2009
Springer

A Generalization of Semenov's Theorem to Automata over Real Numbers

15 years 14 days ago
A Generalization of Semenov's Theorem to Automata over Real Numbers
Abstract This work studies the properties of finite automata recognizing vectors with real components, encoded positionally in a given integer numeration base. Such automata are used, in particular, as symbolic data structures for representing sets definable in the first-order theory R, Z, +, , i.e., the mixed additive arithmetic of integer and real variables. They also lead to a simple decision procedure for this arithmetic. In previous work, it has been established that the sets definable in R, Z, +, can be handled by a restricted form of infinite-word automata, weak deterministic ones, regardless of the chosen numeration base. In this paper, we address the reciprocal property, proving that the sets of vectors that are simultaneously recognizable in all bases, by either weak deterministic or Muller automata, are those definable in R, Z, +, . This result can be seen as a generalization to the mixed integer and real domain of Semenov's theorem, which characterizes the sets of i...
Bernard Boigelot, Jérôme Leroux, Juli
Added 23 Nov 2009
Updated 23 Nov 2009
Type Conference
Year 2009
Where CADE
Authors Bernard Boigelot, Jérôme Leroux, Julien Brusten
Comments (0)