## 2-VPAs are not determinizable

### - by S. La Torre, P. Madhusudan, and G. Parlato

Here is a proof showing that 2-VPAs (or 2-OVPAs)
are not determinizable. This proves that Theorem 6 of the paper
2-Visibly Pushdown Automata (by Dario Carotenuto, Aniello Murano

The proof is a simple adaptation of the non determinizability proof for
bouded-phase visibly pushdown automata over multiple stacks given in
A Robust Class of Context-Sensitive Languages (by Salvatore La Torre,

We prove that there is a simple language that cannot be accepted by any
2-VPA (or 2-OVPA).

Let a and b correspond to pushes of the first stack only and second stack
only respectively. Let c and d correspond to pops of the first stack while
x and y correspond to pops of the second. The language is

L = { (ab) i. c j.d {i-j}. x j.y {i-j} | i &isin N, j <= i }

In other words, we want to check if the number of pops "c" is equal to
the number of pops "x".

First, L is accepted by a nondet 2-stack VPA.
The VPA can, on a and b, push # onto both stacks, and nondeterministically
switch to a mode where it pushes \$ onto both stacks. Intuitively this
switch corresponds to the guess of what j is. On popping, it checks that
c's get popped on \$ and d's on #, and y's on \$ and x's on #.

Next, L is not determinizable: Assume the contrary and let A be a deterministic
VPA accepting L. After reading (ab)^i c^j d^{i-j}, the first stack must
be empty, and the second stack is *independent* of j (i.e. the automaton
must reach the same content of the second stack on (ab) i c j' d {i-j'}
for any j', since the pushes on the stack were done before discovering j
and A is deterministic. By choosing i large enough, larger than the number
of control states in A, it is easy to see that there is some j and j'
(j and j' different and less than i), such that A reaches the same configuration
(state+stacks) on (ab) i c j d {i-j} and (ab) i c j' d {i-j'}.
Hence appending the word x j.y {i-j} must be either accepted after
both the above words or rejected after both the above words, both contradicting
the assumption that A accepts L.