验证项重写系统抽象的时间正则性质

树自动机补全是一种用于证明可由项重写系统建模的系统安全性质的算法。这种表示和验证技术对于证明无限系统（如密码协议或最近的Java字节码程序）的性质非常有效。该算法计算一个树自动机，该自动机表示通过重写初始项所得到的可达项集合的（正则）过度逼近。这种方法受限于缺乏关于项之间重写关系的信息。实际上，通过重写相关联的项属于同一个等价类：它们被树自动机中的同一个状态识别。我们的目标是生成一个自动机，该自动机嵌入重写关系的抽象，足以证明项重写系统的时间性质。我们提出扩展该算法，以生成具有更多等价类的自动机，从而能够区分一个项或子项与其在重写意义上的后继。当使用基础转移来识别项的等价类时，ε-转移表示项之间的重写关系。从补全后的自动机，可以自动构建一个抽象重写序列的Kripke结构。Kripke结构的状态是树自动机的状态，转移关系由ε-转移集合给出。Kripke结构的状态由使用基础转移识别的项集合标记。在此Kripke结构上，我们定义了正则线性时序逻辑（R-LTL）来表达性质。然后可以使用标准模型检验算法来检验这些性质。LTL与R-LTL的唯一区别在于，谓词被替换为可接受项的正则集合。