joint work with Lorenzo Clemente

Speaker(s)

Sławomir Lasota

Affiliation

Uniwersytet Warszawski

Date

Feb. 4, 2015, 2:15 p.m.

Room

room 5870

Title in Polish

First-order definable pushdown automata

Seminar

Seminar Automata Theory

---

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.

---