Symbolic computational techniques for solving games

Rajeev Alur, P. Madhusudan, Wonhong Nam

Research output: Contribution to journalArticlepeer-review

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 the existence of winning strategies. The game structure is given implicitly, and the winning condition is either a reachability game of the form "p until q" (for state predicates p and q) or a safety game of the form "Always p." For reachability games, the first technique employs symbolic fixed-point computation using ordered binary decision diagrams (BDDs) [9]. 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 also show how some of these techniques can be adopted to solve safety games. We compare the various approaches by evaluating them on two examples for reachability games, and on an interface synthesis example for a fragment of TinyOS [15] for safety games. We use existing tools such as Mocha [4], Mucke [7], Semprop [19], Qube [12], and Berkmin [13] and contrast the results.

Original languageEnglish (US)
Pages (from-to)118-128
Number of pages11
JournalInternational Journal on Software Tools for Technology Transfer
Volume7
Issue number2
DOIs
StatePublished - Apr 2005

Keywords

  • Bounded model checking
  • Formal verification
  • Games
  • QBF solving
  • Symbolic model checking

ASJC Scopus subject areas

  • Software
  • Information Systems

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

Cite this