The Diagonal Problem for Higher-Order Recursion Schemes is Decidable

Prelegent(ci)

Paweł Parys

Afiliacja

Uniwersytet Warszawski

Termin

23 marca 2016 14:15

Pokój

p. 5870

Tytuł w języku angielskim

joint work with L. Clemente, S. Salvati, I. Walukiewicz

Seminarium

Seminarium „Teoria automatów”

---

A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show the decidability of the diagonal problem for schemes: given a scheme G, decide whether for every n there exists a tree in the language of G that has at least n appearances of every alphabet letter. This result has several interesting consequences. In particular, it gives an algorithm to compute the downward closure of languages of words recognized by schemes. In turn, this has immediate application to separability problems and reachability analysis of concurrent systems.

---