Is there anything known about the problem of incremental emptiness testing for a pushdown automata?
Suppose you have a PDA with (up to) $n$ states and transitions, but instead of being given the transition table up front, you are given transition edges one at a time and asked whether their insertion would cause the PDA to accept a nonempty language. Also suppose that each transition can either push a single symbol, pop a single symbol, or leave the stack unchanged, and that the PDA has a designated start and end state, and is defined to accept a word if it results in reaching the end state with an empty stack.
So far, the best algorithm I've been able to come up with is $O(n^3)$, based on reducing this to the incremental directed reachability problem, and then applying the classic $O(n^3)$ algorithm. The basic idea is to maintain a directed graph with a vertex for each PDA state, with the invariant that b
is reachable from a
in that graph if and only if you can go from a
to b
in the PDA starting and ending with an empty stack. The $n^3$ reachability algorithm maintains a bit matrix (well actually a table of pointers) for the reachability of each node pair, and hence can determine when b
becomes reachable from a
for the first time. Whenever the source of a pop edge becomes reachable from the sink of a corresponding push edge, insert an edge into the directed graph from the source of the push edge to the sink of the pop edge (the push and pop edges themselves are obviously not included in the directed graph).
Note that incremental reachability can be done in $O(nm)$ time, where $m$ is the number of edges. In the case of the PDA, I specified a linear number of edges $n$ in the input. However, the extra edges added to level the stack transitions can result in up to $m = O(n^2)$ edges in the directed graph, and thus overall $O(n^3)$ time.
I've spent quite a bit of time thinking about this problem, but I haven't been able to improve on the $O(n^3)$ algorithm at all and am beginning to suspect that it is impossible. Does anyone know of any way to improve this or show that it can't be done?