Halpern-Shoham区间时序逻辑的Horn片段（技术报告）
计算机科学中的逻辑
2017-08-29 v5 计算复杂性
摘要
我们研究了Halpern-Shoham区间时序逻辑的Horn片段的可满足性问题，该问题依赖于区间模态算子的类型（box或diamond）、底层线性序的类型（离散或稠密）以及区间关系的语义类型（自反或非自反）。例如，我们证明了带有diamond的Horn公式的可满足性对于任意类型的线性序和语义都是不可判定的。相反，带有box的Horn公式的可满足性在自反语义下的离散和稠密序上以及非自反语义下的稠密序上是可处理的，但在非自反语义下的离散序上变得不可判定。同时带有box和diamond的二元Horn公式的可满足性在非自反语义下总是不可判定的。
引用
@article{arxiv.1604.03515,
title = {Horn Fragments of the Halpern-Shoham Interval Temporal Logic (Technical Report)},
author = {Davide Bresolin and Agi Kurucz and Emilio Muñoz-Velasco and Vladislav Ryzhikov and Guido Sciavicco and Michael Zakharyaschev},
journal= {arXiv preprint arXiv:1604.03515},
year = {2017}
}