Technical reportIOSIF Radu, ROGALEWICZ Adam and ŠIMÁČEK Jiří. The Tree Width of Separation Logic with Recursive Definitions. arXiv:1301.5139, 2013.  Publication language:  english 

Original title:  The Tree Width of Separation Logic with Recursive Definitions 

Title (cs):  Omezená stromová šířka v separační logice s rekursivními definicemi 

Pages:  31 

Place:  arXiv:1301.5139, US 

Year:  2013 

URL:  http://arxiv.org/abs/1301.5139 [HTML] 

Annotation 

Separation Logic is a widely used formalism for describing dynamically allocated linked data structures, such as lists, trees, etc. The decidability status
of various fragments of the logic constitutes a long standing open
problem. Current results report on techniques to decide satisfiability
and validity of entailments for Separation Logic(s) over lists (possibly
with data). In this paper we establish a more general decidability
result. We prove that any Separation Logic formula using rather general
recursively defined predicates is decidable for satisfiability, and
moreover, entailments between such formulae are decidable for validity.
These predicates are general enough to define (doubly) linked lists,
trees, and structures more general than trees, such as trees whose
leaves are chained in a list. The decidability proofs are by reduction
to decidability ofMonadic Second Order Logic on graphs with bounded tree
width. 
BibTeX: 

@TECHREPORT{
author = {Radu Iosif and Adam Rogalewicz and Ji{\v{r}}{\'{i}}
{\v{S}}im{\'{a}}{\v{c}}ek},
title = {The Tree Width of Separation Logic with Recursive
Definitions},
pages = {31},
year = {2013},
location = {arXiv:1301.5139, US},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=10311}
} 
