A Logic for PTIME and a Parameterized Halting Problem

In the work of Nash et al. (2005) have raised the question whether a logic L_les, already introduced by Gurevich in 1988, captures polynomial time, and they give a reformulation of this question in terms of a parameterized halting problem p-Acc_les for nondeterministic Turing machines. We analyze the precise relationship between L_les and p-Acc_les. We show that p-Acc_les is not fixed-parameter tractable if "P ne NP holds for all time constructible and increasing functions.\´\´ Moreover, a slightly stronger complexity theoretic hypothesis implies that L_les does not capture polynomial time. Furthermore, we analyze the complexity of various variants of p-Acc_les and address its construction problem.