Cost Automata, Safe Schemes, and Downward Closures
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2020
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913231765766144 |
|---|---|
| author | Barozzini, David Clemente, Lorenzo Colcombet, Thomas Parys, Paweł |
| author_facet | Barozzini, David Clemente, Lorenzo Colcombet, Thomas Parys, Paweł |
| contents | In this work we prove decidability of the model-checking problem for safe recursion schemes against properties defined by alternating B-automata. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes.
Higher-order recursion schemes are an expressive formalism used to define languages of finite and infinite ranked trees by means of fixed points of lambda terms. They extend regular and context-free grammars, and are equivalent in expressive power to the simply typed $λY$-calculus and collapsible pushdown automata. Safety in a syntactic restriction which limits their expressive power.
The class of alternating B-automata is an extension of alternating parity automata over infinite trees; it enhances them with counting features that can be used to describe boundedness properties. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2004_12187 |
| institution | arXiv |
| publishDate | 2020 |
| record_format | arxiv |
| spellingShingle | Cost Automata, Safe Schemes, and Downward Closures Barozzini, David Clemente, Lorenzo Colcombet, Thomas Parys, Paweł Formal Languages and Automata Theory In this work we prove decidability of the model-checking problem for safe recursion schemes against properties defined by alternating B-automata. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes. Higher-order recursion schemes are an expressive formalism used to define languages of finite and infinite ranked trees by means of fixed points of lambda terms. They extend regular and context-free grammars, and are equivalent in expressive power to the simply typed $λY$-calculus and collapsible pushdown automata. Safety in a syntactic restriction which limits their expressive power. The class of alternating B-automata is an extension of alternating parity automata over infinite trees; it enhances them with counting features that can be used to describe boundedness properties. |
| title | Cost Automata, Safe Schemes, and Downward Closures |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2004.12187 |