Resource reachability games on pushdown graphs

We consider two-player games on the configuration graph of pushdown systems with an additional finite set of non-negative integer counters. These counters can be incremented, reset to zero or left unchanged by the transition rules of the pushdown system. We associate the cost of a play with the highest counter value that occurs and look at a combined reachability and cost-limit winning condition. Is there a uniform cost-bound k such that one can win from a set of configurations A with this bound? We provide a solution to this question by an extension of the well-known saturation principle.

Authors

• Martin Lang
• Christof Löding RWTH Aachen University

Keywords

No keywords are indexed for this paper.