Summaries for context-free games
From MaRDI portal
Publication:4636591
DOI10.4230/LIPICS.FSTTCS.2016.41zbMATH Open1391.68072arXiv1603.07256OpenAlexW2964239272MaRDI QIDQ4636591FDOQ4636591
Authors: Lukáš Holik, Roland Meyer, Sebastian Muskalla
Publication date: 19 April 2018
Abstract: We study two-player games played on the infinite graph of sentential forms induced by a context-free grammar (that comes with an ownership partitioning of the non-terminals). The winning condition is inclusion of the derived terminal word in the language of a finite automaton. Our contribution is a new algorithm to decide the winning player and to compute her strategy. It is based on a novel representation of all plays starting in a non-terminal. The representation uses the domain of Boolean formulas over the transition monoid of the target automaton. The elements of the monoid are essentially procedure summaries, and our approach can be seen as the first summary-based algorithm for the synthesis of recursive programs. We show that our algorithm has optimal (doubly exponential) time complexity, that it is compatible with recent antichain optimizations, and that it admits a lazy evaluation strategy. Our preliminary experiments indeed show encouraging results, indicating a speed up of three orders of magnitude over a competitor.
Full work available at URL: https://arxiv.org/abs/1603.07256
Recommendations
Formal languages and automata (68Q45) 2-person games (91A05) Grammars and rewriting systems (68Q42) Games involving graphs (91A43)
Cited In (4)
This page was built for publication: Summaries for context-free games
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4636591)