A Logical Characterisation of Linear Time on Nondeterministic Turing Machines

The paper gives a logical characterisation of the class NTIME(n) of problems that can be solved on a nondeterministic Turing machine in linear time. It is shown that a set L of strings is in this class if and only if there is a formula of the form ∃f1· · ∃fk∃R1· · ∃Rm∀xϕ that is true exactly for all strings in L. In this formula the fi are unary function symbols, the Ri are unary relation symbols and ϕ is a quantifierfree formula. Furthermore, the quantification of functions is restricted to non-crossing, decreasing functions and in ϕ no equations in which different functions occur are allowed. There are a number of variations of this statement, e.g., it holds also for k = 3. From these results we derive an Ehrenfeucht game characterisation of NTIME(n).

• Type: Conference
• Year: 1999
• Where: STACS
• Authors: Clemens Lautemann, Nicole Schweikardt, Thomas Schwentick
• Keywords: Logical Characterisation, Nondeterministic Turing Machine, STACS 1999, Theoretical Computer Science, Unary Relation Symbols