The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions

The entailment between separation logic formulae with inductive predicates (also known as symbolic heaps) has been shown to be decidable for a large class of inductive definitions [4]. Recently, a 2EXPTIME algorithm has been proposed [7], however no precise lower bound is known (although a EXPTIME-hard bound for this problem has been established in [5]). In this paper, we show that deciding entailment between predicate atoms is 2EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines [3]