The Complexity of Prenex Separation Logic with One Selector

EasyChair Preprint 433

Abstract

We first show that infinite satisfiability can be reduced to finite satisfiability for all prenex formulas of Separation Logic with $k\geq1$ selector fields ($\seplogk{k}$). Second, we show that this entails the decidability of the finite and infinite satisfiability problem for the class of prenex formulas of $\seplogk{1}$, 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\"onfinkel-Ramsey fragment of prenex $\seplogk{1}$ formulae with quantifier prefix in the language $\exists^*\forall^*$ is \pspace-complete. The definition of a complete (hierarchical) classification of the complexity of prenex $\seplogk{1}$, according to the quantifier alternation depth is left as an open problem.

Keyphrases: complexity, decidability, lists, magic wand, separation logic

@booklet{EasyChair:433,
  author    = {Mnacho Echenim and Radu Iosif and Nicolas Peltier},
  title     = {The Complexity of Prenex Separation Logic with One Selector},
  doi       = {10.29007/74ll},
  howpublished = {EasyChair Preprint 433},
  year      = {EasyChair, 2018}}