Higher-order recursion schemes are an expressive formalism used to define languages of possibly infinite ranked trees.
- Prelegent(ci)
- David Barozzini
- Afiliacja
- Uniwersytet Warszawski
- Termin
- 8 kwietnia 2020 14:15
- Informacje na temat wydarzenia
- Online seminar
- Seminarium
- Seminarium „Teoria automatów”
Higher-order recursion schemes are an expressive formalism used to define languages of possibly infinite ranked trees.
We prove, under a syntactical constraint called safety, decidability of the model-checking problem for recursion schemes against properties defined by alternating B-automata, an extension of alternating parity automata for infinite trees with a boundedness acceptance condition.
We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes.
This talk is based on a joint work with Lorenzo Clemente, Thomas Colcombet and Paweł Parys.