Strategy synthesis for linear arithmetic games

Azadeh Farzan, Zachary Kincaid

Research output: Contribution to journalArticlepeer-review

8 Scopus citations

Abstract

Many problems in formal methods can be formalized as two-player games. For several applications-program synthesis, for example-in addition to determining which player wins the game, we are interested in computing a winning strategy for that player. This paper studies the strategy synthesis problem for games defined within the theory of linear rational arithmetic. Two types of games are considered. A satisfiability game, described by a quantified formula, is played by two players that take turns instantiating quantifiers. The objective of each player is to prove (or disprove) satisfiability of the formula. A reachability game, described by a pair of formulas defining the legal moves of each player, is played by two players that take turns choosing positions-rational vectors of some fixed dimension. The objective of each player is to reach a position where the opposing player has no legal moves (or to play the game forever). We give a complete algorithm for synthesizing winning strategies for satisfiability games and a sound (but necessarily incomplete) algorithm for synthesizing winning strategies for reachability games.

Original languageEnglish (US)
Article number61
JournalProceedings of the ACM on Programming Languages
Volume2
Issue numberPOPL
DOIs
StatePublished - Jan 2018

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality

Keywords

  • Functional synthesis
  • Logical games
  • Reactive synthesis

Fingerprint

Dive into the research topics of 'Strategy synthesis for linear arithmetic games'. Together they form a unique fingerprint.

Cite this