Título:
Formalizing alternating-time temporal logic in the coq proof assistant
Otros títulos:
Coordinador:
Director:
Compilador:
Autor:
Luna, Carlos
Sierra, Luis
Zanarini, Dante
Sierra, Luis
Zanarini, Dante
Tutor:
Tipo de documento:
Reporte técnico
Editor:
Palabras clave:
Alternating-time temporal logic (ATL)
Descriptores:
Año de publicación:
2014
Contenido:
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.
Descripción:
Editorial:
UR.FI-INCO
EN:
Reportes Técnicos 14-13;
Financiadores:
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.
Citación:
metadata.cc.license.name:
Documento del Gobiberno:
URI:
http://hdl.handle.net/20.500.12008/5822
ISBN:
e-ISBN:
ISSN:
07976410
ISMN:
Otros identificadores:
Título Obtenido:
Facultad o Servicio que otorga el Título:
Licencia:
Cobertura geográfica:
Cobertura temporal:
metadata.dc.relation.IsVersionOf:
Clasificación:
Es versión de:
Colecciones:
| Ficheros | Descripción | Tamaño | Formato | ||
|---|---|---|---|---|---|
| TR1413.pdf | — | 264.43 KB | Adobe PDF |