LTL表的一个新规则
A New Rule for LTL Tableaux
摘要：
命题线性时态逻辑（Propositional Linear Time Temporal Logic，LTL）是一种面向计算应用的标准时态逻辑，许多推理技术和工具已经被开发出来。然而，这种逻辑的tableaux看起来不像传统的树形tableau系统，它们的处理通常非常复杂。在本文中，我们介绍了一种新的风格的tableau规则，支持一个新的简单的传统风格的树形tableau LTL。我们证明它是健全和完整的。除了易于理解，向学生介绍和使用外，它还易于实现，并且与最先进的系统相比具有竞争力。它特别适合于并行实现。
英文摘要：
Propositional linear time temporal logic (LTL) is the standard temporal logic for computing applications and many reasoning techniques and tools have been developed for it. Tableaux for deciding satisfiability have existed since the 1980s. However, the tableaux for this logic do not look like traditional tree-shaped tableau systems and their processing is often quite complicated. In this paper, we introduce a novel style of tableau rule which supports a new simple traditional-style tree-shaped tableau for LTL. We prove that it is sound and complete. As well as being simple to understand, to introduce to students and to use, it is also simple to implement and is competitive against state of the art systems. It is particularly suitable for parallel implementations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
