# Modal Separation Logic: an ongoing quest for elementary complexity

# Modal Separation Logic: an ongoing quest for elementary complexity

*Talk by Bartosz Bednarczyk*

- Location: TBA
- Start: 8. August 2018 at 1:00 pm
- End: 8. August 2018 at 2:00 pm
- Research group: Computational Logic
- Event series: KBS Seminar
- iCal

with Stephane and Raul Fervari (Universidad Nacional de Córdoba, Argentina) on Modal Separation Logic (MSL).

**Abstract:** Modal separation logic MSL is a logic introduced recently by Demri and Fervari
in [DF-aiml18], whose models are memory states as in separation logic and
the logical connectives include modal operators as well as separating
conjunction and magic wand. With these 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.
The decidability status and the computational complexity of several fragments
of MSL were established in [DF-aiml18], leading to surprising hardness or
easiness results, obtained by designing proof methods that take into
account the modal and separation features of MSL.

We will focus on a fragment of MSL, where only <>^{-1} (predecessor) and * (separating conjunction) operators are allowed. It is not hard to see that such a fragment is decidable by employing a theorem about decidability of MSO with one functional symbol. However the exact complexity of the logic remains unknown. During the talk I will present an approach to solve this problem by translating MSL into QCTL_EX, an extension of well-known CTL (where only EX operator is allowed) with propositional quantification. We will see how this approach failed, but as a sub-product we obtain several nice complexity and expressivity results for QCTL_EX. We will also see what makes QCTL_EX hard and why there is still a chance that the mentioned fragment of MSL could have an elementary complexity.

[DF-aiml18] S. Demri and R. Fervari. On the complexity of modal separation logics. In AiML'18. College Publications, August 2018. To appear.

**Bio:**Bartosz Bednarczyk - University of Wrocław & LSV ENS Paris-Saclay & University of Oxford