Undecidability of Propositional Separation Logic and Its Neighbours
Undecidability of Propositional Separation Logic and Its Neighbours
复制标题
命题分离逻辑及其邻居的不可判定性
DOI：
10.1145/2542667
复制
发表时间：
2014
影响因子：
2.5
通讯作者：
Brotherston J
中科院分区：
文献类型：
--
作者：
Brotherston J
在这篇文章中，我们调查的逻辑结构的理论和实践兴趣的记忆模型。我们的主要兴趣是“固定内存模型背后的逻辑”，而不是“给定逻辑系统背后的任何类型的模型”。作为一种有效的语言推理这样的记忆模型，我们使用分离逻辑的形式主义。我们的主要结果是，对于任何具体选择的堆状记忆模型，该模型的有效性是不可判定的，即使是对于这种语言中的纯命题公式。我们解决这个问题的方法的主要新奇在于，我们专注于特定的，具体的记忆模型的有效性，而不是一般类别的模型的有效性。除了其内在的技术利益，这一结果还提供了对它们的可判定片段的性质的新的见解。特别地，我们证明了，为了获得这样的可判定片段，公式语言必须严格限制或命题变量的赋值必须受到约束。此外，我们还证明了一些近似分离逻辑的命题系统也是不可判定的。特别地，这解决了布尔BI和经典BI的可判定性问题。此外，我们通过将布尔逻辑的纯正蕴涵-合取片段与乘法 *-合取、其单位及其伴随蕴涵的定律相结合，最初由直觉乘法线性逻辑提供。这两个部分都是可判定的：布尔逻辑的蕴涵-合取片段是共NP-完全的，直觉乘法线性逻辑是NP-完全的，所有的不可判定性结果都是通过Minsky机的直接编码得到的。
In this article, we investigate the logical structure of memory models of theoretical and practical interest. Our main interest is in “the logic behind a fixed memory model”, rather than in “a model of any kind behind a given logical system”. As an effective language for reasoning about such memory models, we use the formalism of separation logic. Our main result is that for any concrete choice of heap-like memory model, validity in that model isundecidableeven for purely propositional formulas in this language.The main novelty of our approach to the problem is that we focus on validity in specific, concrete memory models, as opposed to validity in general classes of models.Besides its intrinsic technical interest, this result also provides new insights into the nature of their decidable fragments. In particular, we show that, in order to obtain such decidable fragments, either the formula language must be severely restricted or the valuations of propositional variables must be constrained.In addition, we show that a number of propositional systems that approximate separation logic are undecidable as well. In particular, this resolves the open problems of decidability for Boolean BI and Classical BI.Moreover, we provide one of the simplest undecidable propositional systems currently known in the literature, called “Minimal Boolean BI”, by combining the purely positive implication-conjunction fragment of Boolean logic with the laws of multiplicative *-conjunction, its unit and its adjoint implication, originally provided by intuitionistic multiplicative linear logic. Each of these two components is individually decidable: the implication-conjunction fragment of Boolean logic is co-NP-complete, and intuitionistic multiplicative linear logic is NP-complete.All of our undecidability results are obtained by means of a direct encoding of Minsky machines.
登录
查看更多内容
影响因子：
0.5
作者：
Galmiche, D;Méry, D;Pym, D
通讯作者：
Pym, D
通过阶段语义判断布尔 BI 的不可判定性
DOI：
10.1109/lics.2010.18
发表时间：
2010
期刊：
2010 25th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
Dominique Larchey;D. Galmiche
通讯作者：
D. Galmiche
具有二元模态的可判定和不可判定逻辑
DOI：
--
发表时间：
1995
期刊：
Journal of Logic, Language and Information
影响因子：
--
作者：
Á. Kurucz;I. Németi;I. Sain;András Simon
通讯作者：
András Simon
DOI：
10.1145/2103656.2103663
发表时间：
2012-01
期刊：
--
影响因子：
--
作者：
Philippa Gardner;S. Maffeis;Gareth Smith
通讯作者：
Philippa Gardner;S. Maffeis;Gareth Smith
关于分层存储的推理
DOI：
10.1109/lics.2003.1210043
发表时间：
2003
期刊：
18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings.
影响因子：
--
作者：
Amal J. Ahmed;Limin Jia;D. Walker
通讯作者：
D. Walker