english Icono del idioma   español Icono del idioma  

Por favor, use este identificador para citar o enlazar este ítem: https://hdl.handle.net/20.500.12008/5822 Cómo citar
Título: Formalizing alternating-time temporal logic in the coq proof assistant
Autor: Luna, Carlos
Sierra, Luis
Zanarini, Dante
Tipo: Reporte técnico
Palabras clave: Alternating-time temporal logic (ATL)
Fecha de publicación: 2014
Resumen: 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.
Editorial: UR.FI-INCO
Serie o colección: Reportes Técnicos 14-13;
ISSN: 07976410
Citación: LUNA, C., SIERRA, L., ZANARINI, D. "Formalizing alternating-time temporal logic in the coq proof assistant". Montevideo : UR.FI-INCO, 2014. Reportes Técnicos 14-13.
Aparece en las colecciones: Reportes Técnicos - Instituto de Computación

Ficheros en este ítem:
Fichero Descripción Tamaño Formato   
TR1413.pdf264,43 kBAdobe PDFVisualizar/Abrir


Este ítem está sujeto a una licencia Creative Commons Licencia Creative Commons Creative Commons