Swap logic

Mostrar todas las versiones(2)

We investigate dynamic modal operators that can change the model during evaluation. We define the logic SL by extending the basic modal language with the ♦ modality, which is a diamond operator that in addition has the ability to invert pairs of related elements in the domain while traversing an edg...

Descripción completa

Detalles Bibliográficos
Autores principales: Areces, Carlos Eduardo, Fervari, Raúl Alberto, Hoffmann, Guillaume Emmanuel
Formato: article
Lenguaje:Inglés
Publicado: 2021
Materias:
Modal logic
Dynamic logics
Expressivity
Complexity
Acceso en línea:http://hdl.handle.net/11086/20427
https://doi.org/10.1093/jigpal/jzt030
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-20427
record_format dspace
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Inglés
topic Modal logic
Dynamic logics
Expressivity
Complexity
spellingShingle Modal logic
Dynamic logics
Expressivity
Complexity
Areces, Carlos Eduardo
Fervari, Raúl Alberto
Hoffmann, Guillaume Emmanuel
Swap logic
topic_facet Modal logic
Dynamic logics
Expressivity
Complexity
description We investigate dynamic modal operators that can change the model during evaluation. We define the logic SL by extending the basic modal language with the ♦ modality, which is a diamond operator that in addition has the ability to invert pairs of related elements in the domain while traversing an edge of the accessibility relation. SL is very expressive: it fails to have the finite and the tree model property. We show that SL is equivalent to a fragment of first-order logic by providing a satisfiability preserving translation. In addition, we provide an equivalence preserving translation from SL to the hybrid logic H(:, ↓). We also define a suitable notion of bisimulation for SL and investigate its expressive power, showing that it lies strictly between the basic modal logic and H(:, ↓). We finally show that its model checking problem is PSpace-complete and its satisfiability problem is undecidable.
format article
author Areces, Carlos Eduardo
Fervari, Raúl Alberto
Hoffmann, Guillaume Emmanuel
author_facet Areces, Carlos Eduardo
Fervari, Raúl Alberto
Hoffmann, Guillaume Emmanuel
author_sort Areces, Carlos Eduardo
title Swap logic
title_short Swap logic
title_full Swap logic
title_fullStr Swap logic
title_full_unstemmed Swap logic
title_sort swap logic
publishDate 2021
url http://hdl.handle.net/11086/20427
https://doi.org/10.1093/jigpal/jzt030
work_keys_str_mv AT arecescarloseduardo swaplogic
AT fervariraulalberto swaplogic
AT hoffmannguillaumeemmanuel swaplogic
bdutipo_str Repositorios
_version_ 1764820391937703936

Ejemplares similares