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

The talk will be dedicated to my recent work on Quantified Computation Tree Logic (QCTL) with Stephane Demri (LSV at ENS P-S, France) and my ongoing work

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