Logic-Automata Connections for Transformations - Logic and Its Applications - page 46

(the automaton obtained by dropping the register updates) is not aperiodic.
Therefore, in order to get FOT-definable functions, a first restriction would be
to require that the underyling automaton of an SST is aperiodic. However, it is
not sucient, as shown by the SST of Fig. 5(b), whose underlying automaton
has aperiodic transition monoid. However, the register flow, which alternates
between U and V registers on reading a , is not aperiodic. If one requires that
the transition monoid of an SST, which also speaks about the register flow, is
aperiodic, then one gets exactly FOT-definable functions:

Theorem 3 (E. Filiot, K. Shankara Narayanan and A. Trivedi [26]).
Let f : ʣ ∗ →

ʣ ∗ . The function f is FOT-definable iff it is definable by an SST
with aperiodic and restricted copy transition monoid.

This theorem should not be understood as an effective characterization of
FOT-definable functions. Indeed, it could be the case that an SST which de-
fines an FOT-definable function has not an aperiodic transition monoid. As an
example, consider an SST which alternates on reading the letter a between two
states, both accepting, and realizes the identity function with a single register. Its
transition monoid is not aperiodic, but the function it defines if FOT-definable.
It is also the case for automata: a non-aperiodic automaton may define a
first-order language. However for automata, FO-definable languages can be al-
gebraically characterised, as show by M.P. Schutzenberger : a language L is
FO-definable iff its syntactic monoid is aperiodic [38]. This characterisation is
effective if L is given as a finite automaton, and decidable in PSPace [18].
Finally, like for automata, deciding whether the transition monoid of an SST
is aperiodic and restricted copy is PSPace-C [26].

FO-translations in one-free variable Let us mention another transducer-logic
connection that has been shown for a less expressive class of functions, namely
the FO-translations of [30] restricted to FO-formulas in one-free variable and
length-preserving functions. Such a translation assumes a total order < on ʣ and
is defined by a tuple T of FO-formulas in one-free variable x ,say T =( ˆ ˃ ( x )) ˃∈ʣ ,

a a a

input b b

a | a b | abc a | a | aa b | c

q 0 q 1 q 2 q 3 q 4 q 5

run

copy 1 a a a c a a a c

φ 1 , 1 φ 1 , 1

φ 1 , 2 φ 1 , 2 φ 1 , 2 φ 1 , 2 φ 2 , 1 φ 2 , 1

φ 3 , 1 φ 3 , 1

copy 2 a

b

b

a

φ 2 , 3 φ 2 , 3

copy 3 c c

Fig. 6. Encoding of NFT by MSO-transducer