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:
- $\exists\, i, j \in \mathbb{N}\colon\, i < j \wedge \langle s_i, \alpha_i\rangle = \langle s_j, \alpha_j \rangle$ (“lasso”)
- $\forall\, n \in \mathbb{N}\colon \exists\, k(n) \in \mathbb{N}\colon |\alpha_{k(n)}| \geq n$ (unbounded growth of tape)
This model is well-known as queue automaton, so it's Turing complete and thus $\mathcal{A} \mapsto \mathcal{L}(\mathcal{A})$ is undecidable.