The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Tree-like Grammars and Separation Logic
Christoph Matheja, Christina Jansen, and Thomas Noll
AIB 2015-12
Separation Logic with inductive predicate definitions (SL) and hyperedge
replacement grammars (HRG) are established formalisms to describe the
abstract shape of data structures maintained by heap-manipulating programs.
Fragments of both formalisms are known to coincide, and neither the
entailment problem for SL nor its counterpart for HRGs, the inclusion
problem, are decidable in general.
We introduce tree-like grammars (TLG), a fragment of HRGs with a
decidable inclusion problem.
By the correspondence between HRGs and SL, we simultaneously obtain an
equivalent SL fragment (SLTL) featuring some remarkable properties
including a decidable entailment problem.
