The separation logic of relations (SLR) is a generalization of separation logic (SL) which is useful to describe complex structures like graphs and relational databases. SLR extends SL by interpreting heaps as (multi)sets of relational atoms instead of partial functions. This paper addresses the satisfiability problem for SLR formulas with additional shape constraints (called patterns) expressing conditions such as uniqueness of atoms or functionality of relations. We show that the satisfiability problem is \(\textsf {2}\hbox {-}\textsf {EXPTIME} \) -complete when (dis)equalities over existential variables are excluded from the considered patterns, and undecidable otherwise.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

The Satisfiability Problem in a Separation Logic of Relations

  • Nicolas Peltier

摘要

The separation logic of relations (SLR) is a generalization of separation logic (SL) which is useful to describe complex structures like graphs and relational databases. SLR extends SL by interpreting heaps as (multi)sets of relational atoms instead of partial functions. This paper addresses the satisfiability problem for SLR formulas with additional shape constraints (called patterns) expressing conditions such as uniqueness of atoms or functionality of relations. We show that the satisfiability problem is \(\textsf {2}\hbox {-}\textsf {EXPTIME} \) -complete when (dis)equalities over existential variables are excluded from the considered patterns, and undecidable otherwise.