patternMinor
One counter automaton as a function
Viewed 0 times
onecounterfunctionautomaton
Problem
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.
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.
Solution
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$.
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$.
Context
StackExchange Computer Science Q#106204, answer score: 2
Revisions (0)
No revisions yet.