通过计时器与秩验证无穷状态系统的一阶时序性质

我们提出了一个基于良基秩的一阶时序性质的统一演绎验证框架，其中验证条件使用 SMT 求解器进行消解。为此，我们引入了一种从任意时序性质验证到终止性验证的新颖归约。我们的归约通过预言计时器变量来增强系统，这些变量预测沿着轨迹直到特定时序公式（包括被取反的性质）下一次成立时的步数。与将问题归约为公平终止的标准基于 tableau 的归约不同，我们的归约不引入公平性假设。为了验证增强系统的终止性，我们遵循传统方法，从良基集中为每个状态分配一个秩，并证明该秩在每次转换中递减。我们利用最近提出的隐式秩形式化方法，使用 SMT 求解器表达并自动验证秩的递减，即使该秩无法用一阶逻辑表达。我们将隐式秩从有限域扩展到无穷域，从而能够验证更一般的系统，并使其适用于由我们的归约生成的增强系统，这使我们能够在终止性证明中利用计时器的递减。我们在以往工作的一系列时序验证任务上评估了我们的技术，并在我们的框架内为它们提供了简单、直观的证明。