TY - CHAP
T1 - Modular strategies for recursive game graphs
AU - Alur, Rajeev
AU - La Torre, Salvatore
AU - Madhusudan, Parthasarathy
N1 - Funding Information:
This research was supported in part by ARO URI award DAAD19-01-1-0473, and NSF awards CCR-9970925, ITR/SY 0121431, and CCR-030638. The second author was also supported by the MIUR Grant 60% 2002/2003. A preliminary version appeared in the Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and the Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 2619, 2003, pp. 363–378. ∗Corresponding author. E-mail addresses: [email protected] (R. Alur), [email protected] (S. La Torre), [email protected], [email protected] (P. Madhusudan).
PY - 2003
Y1 - 2003
N2 - In this paper, we focus on solving games in recursive game graphs that can model the control flow in sequential programs with recursive procedure calls. While such games can be viewed as the pushdown games studied in the literature, the natural notion of winning in our framework requires the strategies to be modular with only local memory; that is, resolution of choices within a module does not depend on the context in which the module is invoked, but only on the history within the current invocation of the module. While reachability in (global) pushdown games is known to be EXPTIME-complete, we show reachability in modular games to be NP-complete. We present a fixpoint computation algorithm for solving modular games such that the worst-case number of iterations is exponential in the total number of returned values from the modules. If the strategy within a module does not depend on the global history, but can remember the history of the past invocations of this module, that is, if memory is local but persistent, we show that reachability becomes undecidable.
AB - In this paper, we focus on solving games in recursive game graphs that can model the control flow in sequential programs with recursive procedure calls. While such games can be viewed as the pushdown games studied in the literature, the natural notion of winning in our framework requires the strategies to be modular with only local memory; that is, resolution of choices within a module does not depend on the context in which the module is invoked, but only on the history within the current invocation of the module. While reachability in (global) pushdown games is known to be EXPTIME-complete, we show reachability in modular games to be NP-complete. We present a fixpoint computation algorithm for solving modular games such that the worst-case number of iterations is exponential in the total number of returned values from the modules. If the strategy within a module does not depend on the global history, but can remember the history of the past invocations of this module, that is, if memory is local but persistent, we show that reachability becomes undecidable.
UR - http://www.scopus.com/inward/record.url?scp=26444569586&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=26444569586&partnerID=8YFLogxK
U2 - 10.1007/3-540-36577-x_26
DO - 10.1007/3-540-36577-x_26
M3 - Chapter
AN - SCOPUS:26444569586
SN - 3540008985
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 363
EP - 378
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Garavel, Hubert
A2 - Hatcliff, John
PB - Springer
ER -