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

Speaker(s)

Paweł Parys

Affiliation

Uniwersytet Warszawski

Date

March 23, 2016, 2:15 p.m.

Room

room 5870

Title in Polish

The Diagonal Problem for Higher-Order Recursion Schemes is Decidable

Seminar

Seminar Automata Theory

---

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.

---