Symbolic computational techniques for solving games

P. Madhusudan, Wonhong Nam, Rajeev Alur

Research output: Contribution to journalConference article

Abstract

Games are useful in modular specification and analysis of systems where the distinction among the choices controlled by different components (for instance, the system and its environment) is made explicit. In this paper, we formulate and compare various symbolic computational techniques for deciding existence of winning strategies. The game structure is given implicitly, and the winning condition is of the form "p until q" for state predicates p and q. The first technique employs symbolic fixpoint computation using ordered binary decision diagrams [8]. The second technique checks for the existence of strategies that ensure winning within k steps, for a user specified bound k, by reduction to the satisfiability of quantified boolean formulas. Finally, the bounded case can also be solved by reduction to satisfiability of ordinary boolean formulas, and we discuss two techniques, one based on encoding the strategy tree, and one based on encoding a witness subgraph, for reduction to SAT. We compare the various approaches on two examples using existing tools such as MOCHA [3], MUCKE [7], SEMPROP [17], QUBE [11], BERKMIN [12].

Original languageEnglish (US)
Pages (from-to)578-592
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
Volume89
Issue number4
DOIs
StatePublished - 2003
EventBMC'2003, First International Workshop on Bounded Model Checking - Boulder, COL, United States
Duration: Jul 13 2003Jul 13 2003

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Symbolic computational techniques for solving games'. Together they form a unique fingerprint.

  • Cite this