时态运行时验证使用单调差分逻辑
摘要：运行时验证有时序运行上的有界时态逻辑的算法 基于时限运行的有界时态逻辑的运行时验证需要一个算法，该算法由三个部分组成。首先，需要将要验证的有界时态公式转化为差分不等式上的单调一阶逻辑，我们称之为单调差分逻辑。其次，在每个时限运行的步骤中，通过计算该步骤的状态和时间的商来修改单调差分公式。最后，通过单调差分逻辑的决策过程检查所得的公式是否为永真式或不可满足式。 我们进一步提供了一个基于数据结构差分决策图的简单的单调差分逻辑决策过程。该算法在一类严格单调一阶公式中具备很强的完备性，并在其他公式中具有近似性。近似性是因为并非所有的不可满足式或永真式能够在运行时验证的最早时刻被识别出来。 与现有方法相反，所提出的算法不通过句法重写而是利用高效的决策结构，使其适用于实际应用，例如商业软件。
作者：Henrik Reif Andersen and Kaare J. Kristoffersen
论文ID：0705.4604
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-06-01