Pin & Weil [PW95] characterized the automata of existentially first-order definable languages. We will use this result for the following characterization of the complexity class NP. Assume that the Polynomial-Time Hierarchy does not collapse. Then a regular language L characterizes NP as an unbalanced polynomial-time leaf language if and only if L is existentially but not quantifierfree definable in FO[<,min,max,-1,+1].
展开▼