Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings

TL;DR

This paper introduces a novel deductive verification framework for first-order temporal properties of infinite-state systems, utilizing timers, rankings, and SMT solvers to reduce temporal verification to termination proofs without fairness assumptions.

Contribution

It presents a new reduction from temporal property verification to termination, extending implicit rankings to infinite domains, and demonstrating practical verification of complex temporal properties.

Findings

Effective verification of temporal properties using timers and rankings.

Extension of implicit rankings to infinite domains.

Successful evaluation on diverse temporal verification tasks.

Abstract

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.