Domains for Higher-Order Games
From MaRDI portal
Publication:5111275
DOI10.4230/LIPICS.MFCS.2017.59zbMATH Open1441.68125arXiv1705.00355OpenAlexW2963788871MaRDI QIDQ5111275FDOQ5111275
Roland Meyer, Sebastian Muskalla, Matthew Hague
Publication date: 26 May 2020
Abstract: We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixed-point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a (k+1)EXP algorithm for order-k recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixed-point computations can be applied.
Full work available at URL: https://arxiv.org/abs/1705.00355
Recommendations
Formal languages and automata (68Q45) Applications of game theory (91A80) Semantics in the theory of computing (68Q55)
Cites Work
- Borel determinacy
- Nested interpolants
- The IO- and OI-hierarchies
- An automata-theoretical characterization of the OI-hierarchy
- Title not available (Why is that?)
- Antichains: A New Algorithm for Checking Universality of Finite Automata
- Pushdown processes: Games and model-checking
- Title not available (Why is that?)
- Reachability analysis of pushdown automata: Application to model-checking
- Title not available (Why is that?)
- Recognizability in the Simply Typed Lambda-Calculus
- A Saturation Method for Collapsible Pushdown Systems
- Types and higher-order recursion schemes for verification of higher-order programs
- A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata
- Automata, Languages and Programming
- Title not available (Why is that?)
- Winning Regions of Pushdown Parity Games: A Saturation Method
- Title not available (Why is that?)
- Title not available (Why is that?)
- Strictness analysis for higher-order functions
- Abstract Interpretation, Logical Relations, and Kan Extensions
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems
- Safety of abstract interpretations for free, via logical relations and Galois connections
- Proving Liveness of Parameterized Programs
- Efficient Büchi Universality Checking
- Relational semantics of linear logic and higher-order model-checking
- Advanced Ramsey-Based Büchi Automata Inclusion Testing
- Proof spaces for unbounded parallelism
- Collapsible Pushdown Automata and Recursion Schemes
- Saturation-Based Model Checking of Higher-Order Recursion Schemes.
- An Infinitary Model of Linear Logic
- Abstract interpretation from Büchi automata
- Title not available (Why is that?)
- Using models to model-check recursive schemes
- Proofs that count
- Finitary Semantics of Linear Logic and Higher-Order Model-Checking
- A model for behavioural properties of higher-order programs
- Typing Weak MSOL Properties
- Summaries for Context-Free Games
- Domains for Higher-Order Games
Cited In (1)
Uses Software
This page was built for publication: Domains for Higher-Order Games
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111275)
