区间时序逻辑模型检测的复杂性：区间逻辑HS的一些良态片段
计算机科学中的逻辑
2016-01-25 v1 计算复杂性
数据结构与算法
摘要
模型检测已成功应用于包括人工智能、理论计算机科学和数据库在内的许多计算机科学领域。大多数提出的解决方案使用经典的、基于点的时序逻辑，而在区间时序逻辑方面的研究很少。近年来，提出了一种用于有限 Kripke 结构（在齐性假设下）上的 Halpern 和 Shoham 区间模态逻辑 HS 的非初等模型检测算法，以及针对其中两个有意义片段的 EXPSPACE 模型检测过程。本文中，我们展示了可以为 HS 的一些表达力足够的片段开发更高效的模型检测过程。
引用
@article{arxiv.1601.03202,
title = {Complexity of ITL model checking: some well-behaved fragments of the interval logic HS},
author = {A. Molinari and A. Montanari and A. Peron},
journal= {arXiv preprint arXiv:1601.03202},
year = {2016}
}