Visibly Pushdown Modular Games
Ilaria De Crescenzo, Salvatore La Torre, Yaron Velner

TL;DR
This paper explores modular strategies in recursive game graphs with visibly pushdown automata conditions, establishing decidability, complexity results, and efficient solutions for specific cases.
Contribution
It introduces the first study of modular strategies with visibly pushdown automaton winning conditions, characterizes their complexity, and offers faster algorithms for finite-state automata cases.
Findings
Modular games with visibly pushdown automaton conditions are decidable.
Complexity varies: EXPTIME-complete for Büchi/Co-Büchi, 2EXPTIME-complete for CARET/NWTL.
New faster algorithm for finite-state automata winning conditions.
Abstract
Games on recursive game graphs can be used to reason about the control flow of sequential programs with recursion. In games over recursive game graphs, the most natural notion of strategy is the modular strategy, i.e., a strategy that is local to a module and is oblivious to previous module invocations, and thus does not depend on the context of invocation. In this work, we study for the first time modular strategies with respect to winning conditions that can be expressed by a pushdown automaton. We show that such games are undecidable in general, and become decidable for visibly pushdown automata specifications. Our solution relies on a reduction to modular games with finite-state automata winning conditions, which are known in the literature. We carefully characterize the computational complexity of the considered decision problem. In particular, we show that modular games with…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
