Separation Logic with Monadic Inductive Definitions and Implicit Existentials

This paper proves the decidability of entailments in separation logic with monadic inductive definitions and implicit existentials. This system is obtained from the bounded-treewidth separation logic SLRDbtw of Iosif et al. in 2013 by adding implicit existential variables and restricting inductive definitions to monadic ones. The system proposed in this paper is a decidable system where one can use general recursive data structures with pointers as data, such as lists of pointers. The key idea is to reduce the problem to the decidability of SLRDbtw, by assigning local addresses or some distingu ished address to implicit existential variables so that the resulting definition clauses satisfy the establishment condition of SLRDbtw. This paper also proves the undecidability of the entailments when one adds implicit existentials to SLRDbtw. This shows that the implicit existentials are critical for the decidability.