Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems

TL;DR

This paper introduces temporal prophecy, a new method that refines infinite-state systems with first-order temporal logic to improve the precision of temporal property verification, enhancing robustness and handling complex examples.

Contribution

It presents a novel mechanism called temporal prophecy that refines infinite-state systems, increasing verification precision and robustness through a new tableau-based approach.

Findings

Temporal prophecy increases verification precision for infinite-state systems.

The approach leads to a cut elimination theorem, enhancing proof robustness.

Successfully integrated into Ivy, handling challenging temporal verification cases.

Abstract

Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but the resulting safety property does not. This paper introduces a mechanism for tackling this imprecision. This mechanism, which we call temporal prophecy, is inspired by prophecy variables. Temporal prophecy refines an infinite-state system using first-order linear temporal logic formulas, via a suitable tableau construction. For a specific liveness-to-safety transformation based on first-order logic, we show that using temporal prophecy strictly increases the precision. Furthermore, temporal prophecy leads to robustness of the proof method, which is manifested by a cut elimination theorem. We integrate our approach into the Ivy deductive verification system, and show that it can handle challenging temporal verification examples.