  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.
