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...
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | , |
| Format: | report |
| Language: | English |
| Published: |
2014
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/20.500.12008/5822 |
| Tags: |
No Tags, Be the first to tag this record!
|
Similar Items: Formalizing alternating-time temporal logic in the coq proof assistant
- A Fuzzy Logic Approach To Modelling The Passengers’ Flow And Dwelling Time
- The radical resection of the temporal bone
- Mathematical model for a temporal-bounded classifier in security environments
- NeuroFPGA : Implementing artificial neural networks on programmable logic devices
- Temporal bounded reasoning for context-based information fusion in DoS attack detection
- El colgajo del musculo temporal y su aplicación en la cirugía maxilofacial