Summaries for Context-Free Games

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F16%3APU122841" target="_blank" >RIV/00216305:26230/16:PU122841 - isvavai.cz</a>

Výsledek na webu

<a href="http://drops.dagstuhl.de/opus/volltexte/2016/6876" target="_blank" >http://drops.dagstuhl.de/opus/volltexte/2016/6876</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.41" target="_blank" >10.4230/LIPIcs.FSTTCS.2016.41</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Summaries for Context-Free Games

Popis výsledku v původním jazyce

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. 

Název v anglickém jazyce

Summaries for Context-Free Games

Popis výsledku anglicky

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. 

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

ISBN

978-3-95977-027-9

ISSN

—

e-ISSN

—

Počet stran výsledku

16

Strana od-do

41-57

Název nakladatele

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Místo vydání

Dagstuhl

Místo konání akce

Chennai Mathematical Institute, Chennai, India

Datum konání akce

13. 12. 2016

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—