Until算子的历史

Until是一个出了名难处理的时间算子，因为它同时具有存在性和全称性：A until B在当前时刻w成立当且仅当要么B在w成立，要么存在未来某个时刻w'使得B成立，并且A在从当前时刻到w'之间的所有时刻都成立。这种“矛盾”性质在试图为until给出演绎规则时构成了重大挑战。相比之下，在本文中，我们明确揭示了until的这种对偶性，通过引入一个新的时间算子来为线性时间逻辑提供良构的自然演绎规则，该算子允许我们形式化until的“历史”，即从当前时刻到w'之间的时间时刻上的“内部”全称量化。这种方法为形式化带有until算子的时间逻辑的演绎系统提供了基础。具体而言，我们在此给出了一个带有新算子的线性时间逻辑的标记自然演绎系统，并通过适当的翻译证明，该系统相对于带有until的线性时序逻辑LTL也是可靠且完备的。