We present a unified deductive verification framework for first-order temporal properties based on well-founded rankings, where verification conditions are discharged using SMT solvers. To that end, we introduce a novel reduction from verification of arbitrary temporal properties to verification of termination. Our reduction augments the system with prophecy timer variables that predict the number of steps along a trace until the next time certain temporal formulas, including the negated property, hold. In contrast to standard tableaux-based reductions, which reduce the problem to fair termination, our reduction does not introduce fairness assumptions. To verify termination of the augmented system, we follow the traditional approach of assigning each state a rank from a well-founded set and showing that the rank decreases in every transition. We leverage the recently proposed formalism of implicit rankings to express and automatically verify the decrease of rank using SMT solvers, even when the rank is not expressible in first-order logic. We extend implicit rankings from finite to infinite domains, enabling verification of more general systems and making them applicable to the augmented systems generated by our reduction, which allows us to exploit the decrease of timers in termination proofs. We evaluate our technique on a range of temporal verification tasks from previous works, giving simple, intuitive proofs for them within our framework.

翻译：本文提出一个基于良基秩函数的统一演绎验证框架，用于验证一阶时序性质，其验证条件可通过SMT求解器进行消解。为此，我们提出一种将任意时序性质验证归约为终止性验证的新方法。该归约方法通过引入预言计时器变量来增强系统，这些变量能够预测在轨迹上直至下一个满足特定时序公式（包括被否定性质）的步骤数。与基于标准Tableau的归约方法（将问题归约为公平终止性验证）不同，本方法不引入公平性假设。为验证增强系统的终止性，我们采用传统的秩函数方法：为每个状态分配一个来自良基集的秩值，并证明该秩值在每次状态转移时严格递减。我们利用最近提出的隐式秩函数形式体系，即使秩函数无法用一阶逻辑表达，仍可通过SMT求解器自动验证其递减性。我们将隐式秩函数从有限域扩展到无限域，从而能够验证更一般的系统，并使其适用于本归约方法生成的增强系统——这允许我们在终止性证明中利用计时器的递减特性。我们在多个先前工作中的时序验证任务上评估了本技术，并在本框架内为这些任务提供了简洁直观的证明。