The Complexity of Prenex Separation Logic with One Selector

TL;DR

This paper investigates the satisfiability and complexity of prenex separation logic with one selector, establishing decidability results and complexity bounds, including a extsc{pspace}-completeness result for a specific fragment.

Contribution

It reduces infinite satisfiability to finite for prenex formulas with one or more selectors and characterizes the complexity of these formulas, including a extsc{pspace}-complete fragment.

Findings

Finite satisfiability reduces to infinite satisfiability for all prenex formulas with $k extgreater=1$ selectors.

Decidability of satisfiability for prenex formulas with one selector via reduction to first-order logic.

The Bernays-Sch"onfinkel-Ramsey fragment with $orall^* oorall^*$ quantifier prefix is extsc{pspace}-complete.

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.