David Barozzini ; Lorenzo Clemente ; Thomas Colcombet ; Paweł Parys - Cost Automata, Safe Schemes, and Downward Closures

fi:8485 - Fundamenta Informaticae, April 18, 2023, Volume 188, Issue 3
Cost Automata, Safe Schemes, and Downward ClosuresArticle

Authors: David Barozzini ; Lorenzo Clemente ; Thomas Colcombet ; Paweł Parys

    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.


    Volume: Volume 188, Issue 3
    Published on: April 18, 2023
    Accepted on: March 6, 2023
    Submitted on: September 16, 2021
    Keywords: Computer Science - Formal Languages and Automata Theory

    Consultation statistics

    This page has been seen 133 times.
    This article's PDF has been downloaded 89 times.