基于区间的命题时态逻辑的分层分析
摘要：提出了一种层次化框架，用于分析命题线性时态逻辑(PTL)，以获得标准结果，如小模型性质、决策过程和公理完备性。考虑了有限时间和无限时间，框架的一个重要优势是能够将无限时间推理系统地化简为有限时间推理。对带有“直到”运算符和过去时间的PTL的处理自然地简化为没有这两个运算符的PTL的处理。我们的方法利用了一种名为“转换配置”的PTL低层规范形式。此外，我们还使用时间间隔的推理。除了是层次化和基于间隔的之外，这种方法与其他基于公式集和这些集的序列的PTL分析方法不同。我们用有限和无限状态序列代表时间间隔来描述模型。分析将较大的时间间隔与较小的时间间隔关联起来。所涉及的步骤以命题间隔时态逻辑(PITL)表示，与PTL相比，PITL更适合顺序地组合和分解公式。因此，我们可以在PTL模型构建中阐述与传统分析同样相关但通常只在元层面考虑的问题。我们还描述了一种基于二进制决策图的决策过程。
作者：Ben Moszkowski
论文ID：cs/0601008
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23