# Decidability of halting problem for special kind of automata

Given an automaton $$\mathcal{A} = \left\langle S, s_0, \delta \right\rangle$$ over the finite alphabet $$\Sigma$$, where

• $$S$$ is a finite set of states,
• $$s_0 \in S$$ is an initial state,
• $$\delta\colon S \times \Sigma \rightarrow (\Sigma^\ast \times S) \cup \{\bot\}$$ is a (partial) transition function.

Consider a minimal transition relation $$\rightarrow$$ over configurations $$S \times \Sigma^\ast$$, such that,

$$\forall\, s, s^\prime \in S,\, x \in \Sigma% \cup \{\varepsilon\} ,\, \alpha, \gamma \in \Sigma^\ast\colon\, \delta(s, x) = \langle \gamma, s^\prime \rangle \Rightarrow \langle s, x\alpha\rangle \rightarrow \langle s^\prime, \alpha\gamma\rangle.$$

A run of $$\mathcal{A}$$ is any sequence of transitions:

$$\langle s_0, \alpha_0\rangle \rightarrow \langle s_1, \alpha_1\rangle \rightarrow \ldots \rightarrow \langle s_n, \alpha_n\rangle.$$

$$\mathcal{A}$$ accepts a word $$\alpha_0 \in \Sigma^\ast$$, iff there are only finite number of possible runs, i.e. there is no run of infinite length.

Thus we can define a language $$\mathcal{L}(\mathcal{A}) \subseteq \Sigma^\ast$$ of accepted words.

I wonder if $$\mathcal{A} \mapsto \mathcal{L}(\mathcal{A})$$ is decidable? In other words, is the halting problem decidable, given any $$\mathcal{A}$$ and input word $$\alpha_0 \in \Sigma^\ast$$? If yes, in which complexity class it is?

My own thoughts on that below.

Let $$\alpha_0 \notin \mathcal{L}(\mathcal{A})$$, then there is a run of infinite length. There are only two cases possible:

1. $$\exists\, i, j \in \mathbb{N}\colon\, i < j \wedge \langle s_i, \alpha_i\rangle = \langle s_j, \alpha_j \rangle$$ (“lasso”)
2. $$\forall\, n \in \mathbb{N}\colon \exists\, k(n) \in \mathbb{N}\colon |\alpha_{k(n)}| \geq n$$ (unbounded growth of tape)
• Can you please motivate your definition of "$\mathcal{A}$ accepts $\alpha_0$, it seems very peculiar. – Olivier Roche Dec 21 '19 at 20:36
• @OlivierRoche Maybe “accepts” is a wrong choice of word here, but the idea is to consider whether the run on word $\alpha_0$ is finite or not. You're right that this is peculiar for automata, since its acceptance condition deals with runs of infinite length. However, there are some automata with similar acceptance conditions that deals with infinity, e.g. Büchi automaton, which accepts exactly those runs in which at least one of the infinitely often occurring states is in some accepting set $F$. – Nastya Koroleva Dec 21 '19 at 20:49
• This reminds me of tag systems. I haven't gone through the details but it seems like your model could simulate cyclic tag systems, which have an undecidable halting problem. – Ilkka Törmä Dec 21 '19 at 22:55
• @IlkkaTörmä Thanks for the helpful reference! I will definitely take a look. – Nastya Koroleva Dec 21 '19 at 23:36
• @PeterTaylor the image of the transition function $\langle \gamma, s^\prime \rangle \in \Sigma^\ast \times S$ is an ordered pair of word and new state. – Nastya Koroleva Dec 22 '19 at 19:49

This model is well-known as queue automaton, so it's Turing complete and thus $$\mathcal{A} \mapsto \mathcal{L}(\mathcal{A})$$ is undecidable.