On the Complexity of Modal Separation Logics - Laboratoire Méthodes Formelles Access content directly
Conference Papers Year : 2018

On the Complexity of Modal Separation Logics

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, leading to surprising results, obtained by designing 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 inequality modality Diff and separating conjunction * is shown Tower-complete whereas the restriction either to <> and * or to Diff and * is only NP-complete.
Fichier principal
Vignette du fichier
DF-aiml18.pdf (691.07 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02366671 , version 1 (16-11-2019)

Identifiers

  • HAL Id : hal-02366671 , version 1

Cite

Stephane Demri, Raul Fervari. On the Complexity of Modal Separation Logics. Advances in Modal Logic, Bern, 2018, Aug 2018, Bern, Switzerland. ⟨hal-02366671⟩
65 View
83 Download

Share

Gmail Facebook X LinkedIn More