Tags:Entailment problem, Induction, PCE fragment and Separation logic
Abstract:
The predicate definitions in Separation Logic (SL) play an important role: they introduce disjunctions and existential quantifications in fragments of SL not allowing the complete boolean fragment, and they capture a large spectrum of unbounded heap shapes due to their inductiveness. This expressiveness power comes with a limitation: the entailment problem is undecidable if predicates have general inductive definitions (ID). Iosif et al. proposed syntactic and semantic conditions, called PCE, on the ID of predicates to ensure the decidability of the entailment problem. We provide a (possibly non terminating) algorithm to transform arbitrary ID into equivalent PCE definitions, when possible. We show that the existence of an equivalent PCE definition for a given ID is undecidable, but we identify necessary conditions that are decidable.
What Is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?