关于度量时序逻辑在有限字上的可判定性与复杂度
计算机科学中的逻辑
2017-01-11 v3 计算复杂性
摘要
度量时序逻辑（Metric Temporal Logic, MTL）是实时系统的一种重要规约形式化方法。在本文中，我们证明了 MTL 在有限时间字上的可满足性问题是可判定的，其复杂度为非原始递归。我们还考虑了 MTL 的模型检测问题：即给定 Alur-Dill 时间自动机接受的所有字是否满足给定的 MTL 公式。我们证明该问题在有限字上是可判定的。对于无限字，我们证明了 MTL 的安全性片段——包括不变性和时间有界响应性质——的模型检测也是可判定的。这些结果相当令人惊讶，因为它们与文献中出现的各种相反声明相矛盾。
引用
@article{arxiv.cs/0702120,
title = {On the decidability and complexity of Metric Temporal Logic over finite words},
author = {Joel Ouaknine and James Worrell},
journal= {arXiv preprint arXiv:cs/0702120},
year = {2017}
}