[en] This article studies the expressive power of finite automata recognizing sets of real numbers encoded in positional notation. We consider Muller automata as well as the restricted class of weak deterministic automata, used as symbolic set representations in actual applications. In previous work, it has been established that the sets of numbers that are recognizable by weak deterministic automata in two bases that do not share the same set of prime factors are exactly those that are definable in the first order additive theory of real and integer numbers. This result extends Cobham's theorem, which characterizes the sets of integer numbers that are recognizable by finite automata in multiple bases. In this article, we first generalize this result to multiplicatively independent bases, which brings it closer to the original statement of Cobham's theorem. Then, we study the sets of reals recognizable by Muller automata in two bases. We show with a counterexample that, in this setting, Cobham's theorem does not generalize to multiplicatively independent bases. Finally, we prove that the sets of reals that are recognizable by Muller automata in two bases that do not share the same set of prime factors are exactly those definable in the first order additive theory of real and integer numbers. These sets are thus also recognizable by weak deterministic automata. This result leads to a precise characterization of the sets of real numbers that are recognizable in multiple bases, and provides a theoretical justification to the use of weak automata as symbolic representations of sets.
Disciplines :
Computer science
Author, co-author :
Boigelot, Bernard ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique
Brusten, Julien ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique
Bruyère, Véronique; Université de Mons-Hainaut - UMH > Institut d'Informatique
Language :
English
Title :
On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases
Publication date :
2010
Journal title :
Logical Methods in Computer Science
eISSN :
1860-5974
Publisher :
Springer, Heidelberg, Germany
Volume :
6
Issue :
1
Pages :
1-17
Peer reviewed :
Peer Reviewed verified by ORBi
Funders :
Interuniversity Attraction Poles program MoVES of the Belgian Federal Science Policy Office Grant 2.4530.02 of the Belgian Fund for Scientific Research (F.R.S.-FNRS)
B. Boigelot and J. Brusten. A generalization of Cobham's theorem to automata over real numbers. Theoretical Computer Science, 410(18):1694-1703, 2009.
B. Boigelot, L. Bronne, and S. Rassart. An improved reachability analysis method for strongly linear hybrid systems. In Proc. 9th CAV, volume 1254 of Lecture Notes in Computer Science, pages 167-177, Haifa, June 1997. Springer.
V. Bruyère, G. Hansel, C. Michaux, and R. Villemaire. Logic and p-recognizable sets of integers. Bulletin of the Belgian Mathematical Society, 1(2):191-238, March 1994.
B. Boigelot, S. Jodogne, and P. Wolper. An effective decision procedure for linear arithmetic over the integers and reals. ACM Transactions on Computational Logic, 6(3):614-633, 2005.
B. Boigelot. Symbolic methods for exploring infinite state Sspaces. PhD thesis, Universit ́e de Liège, 1998.
B. Boigelot, S. Rassart, and P. Wolper. On the expressiveness of real and integer arithmetic automata. In Proc. 25th ICALP, volume 1443 of Lecture Notes in Computer Science, pages 152-163, Aalborg, July 1998. Springer.
J. R. Büchi. On a decision method in restricted second order arithmetic. In Proc. International Congress on Logic, Methodoloy and Philosophy of Science, pages 1-12, Stanford, 1962. Stanford University Press.
A. Cobham. On the base-dependence of sets of numbers recognizable by finite automata. Mathematical Systems Theory, 3:186-192, 1969.
J. Eisinger and F. Klaedtke. Don't care words with an application to the automata-based approach for real addition. In Proc. 18th CAV, volume 4144 of Lecture Notes in Computer Science, pages 67-80, Seattle, August 2006. Springer
Fast Acceleration of Symbolic Transition systems (FAST). Available at: http://www.lsv.ens-cachan.fr/fast/
G. H. Hardy and E. M. Wright. An introduction to the theory of numbers. Oxford University Press, 5th edition, 1985.
The Liège Automata-based Symbolic Handler (LASH). Available at: http://www.montefiore.ulg.ac.be/~boigelot/research/lash/.
Linear Integer/Real Arithmetic solver (LIRA). Available at: http://lira.gforge.avacs.org/.
R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5):521-530, 1966.
O. Maler and L. Staiger. On syntactic congruences for ω-languages. Theoretical Computer Science, 183(1):93-112, 1997.
D. Perrin. Finite automata. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 1-57. Elsevier and MIT Press, 1990.
D. Perrin and J.E. Pin. Infinite words, volume 141 of Pure and Applied Mathematics. Elsevier, 2004.
S. Safra. On the complexity of ω-automata. In Proc. 29th Symposium on Foundations of Computer Science, pages 319-327. IEEE Computer Society, October 1988.
M. Vardi. The Büchi complementation saga. In Proc. 24th. STACS, volume 4393 of Lecture Notes in Computer Science, pages 12-22, Aachen, February 2007. Springer.
P. Wolper and B. Boigelot. An automata-theoretic approach to Presburger arithmetic constraints. In Proc. 2nd SAS, volume 983 of Lecture Notes in Computer Science, pages 21-32, Glasgow, September 1995. Springer.
V. Weispfenning. Mixed real-integer linear quantifier elimination. In Proc. ACM SIGSAM IS-SAC, pages 129-136, Vancouver, July 1999. ACM Press.
T. Wilke. Locally threshold testable languages of infinite words. In Proc. 10th STACS, volume 665 of Lecture Notes in Computer Science, pages 607-616, Würzburg, 1993. Springer.