Situation calculus game structures and GDL

We present a situation calculus-based account of multiplayers synchronous games in the style of general game playing. Such games can be represented as action theories of a special form, situation calculus synchronous game structures (SCSGSs), in which we have a single action tick whose effects depend on the combination of moves selected by the players. Then one can express properties of the game, e.g., winning conditions, playability, weak and strong winnability, etc. in a first-order alternating-time μ-calculus. We discuss verification in this framework considering computational effectiveness. We also show that SCSGSs can be considered as a firstorder variant of the Game Description Language (GDL) that supports infinite domains and possibly non-terminating games. We do so by giving a translation of GDL specifications into SCSGSs and showing its correctness. Finally, we show how a player's possible moves can be specified in a Golog-like programming language.