References & Citations
Computer Science > Formal Languages and Automata Theory
Title: Cost Automata, Safe Schemes, and Downward Closures
(Submitted on 25 Apr 2020 (v1), last revised 28 Mar 2023 (this version, v6))
Abstract: 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 $\lambda 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.
Submission history
From: Paweł Parys [view email][v1] Sat, 25 Apr 2020 16:53:46 GMT (171kb,D)
[v2] Wed, 15 Sep 2021 04:37:06 GMT (55kb,D)
[v3] Fri, 15 Apr 2022 04:13:04 GMT (67kb,D)
[v4] Wed, 28 Sep 2022 13:42:57 GMT (87kb,D)
[v5] Thu, 2 Mar 2023 11:07:56 GMT (87kb,D)
[v6] Tue, 28 Mar 2023 07:34:19 GMT (156kb,D)
Link back to: arXiv, form interface, contact.