Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties

TL;DR

This paper explores the logical properties of infinite trees generated by higher-order recursion schemes, providing effective solutions for model-checking, logical reflection, and selection problems using automata-theoretic techniques.

Contribution

It introduces effective methods for solving model-checking and related problems for higher-order recursion schemes using collapsible pushdown automata.

Findings

Effective solutions for model-checking of higher-order recursion schemes

Decidability results for logical reflection and selection problems

Utilization of collapsible pushdown automata and parity games

Abstract

This paper studies the logical properties of a very general class of infinite ranked trees, namely those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal mu-calculus, three main problems: model-checking, logical reflection (aka global model-checking, that asks for a finite description of the set of elements for which a formula holds) and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems we provide an effective solution. This is obtained thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.