Deciding FO-definability of Regular Languages.

We prove that, similarly to known PSpace-completeness of recognising FO( 1. These FO-languages are known to define regular languages that are decidable in AC0 and ACC0, respectively.) We obtain these results by first showing that known algebraic characterisations of FO-definability of L(A) can be captured by `localisable' properties of the transition monoid of A. Using our criterion, we then generalise the known proof of PSpace-hardness of FO(<)-definability, and establish the upper bounds not only for arbitrary DFAs but also for two-way NFAs.