One counter automaton as a function

Question

We can associate a one counter finite automaton with a function $f:\Sigma^* \to \mathbb{N} \times \{0,1\}$, where $f(x)=(n,b)$ describes the state where the automaton terminates when fed an input word $x \in \Sigma^*$: $n$ holds the number inside the counter, and $b=1$ iff the state is an accepting state.

Is it decidable to determine whether two of these automata are associated with the same function?

I looked at posts like this one and this one too but I can't find the answer.

Furthermore, since these machines are always aimed to accept/reject a string, is there any natural way to expand them to represent a function? As an example, think of a machine that simply counts the number of times it visited a specific node in the DFA, or even simpler: counts the length of its input word.

Answer 1

You can use the counter value as the result of the function.

Furthermore, if I understood well your question, a simple way to map $(bool,nat)$ is the following: modify the state transitions of the original automata $A$ to make the counter value equal to $2x$ if the counter of the original A is $x$ and the state is rejecting, $2x+1$ if the counter of the original $A$ is $x$ and the state is accepting.

If the one-counter machine that returns $(bool, nat)$ (with no distinction between accept/reject states, because the accept/reject condition is embedded in the returned value as explained above) is deterministic, then you can decide equivalence using this trick:

Given automata $M_1$, $M_2$ computing $f_1,f_2:\Sigma^* \to N \times \{0,1\}$; you can transform them back to two standard accept/reject automata $M_1', M_2'$ computing $f_1',f_2':\Sigma^* \to \{0,1\}$.

Expand the alphabet adding an extra symbol $*$; and make $M_1'(x*^k ) = Accept$ if and only if $M_1(x) = k$.

When $M_1', M_2'$ find a $*$ they decrement the counter if it is $>0$, otherwise they enter a permanent reject state. If the counter reaches $0$ after the decrement, then they enter an accept state. If they find another symbol after a $*$ they enter a permanent reject state.

Now you can check language equivalence of the "standard" one-counter automata $M_1', M_2'$ (decidable in the deterministic case, see L.G.Valiant, M.S.Paterson, Deterministic One-Counter Automata, 1975) and by construction $L(M_1') = L(M_2')$ if and only if $f_1 = f_2$.

Answer 2

A related model is the finite state automaton with two tapes: it accepts pairs of strings ($u,v)$, each read from its respective tape. This is equivalent to so-called finite state transductions. Those define a "regular" mapping from strings to strings. Just imagine that the finite state automaton has instructions for "read" (from the first tape) and "write" to the second tape.

Why is this relevant to your question? Because we can easily restrict the output tape to a single symbol. Thus the machine accepts a subset of $\Sigma\times \{b\}^*$ for some symbol $b$. This is of course equivalent to subsets of $\Sigma^* \times N$.

Unfortunately it is undecidable whether two of these machines are equivalent. Theorem 6.3 in O.H. Ibarra, Reversal-bounded multicounter machines and their decision problems, J. Assoc. Comput. Mach., 25 (1978), 116-133.

Let $a$, $b$, and $c$ be three different symbols. Then it is undecidable whether or not, for an arbitrary regular transduction $R$ from $\{a, c\}$ to $\{b\}$, $g = \{a, c\}^* \times \{b\}^*$.

This does not contradict the fact that equivalence for one-counter machines is decidable. After all for one counter machines, the counter-value is not part of the output. In general one-counter machines accept if the counter is zero.