Formalizing alternating-time temporal logic in the coq proof assistant

Abstract

This work presents a complete formalization of Alternating-time Temporal Logic (ATL) and its semantic model, Concurrent Game Structures (CGS), in the Calculus of (Co)Inductive Constructions, using the logical framework Coq. Unlike standard ATL semantics, temporal operators are formalized in terms of inductive and coinductive types, employing a fixpoint characterization of these operators. The formalization is used to model a concurrent system with an unbounded number of players and states, and to verify some properties expressed as ATL formulas. Unlike automatic techniques, our formal model has no restrictions in the size of the CGS, and arbitrary state predicates can be used as atomic propositions of ATL. Keywords: Reactive Systems and Open Systems, Alternating-time Temporal Logic, Concurrent Game Structures, Calculus of (Co)Inductive Constructions, Coq Proof Assistant.