Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates
share
We establish various complexity results for the entailment problem between formulas in Separation Logic with user-defined predicates denoting recursive data structures. The considered fragments are characterized by syntactic conditions on the inductive rules that define the semantics of the predicates. We focus on so-called P-rules, which are similar to (but simpler than) the PCE rules introduced by Iosif et al. in 2013. In particular, for a specific fragment where predicates are defined by so-called loc-deterministic inductive rules, we devise a sound and complete cyclic proof procedure running in polynomial time. Several complexity lower bounds are provided, showing that any relaxing of the provided conditions makes the problem intractable.
READ FULL TEXT