First-order definable pushdown automata

Prelegent(ci)

Sławomir Lasota

Afiliacja

Uniwersytet Warszawski

Termin

4 lutego 2015 14:15

Pokój

p. 5870

Tytuł w języku angielskim

joint work with Lorenzo Clemente

Seminarium

Seminarium „Teoria automatów”

---

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.

---