First-order definable pushdown automata

We reinterpret the classical definition of pushdown automata in the setting of first-order definable sets (a subclass of sets with atoms). In view of potential applicability of this model in verification of recursive programs that manipulate data, we investigate complexity of reachability analysis (aka nonemptiness problem).

As an important special case we prove NEXPTIME upper bound for nonemptiness of (a subclass of) timed pushdown automata, by reduction to systems of equations over sets of integers.