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.

Follow-up work extended end-to-end verification tools to incorporate constructive hybrid games, leading to more robust implementations which support a wider range of CPS models. Along the way, we 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.