Constructive Hybrid Games in Game Logic


Constructive Game Logic (CGL) is a constructive counterpart to Parikh's Game Logic (GL). Game logics generalize dynamic logics with game modalities which express when a player of some 2-player, perfect-information, zero-sum game has a strategy to achieve some postcondition. CGL, in contrast to GL, ensures that the winning strategies of games are computable, i.e., implementable on a computer. Thus, CGL is especially suitable as a foundation for next-generation implementations of correct-by-construction synthesis technology which can produce control and monitoring code from a proof of correctness.

CGL supports a rich underlying theory. We explore several complementary semantic viewpoints: computable strategies can be defined explicitly as a language of realizers. Alternatively, CGL formulas can be translated into type theory, in which case strategies are terms, which are given operational meaning by playing against an opponent strategy for the same game. Proofs of CGL have their own operational interpretation as pure programs which can be normalized to normal proofs.

CGL has been extended to CdGL, the constructive logic of hybrid games, which enables verification of a wide range of cyber-physical systems. CdGL incorporates reasoning similar to the dGL, the classical logic of hybrid games: games can be analyzed using solutions, invariants, and auxiliary variables. This range of reasoning techniques is essential for practical applications, and CdGL ensures that such reasoning has a solid constructive foundation.

Ongoing thesis work seeks to extend end-to-end verification tools to incorporate constructive hybrid games, leading to more robust implementations which support a wider range of CPS models. In support of this goal, we have developed a refinement calculus for comparing hybrid games, with which we have shown that proofs of hybrid game correctness theorems can be exploited to reify winning strategies in hybrid systems which are suitable for use in existing tools while remaining faithful to a hybrid game.

d;sr

Constructive Games Expose Strategic Computation

Related Publication(s)

Brandon Bohrer and André Platzer.
Refining Constructive Hybrid Games
5th International Conference on Formal Structures for Computation and Deduction
FSCD 2020, Natal, Brazil, June 29-July 6, 2012, LIPIcs, 2020. © The authors.
To appear. preprint

Brandon Bohrer and André Platzer.
Constructive Hybrid Games
10th International Joint Conference on Automated Reasoning
IJCAR 2020, Paris, France, June 29-July 5, 2020, Springer, 2020. © The authors.
To appear. preprint

Brandon Bohrer, and André Platzer.
Constructive Game Logic
29th European Symposium on Programming
ESOP 2020, Dublin, Ireland, 2020, Springer, 2020. © The authors.
To appear. preprint