使用 Presto 对重写逻辑理论进行符号特化

本文介绍 Presto，一个用于 Maude 重写逻辑理论的符号部分求值器，可改进系统分析与验证。在 Presto 中，条件重写理论 R（其规则定义系统的并发转移）的自动优化，是通过相对于 R 的规则对底层伴随等式逻辑理论 E 进行部分求值来实现的，其中 E 规定了 R 的系统状态的代数结构。当一个过于通用的等式理论 E 的算符可能服从结合、交换和/或单位元公理的复杂组合，并被插入宿主重写理论 R 时（例如协议分析中使用的复杂密码学等式理论），这尤其有用。Presto 实现了基于折叠变体缩窄（Maude 等式理论的符号引擎）的不同展开算符。当与适当的抽象算法结合时，它们使特化能适应理论的终止行为，并在确保特化的强正确性与终止的同时带来显著改进。我们在若干协议分析示例中展示了 Presto 的有效性，其实现了显著的加速。实际上，Presto 提供的变换可将无限的折叠变体缩窄空间削减为有限空间，并且一些代价高昂的代数公理与规则条件也可被消除。据我们所知，这是首个尊重函数式、逻辑式、并发式与面向对象计算语义的 Maude 部分求值器。已在 Theory and Practice of Logic Programming (TPLP) 审稿中。