Monadic logical definability of nondeterministic linear time (Q1266167)

With an identification of finite models and binary strings, a logic \(\mathcal L\) captures a complexity class \(\mathcal C\) iff every language in \(\mathcal C\) is the class of finite models of some sentence over \(\mathcal L\) and, conversely, every such model class is in \(\mathcal C\) [see for example \textit{H.-D. Ebbinghaus} and \textit{J. Flum}, Finite model theory (1995; Zbl 0841.03014)]. The authors show that existential monadic second-order logic with addition captures NLIN, i.e., the class of languages which can be recognized in linear time by nondeterministic RAMs. Here in addition the first-order part of the sentence which characterizes a given language can be restricted to the form \(\forall^{\ast}\exists^{\ast}\). This result answers a question raised by James F. Lynch who showed a similar result for the class NTIME(n) of languages which can be recognized in linear time by nondeterministic Turing machines: every language in NTIME(n) is the class of finite models of a sentence as above [see \textit{J. F. Lynch}, Math. Syst. Theory 15, 127-144 (1982; Zbl 0484.03020) and Comput. Complexity 2, No. 1, 40-66 (1992; Zbl 0752.68040)]. The authors remark that their logical characterization of the class NLIN has been refined in an article by \textit{F. Olive} published in Lect. Notes Comput. Sci. 1414, 360-372 (1998).