206
9 mars 2017 - 14h00
Deterministic Automaton and logically definable sets of numbers.
par Arthur Milchior de Université Paris Diderot IRIF
Abstract: For a fixed base b, any integer can be encoded as a finite word of
alphabet of digits. In dimension d>0, a vector of d integers is encoded
as a word of alphabet of vector of d digits. A set of vector of integers
is thus encoded as a language whose alphabet is the set of vector of
digits. Thus, an automaton whose alphabet is the set of vector of digits
recognizes a set of integers. Similarly, a Büchi automaton recognizes a
set of vector of real.
It is then natural to consider algorithms which decide whether the set
of vectors of numbers accepted by a finite automaton admits some
properties. For example, Honkala proved in 1986 that it is decidable
whether an automaton recognize a FO[N,+,<]-definable set of integers.
Muchnik proved a similar result for automata recognizing sets of vectors
of integers. A polynomial-time algorithm was then given by Leroux in
2006, and a quasi-linear time algorithm for the case of dimension 1 was
given in 2013 by Marsault and Sakarovitch.
We state that it is decidable in linear time:
- whether a set of reals recognized by a given finite minimal weak Büchi
automaton is FO[R,+,<]-definable.
- whether a set of vectors recognized by a minimal finite deterministic
automaton can be defined in some logics less expressive than FO[N,+],
such as FO[N,<,mod].
Furthermore, formulas which defines those sets can be computed in linear
time and cubic time respectively.
Furthermore, is shown that it is decidable whether a set of vector of
real or of integers accepted by a (weak Büchi) automaton:
- is definable in a logic which admits quantifier-elimination. For
example, if the set is definable in FO[R,+,<], FO[R,Z,+,<,mod,floor]
where mod is the set of modular predicate, FO[N,<,mod] or FO[<].
- satisfies a first-order formula in some formalism. For example, whether
a set is a submonoid/subsemigroup of (R^d,+)
In this talk, I intend to:
- introduce automata recognizing set of vector of numbers,
- characterize the set of numbers which are FO[N,<,mod]- and
FO[R,+,<]-definable,
- introduce and generalizes the methods used by Honkala, Muchnik and
Marsault-Sakarovitch
- explain how how those methods can be applied to the above-mentioned
problems.
