Some new proofs of Shepherdson’s theorem

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.