Mostrar el registro sencillo del ítem
dc.contributor.author
Fervari, Raul Alberto
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.contributor.author
Trucco, Francisco Carlos
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.contributor.author
Ziliani, Luis Francisco
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.date.available
2022-02-25T13:49:30Z
dc.date.issued
2021-04
dc.identifier.citation
Fervari, Raul Alberto; Trucco, Francisco Carlos; Ziliani, Luis Francisco; Verification of Dynamic Bisimulation Theorems in Coq; Elsevier; Journal of Logical and Algebraic Methods in Programming; 120; 4-2021; 1-30
dc.identifier.issn
2352-2208
dc.identifier.uri
http://hdl.handle.net/11336/152736
dc.description.abstract
Over the last years, the study of logics that can update a model while evaluating a formula has gained in interest. Motivated by many examples in practice such as hybrid logics, separation logics and dynamic epistemic logics, the ability to update a model has been investigated from a more general point of view. In this work, we formalize and verify in the proof assistant Coq, the bisimulation theorems for a particular family of dynamic logics that can change the structure of a relational model while evaluating a formula. Our framework covers update operators to perform different kinds of modifications on the accessibility relation, the valuation and the evaluation point of a model. The benefits of this formalization are twofold. First, our results apply for a wide variety of dynamic logics. Second, we argue that this is the first step towards the development of a modal logic library in Coq, which allows us to mechanize many relevant results.
dc.format
application/pdf
dc.language.iso
eng
dc.publisher
Elsevier
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.rights
info:eu-repo/semantics/restrictedAccess
dc.rights.uri
https://creativecommons.org/licenses/by-nc-sa/2.5/ar/
dc.subject
BISIMULATION
dc.subject
DYNAMIC LOGICS
dc.subject
MODAL LOGICS
dc.subject
PROOF MECHANIZATION
dc.subject.classification
Ciencias de la Computación
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.subject.classification
Ciencias de la Computación e Información
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.subject.classification
CIENCIAS NATURALES Y EXACTAS
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.title
Verification of Dynamic Bisimulation Theorems in Coq
dc.type
info:eu-repo/semantics/article
dc.type
info:ar-repo/semantics/artículo
dc.type
info:eu-repo/semantics/publishedVersion
dc.date.updated
2022-02-22T15:54:08Z
dc.identifier.eissn
2352-2216
dc.journal.volume
120
dc.journal.pagination
1-30
dc.journal.pais
Países Bajos
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.journal.ciudad
Amsterdam
dc.description.fil
Fil: Fervari, Raul Alberto. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física. Sección Ciencias de la Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas. Centro Científico Tecnológico Conicet - Córdoba; Argentina
dc.description.fil
Fil: Trucco, Francisco Carlos. TU Wien; Austria
dc.description.fil
Fil: Ziliani, Luis Francisco. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física. Sección Ciencias de la Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas. Centro Científico Tecnológico Conicet - Córdoba; Argentina
dc.journal.title
Journal of Logical and Algebraic Methods in Programming
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/https://www.sciencedirect.com/science/article/pii/S2352220821000055
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/doi/https://doi.org/10.1016/j.jlamp.2021.100642
Archivos asociados