Modular strategies for recursive game graphs. (English) Zbl 1088.68099

Summary: Many problems in formal verification and program analysis can be formalized as computing winning strategies for two-player games on graphs. In this paper, we focus on solving games in recursive game graphs which 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 fixed-point computation algorithm for solving modular games such that in the worst case the 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.


68Q60 Specification and verification (program logics, model checking, etc.)
91A05 2-person games
91A43 Games involving graphs


Full Text: DOI Link


[4] Alur, R.; Henzinger, T. A.; Kupferman, O., Alternating-time temporal logic, J. ACM, 49, 5, 1-42 (2002)
[10] Büchi, J. R.; Landweber, L. H.G., Solving sequential conditions by finite-state strategies, Trans. AMS, 138, 295-311 (1969) · Zbl 0182.02302
[13] Chandra, A. K.; Kozen, D. C.; Stockmeyer, L. J., Alternation, J. Assoc. Comput. Mach., 28, 1, 114-133 (1981) · Zbl 0473.68043
[14] de Alfaro, L.; Henzinger, T. A., Interface automata, (Proc. Ninth Annu. Symp. Foundations of Software Engineering (FSE) (2001), ACM Press), 109-120
[15] Emerson, E. A., Model checking and the mu-calculus, (Immerman, N.; Kolaitis, Ph., Proc. DIMACS Symp. Descriptive Complexity and Finite Models (1997), American Mathematical Society Press), 185-214 · Zbl 0877.03020
[16] Garey, M.; Johnson, D. S., Computers and Intractability: A Guide to the Theory of NP-completeness (1979), W. Freeman and Co.: W. Freeman and Co. San Francisco · Zbl 0411.68039
[17] Harel, D.; Raz, D., Deciding emptiness for stack automata on infinite trees, Inform. and Comput., 113, 2, 278-299 (1994) · Zbl 0820.68079
[19] Hyland, J. M.E.; Ong, C.-H. L., On full abstraction for PCF: I, II, and III, Inform. and Comput., 163, 2, 285-408 (2000) · Zbl 1006.68027
[20] Kupferman, O.; Vardi, M. Y., Church’s problem revisited, Bull. Symbolic Logic, 5, 2, 245-263 (1999) · Zbl 0932.03029
[21] Kupferman, O.; Vardi, M.; Wolper, P., Module checking, Inform. and Comput., 164, 2, 322-344 (2001) · Zbl 1003.68071
[23] McNaughton, R., Infinite games played on finite graphs, Ann. Pure Appl. Logic, 65, 149-184 (1993) · Zbl 0798.90151
[24] Muller, D. E.; Schupp, P. E., The theory of ends, pushdown automata, and second-order logic, Theoret. Comput. Sci., 37, 51-75 (1985) · Zbl 0605.03005
[28] Rudie, K.; Wonham, W. M., Think globally, act locally: decentralized supervisory control, IEEE Trans. Automat. Control, 37, 11, 1692-1708 (1992) · Zbl 0778.93002
[29] Szyperski, C.; Gruntz, D.; Mure, S., Component Software—Beyond Object-Oriented Programming (2002), Addison-Wesley, ACM Press
[32] Walukiewicz, I., Pushdown processes: games and model-checking, Inform. and Comput., 164, 2, 234-263 (2001) · Zbl 1003.68072
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.