On July 19, 2022 at 14:00 EEST, Radu Iosif (CNRS – VERIMAG) will give a talk in the Logic Seminar.
Title: On the Expressiveness of a Logic of Separated Relations
Abstract: We compare the model-theoretic expressiveness of the existential fragment of Separation Logic over unrestricted relational signatures (SLR) with only separating conjunction as logical connective and higher-order inductive definitions, traditionally known as the symbolic heap fragment, with (Monadic) Second Order Logic ((M)SO). While SLR and MSO are incomparable on structures of unbounded treewidth, it turns out that SLR can be embedded in SO, in general, and that MSO becomes a strict subset of SLR, when the treewidth of the models is bounded by a parameter given as input. We also discuss the problem of defining a fragment of SLR that is equivalent to MSO over models of bounded treewidth. Such a fragment would then become the most general Separation Logic with a decidable entailment problem, a key ingredient of practical verification methods for self-adapting (reconfigurable) component-based and distributed systems. Joint work with Florian Zuleger (TU Wien).
The talk will take place at FMI Hall 214 “Google”; it will also be transmitted online as usual.
Google Meet link: https://meet.google.com/xwm-syvx-bbr