-
Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
Authors:
Christopher H. Broadbent,
Arnaud Carayol,
C. -H. Luke Ong,
Olivier Serre
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 selec…
▽ More
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.
△ Less
Submitted 2 March, 2021; v1 submitted 13 October, 2020;
originally announced October 2020.
-
Collapsible Pushdown Parity Games
Authors:
Christopher H. Broadbent,
Arnaud Carayol,
Matthew Hague,
Andrzej S. Murawski,
C. -H. Luke Ong,
Olivier Serre
Abstract:
This paper studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to es…
▽ More
This paper studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to establish the decidability of such games and to provide an effective representation of the winning region as well as of a winning strategy. Thus, the results obtained here provide all necessary tools for an in-depth study of logical properties of trees generated by collapsible pushdown automata/recursion schemes.
△ Less
Submitted 13 October, 2020;
originally announced October 2020.
-
Emptiness of Stack Automata is NEXPTIME-complete: A Correction
Authors:
Christopher Broadbent,
Arnaud Carayol,
Matthew Hague,
Olivier Serre
Abstract:
A saturation algorithm for collapsible pushdown systems was published in ICALP 2012. This work introduced a class of stack automata used to recognised regular sets of collapsible pushdown configurations. It was shown that these automata form an effective boolean algebra, have a linear time membership problem, and are equivalent to an alternative automata representation appearing in LICS 2010. It w…
▽ More
A saturation algorithm for collapsible pushdown systems was published in ICALP 2012. This work introduced a class of stack automata used to recognised regular sets of collapsible pushdown configurations. It was shown that these automata form an effective boolean algebra, have a linear time membership problem, and are equivalent to an alternative automata representation appearing in LICS 2010. It was also claimed that the emptiness problem for stack automata is PSPACE-complete. Unfortunately, this claim is not true. We show that the problem is in fact NEXPTIME-complete when the stacks being accepted are collapsible pushdown stacks, rather than the annotated stacks used in ICALP 2012.
△ Less
Submitted 30 May, 2018;
originally announced May 2018.
-
C-SHORe: Higher-Order Verification via Collapsible Pushdown System Saturation
Authors:
Christopher Broadbent,
Arnaud Carayol,
Matthew Hague,
Olivier Serre
Abstract:
Higher-order recursion schemes (HORS) have received much attention as a useful abstraction of higher-order functional programs with a number of new verification techniques employing HORS model-checking as their centrepiece. We give an account of the C-SHORe tool, which contributed to the ongoing quest for a truly scalable model-checker for HORS by offering a different, automata theoretic perspecti…
▽ More
Higher-order recursion schemes (HORS) have received much attention as a useful abstraction of higher-order functional programs with a number of new verification techniques employing HORS model-checking as their centrepiece. We give an account of the C-SHORe tool, which contributed to the ongoing quest for a truly scalable model-checker for HORS by offering a different, automata theoretic perspective. C-SHORe implements the first practical model-checking algorithm that acts on a generalisation of pushdown automata equi-expressive with HORS called collapsible pushdown systems (CPDS). At its core is a backwards saturation algorithm for CPDS. Additionally, it is able to use information gathered from an approximate forward reachability analysis to guide its backward search. Moreover, it uses an algorithm that prunes the CPDS prior to model-checking and a method for extracting counter-examples in negative instances. We provide an up-to-date comparison of C-SHORe with the state-of-the-art verification tools for HORS. The tool and additional material are available from http://cshore.cs.rhul.ac.uk.
△ Less
Submitted 17 September, 2018; v1 submitted 13 March, 2017;
originally announced March 2017.
