Formalizing alternating-time temporal logic in the coq proof assistant

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...

Full description

Bibliographic Details

Main Author:	Luna, Carlos (author)
Other Authors:	Sierra, Luis (author), Zanarini, Dante (author)
Format:	report
Language:	English
Published:	2014
Subjects:	Alternating-time temporal logic (ATL)
Online Access:	http://hdl.handle.net/20.500.12008/5822
Tags:	Add Tag No Tags, Be the first to tag this record!