Two-Way Parikh Automata with a Visibly Pushdown Stack

February 11, 2019

Luc Dartois (LACL UPEC)

In this talk we investigate the complexity of the emptiness problem for Parikh automata equipped with a pushdown stack.
Pushdown Parikh automata extend pushdown automata with counters which can only be incremented and an acceptance condition given as a semi-linear set, which we represent as an existential Presburger formula over the final values of the counters. The non-emptiness problem both in the deterministic and non-deterministic cases is NP-c. If the input head can move in a two-way fashion, emptiness gets undecidable, even if the automaton deterministic.
We shift our focus to Visibly Pushdown Automata (read automata on XML documents) and we recover decidability using the single-use syntactic restriction, enforcing that any transition which increments at least one dimension is triggered only a bounded number of times per input position.
The main result showed in this talk is that non-emptiness of two-way visibly Parikh automata which are single-use is NExpTime-c.
We finally give applications of this result to decision problems for expressive transducer models from nested words (again read XML documents) to words, including the equivalence problem.