Modular strategies for recursive game graphs

Rajeev Alur, Salvatore La Torre, P. Madhusudan

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish (US)
Pages (from-to)230-249
Number of pages20
JournalTheoretical Computer Science
Volume354
Issue number2
DOIs
StatePublished - Mar 28 2006

Keywords

  • Games in verification
  • Model-checking
  • Pushdown systems

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Modular strategies for recursive game graphs'. Together they form a unique fingerprint.

Cite this