TPTL 与 TPTLb+Past 的一次遍历树形表系统
计算机科学中的逻辑
2018-09-11 v1
摘要
本文针对定时命题时序逻辑（Timed Propositional Temporal Logic, TPTL）及其带过去算子的扩展的有界变体，提出了一种新颖的一次遍历树形表方法。TPTL 是一种实时时序逻辑，其可满足性问题为 EXPSPACE 完全，已成功应用于实时系统的验证。与 LTL 不同，向 TPTL 添加过去算子使得所得逻辑（TPTL+P）的可满足性问题成为非初等。本文为 TPTL 和有界 TPTL+P（TPTLb+P）设计了一种一次遍历树形表，后者是为编码基于时间线的规划问题而引入的语法限制，恢复了 EXPSPACE 完全复杂度。TPTL 与 TPTLb+P 的表系统以统一方式呈现，彼此非常相似，提供了一个共同骨架后再特化到各逻辑。在此过程中，我们将 TPTLb+P 的语义刻画为 TPTL+P 的一个纯语法片段，并给出将前者嵌入后者的翻译。系统的可靠性与完备性均被完全证明。特别地，我们给出了极大简化的模型论完备性证明，规避了已知 LTL 与 LTL+P 的一次遍历树形表证明中使用的复杂组合论证。
引用
@article{arxiv.1809.03101,
title = {One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past},
author = {Luca Geatti and Nicola Gigante and Angelo Montanari and Mark Reynolds},
journal= {arXiv preprint arXiv:1809.03101},
year = {2018}
}
备注
In Proceedings GandALF 2018, arXiv:1809.02416