A 2nfa is a nondeterministic finite automaton that can move its head left or right on the input tape, or not. Is the following language known to be decidable? $$ \textit{H}_{\mathsf{2nfa}} = \{ \langle M \rangle \mid M \textit{ is a } \mathsf{2nfa} \textit{ that halts on every input and on every branch} \} $$


This is not the same as the halting problem on 2nfa's: $$ \mathit{HALT}_{\mathsf{2nfa}} = \{ \langle M, x \rangle \mid M \textit{ is a } \mathsf{2nfa} \textit{ that halts on every branch, running on } x \} $$ Albeit the two are related, and as follows: $$ \langle M \rangle \in \textit{H}_{\mathsf{2nfa}} \iff \forall x, \langle M, x \rangle \in \textit{HALT}_{\mathsf{2nfa}} $$

I have attempted to write an algorithm deciding $\textit{H}_{\mathsf{2nfa}}$. It looks for the sequence of transitions of $M$, that start and end at the same state and the overall displacement of the head along the sequence is $0$. If there is such a loop, and some further details are satisfied, the algorithm decides that $M$ is not halting.

The problem is that I could not establish any bound on the length of the sequences to look for. I guess that looking for sequences of length up to some function of $M$'s number of states should be enough.

Is there perhaps another, more elegant way? Even better, a known result to refer?

  • 1
    $\begingroup$ The "global" state of the 2NFA on input $x$ at step $t$ is the pair $(q_t,p_t)$, where $q_t$ is the current state, and $p_t$ is head position on the input. Clearly if you don't allow the head to move off the input we have $1 \leq p_t \leq |x|$; so you must simply record every pair, if you find a repeated one then there is an infinite loop on a branch. There are at most $|Q| \times |x|$ distinct pairs. If you allow the head to move off the input, then you can consider the input $0^{|Q|} \,x\, 0^{|Q|}$ with the head at the beginning of $x$. If it moves off, then there is an infinite loop. $\endgroup$ Commented Jun 8, 2020 at 9:07
  • $\begingroup$ @MarzioDeBiasi This explains that the halting problem on 2NFA's is decidable, right? I was asking something else; whether a 2NFA halts on every branch running on any input x, not a particular one. I have just added that clarification to the question. I do not see a clear reduction from my problem to the halting problem. $\endgroup$ Commented Jun 8, 2020 at 10:48
  • $\begingroup$ ok, is the head allowed to move "off" the input ? $\endgroup$ Commented Jun 8, 2020 at 10:55
  • $\begingroup$ @MarzioDeBiasi Sorry, I had to think this through. The input is delimited with end markers on both ends. Let's say that the 2nfa pays attention to not cross those markers. (My guess is that this shouldn't matter; i.e. if the problem is decidable for 2nfa's that pay attention to stay within limits, then it would also be decidable for 2nfa's that do not pay attention.) $\endgroup$ Commented Jun 8, 2020 at 12:27

1 Answer 1


Lemma 1. $H_{\textsf{2nfa}}$ is decidable.

Proof. Decide it as follows. Given as input a two-way non-deterministic finite automaton $M_{\textsf{2nfa}}$:

  1. Convert $M_{\textsf{2nfa}}$ into a two-way alternating finite automaton $M_{\textsf{2wafa}}$ such that the language of $M_{\textsf{2wafa}}$ is $$L(M_{\textsf{2wafa}}) = \{x \in \Sigma^* : \text{ all execution paths of $M_{\textsf{2nfa}}$ on input $x$ halt }\},$$ that is, the set of inputs $x$ to $M_{\textsf{2nfa}}$ such that all execution paths of $M_{\textsf{2nfa}}$ on $x$ halt. (An alternating finite automata has $\exists$-transitions and $\forall$-transitions. Here we make every (non-deterministic) transition of $M_{\textsf{2nfa}}$ into a $\forall$-transition in $M_{\textsf{2wafa}}$, we don't use $\exists$-transitions, and we make the accept states of $M_{\textsf{2wafa}}$ be the halting states of $M_{\textsf{2nfa}}$.)

  2. Convert $M_{\textsf{2wafa}}$ into an equivalent one-way NFA $M_{\textsf{nfa}}$. (See e.g. here. I assume but have not verified that this conversion is computable. It appears to be computable, see the proof of Lemma 1, p. 296.)

  3. Convert $M_{\textsf{nfa}}$ into an equivalent DFA $M_{\textsf{dfa}}$, and check whether $L(M_{\textsf{dfa}}) = \Sigma^*$ (all using standard techniques). Accept if so. $~~\Box$

  • 1
    $\begingroup$ The issue of possibly unbounded run times of a 2-way NFA appears to be dealt with in a more direct way in Complement for two-way alternating automata by Geffert et al. $\endgroup$
    – Neal Young
    Commented Jun 8, 2020 at 21:37
  • $\begingroup$ I have been keeping this tab open, for the day I'll finally have time to verify that the conversion at Stage 2 is computable myself. I couldn't do it in a short glimpse, unfortunately, and it has already been 2 weeks since you've helped me. I am accepting the answer now, but I promise to comment with my approval later on! $\endgroup$ Commented Jun 20, 2020 at 22:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.