自然数上区间时态逻辑ABBar的可判定性
计算机科学中的逻辑
2010-02-03 v2
摘要
本文关注Allen关系“相遇”、“开始”和“被开始”的区间时态逻辑（简称ABBar），该逻辑在自然数上解释。我们首先介绍该逻辑，并证明其表达能力足以建模独特的区间性质（如完成条件）、捕获基于点的时态逻辑的基本模态（如until算子）以及编码相关的度量约束。然后，我们通过提供一种基于原创收缩方法的小模型定理，证明ABBar在自然数上的可满足性问题可判定。最后，我们证明该问题是EXPSPACE完全的。
引用
@article{arxiv.0912.3429,
title = {Decidability of the interval temporal logic ABBar over the natural numbers},
author = {A. Montanari and G. Puppis and P. Sala and G. Sciavicco},
journal= {arXiv preprint arXiv:0912.3429},
year = {2010}
}