Producción CyT
Congreso
Autoría
Fecha
2020
Editorial y Lugar de Edición
IEEE Press
Resumen
Información suministrada por el agente en
SIGEVA
We study the expressivity and complexity of two modal logics interpreted on finite forests and equipped with standardmodalities to reason on submodels. The logic ML( ) extendsthe modal logic K with the composition operator from ambient logic, whereas ML(∗) features the separating conjunction ∗ from separation logic. Both operators are second-orderin nature. We show that ML( ) is as expressive as the gradedmodal logic GML (on trees) whereas ML(∗) is strictly lessexpressive t...
We study the expressivity and complexity of two modal logics interpreted on finite forests and equipped with standardmodalities to reason on submodels. The logic ML( ) extendsthe modal logic K with the composition operator from ambient logic, whereas ML(∗) features the separating conjunction ∗ from separation logic. Both operators are second-orderin nature. We show that ML( ) is as expressive as the gradedmodal logic GML (on trees) whereas ML(∗) is strictly lessexpressive than GML. Moreover, we establish that the satisfiability problem is Tower-complete for ML(∗), whereasit is (only) AExpPol-complete for ML( ), a result which issurprising given their relative expressivity. As by-products,we solve open problems related to sister logics such as staticambient logic and modal separation logic.
Ver más
Ver menos
Palabras Clave
SEPARATION LOGICSGRADED MODAL LOGICSTATIC AMBIENT LOGICSMODAL LOGIC ON TREESEXPRESSIVITYCOMPLEXITY