Room 206 (2nd floor, badged access)
5 avril 2019 - 14h00
On the Expressive Completeness and Complexity of Prenex Separation Logic
par Radu IOSIF de VERIMAG
Abstract: This talk investigates the satisfiability problem for Separation Logic, with unrestricted nesting of separating conjunctions and implications, for prenex formulae, in the cases where the universe of possible locations is either countably infinite or finite. If the quantifier prefix is in the language exists*forall*, we call this fragment Bernays-Schönfinkel-Ramsey Separation Logic [BSR(SLk)].
In the first part of the talk, we show that, unlike in first-order logic, the (in)finite satisfiability problem is undecidable for BSR(SLk) and we define two non-trivial subsets thereof, that are decidable for finite and infinite satisfiability, respectively, by controlling the occurrences of universally quantified variables within the scope of separating implications, as well as the polarity of the occurrences of the latter. The decidability results are obtained by a controlled elimination of separating connectives, described as (i) an effective translation of a prenex form Separation Logic formula into a combination of a small number of emph{test formulae}, using only first-order connectives, followed by (ii) a translation of the latter into an equisatisfiable first-order formula.
In the second part of the talk, we show that infinite satisfiability can be reduced to finite satisfiability for all prenex formulas of Separation Logic with k≥1 selector fields (SLk). Then, we show that this entails the decidability of the finite and infinite satisfiability problem for the class of prenex formulas of $SL1$, by reduction to the first-order theory of one unary function symbol and unary predicate symbols. We also prove that the complexity is not elementary, by reduction from the first-order theory of one unary function symbol. Finally, we prove that the Bernays-Schönfinkel-Ramsey fragment of prenex $SL1$ is pspace-complete. The definition of a complete (hierarchical) classification of the complexity of prenex $SL1$, according to the quantifier alternation depth is left as an open problem.
This is joint work with Nicolas Peltier and Mnacho Echenim (LIG). A short version of this talk will be presented at FOSSACS'19
