Géraud Sénizergues (LaBRI, Univ. Bordeaux)

We consider the classical theorem, due to [Shepherdson 1959], asserting that two-way finite automata recognize exactly the regular languages. We give four new proofs of this theorem:

  • proof.1 leans on Büchi right-linear deduction systems [Büchi-Hoske 1969];
  • proof.2 leans on Rabin’s tree theorem [Rabin 1969];
  • proof.3 leans on the structure of co-accessible configurations of an automata of order 2 [Hague-Hong 2007];
  • proof.4 leans on the structure of models of MSO-formula over the set of words of words [Fratani 2012].

These variations on an old theme of the fifties, illustrate several proof-methods that were developed since this time.

The talk is based on an ongoing work by Olivier Gauwin and Géraud Sénizergues.