Download PDFOpen PDF in browserThe Complexity of Prenex Separation Logic with One SelectorEasyChair Preprint 43320 pages•Date: August 16, 2018AbstractWe 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 firstorder theory of one unary function symbol and unary predicate symbols. We also prove that the complexity is not elementary, by reduction from the firstorder theory of one unary function symbol. Finally, we prove that the BernaysSch\"onfinkelRamsey fragment of prenex $\seplogk{1}$ formulae with quantifier prefix in the language $\exists^*\forall^*$ is \pspacecomplete. 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
