Science and Technology Production
Congress
Authorship
Date
2020
Publishing House and Editing Place
IEEE Press
Summary
Information provided by the agent in
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.
Show more
Show less
Key Words
SEPARATION LOGICSGRADED MODAL LOGICSTATIC AMBIENT LOGICSMODAL LOGIC ON TREESEXPRESSIVITYCOMPLEXITY