The Complexity of Prenex Separation Logic with One Selector

EasyChair Preprint no. 433

20 pagesDate: August 16, 2018

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