Mostrar el registro sencillo del ítem
dc.contributor.author
Demri, Stéphane
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.date.available
2022-08-05T12:20:46Z
dc.date.issued
2019-12
dc.identifier.citation
Demri, Stéphane; Fervari, Raul Alberto; The power of modal separation logics; Oxford University Press; Journal of Logic and Computation; 29; 8; 12-2019; 1139-1184
dc.identifier.issn
0955-792X
dc.identifier.uri
http://hdl.handle.net/11336/164337
dc.description.abstract
We introduce a modal separation logic MSL whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction and implication from separation logic. With such a combination of operators, some fragments of MSL can be seen as genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. We analyse the decidability status and the computational complexity of several fragments of MSL, obtaining surprising results by design of proof methods that take into account the modal and separation features of MSL. For example, the satisfiability problem for the fragment of MSL with, the difference modality and separating conjunction ∗ is shown TOWER-complete whereas the restriction either to and ∗ or to and ∗ is only NP-complete. We establish that the full logic MSL admits an undecidable satisfiability problem. Furthermore, we investigate variants of MSL with alternative semantics and we build bridges with interval temporal logics and with logics equipped with sabotage operators.
dc.format
application/pdf
dc.language.iso
eng
dc.publisher
Oxford University Press
![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
COMPLEXITY
dc.subject
EXPRESSIVE POWER
dc.subject
MODEL-CHECKING
dc.subject
RELATION-CHANGING LOGICS
dc.subject
SATISFIABILITY
dc.subject
SEPARATION LOGICS
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
The power of modal separation logics
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-08-03T18:08:09Z
dc.identifier.eissn
1465-363X
dc.journal.volume
29
dc.journal.number
8
dc.journal.pagination
1139-1184
dc.journal.pais
Reino Unido
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.journal.ciudad
Oxford
dc.description.fil
Fil: Demri, Stéphane. Centre National de la Recherche Scientifique; Francia. Université Paris-Saclay; Francia
dc.description.fil
Fil: Fervari, Raul Alberto. Consejo Nacional de Investigaciones Científicas y Técnicas. Centro Científico Tecnológico Conicet - Córdoba; Argentina. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina
dc.journal.title
Journal of Logic and Computation
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/https://academic.oup.com/logcom/article-abstract/29/8/1139/5632063
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/doi/https://doi.org/10.1093/logcom/exz019
Archivos asociados