Cost Automata, Safe Schemes, and Downward Closures

• Autorzy: Barozzini David , Clemente Lorenzo , Colcombe Thomas , Parys Paweł

Identyfikatory

DOI

10.3233/FI-222145

• Języki publikacji: EN

Abstrakty

EN

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

Słowa kluczowe

EN

cost logics; cost automata; downward closures; higher-order recursion schemes; safe recursion schemes

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: Vol. 188, nr 3
• Strony: 127--178
• Opis fizyczny: Bibliogr.

Twórcy

autor

Barozzini David

• Institute of Informatics University of Warsaw Warsaw, Poland

autor

Clemente Lorenzo

• Institute of Informatics University of Warsaw Warsaw, Poland

autor

Colcombe Thomas

• IRIF-CNRS-Universit´e de Paris Paris, France

autor

Parys Paweł

• Institute of Informatics University of Warsaw Warsaw, Poland