Various verification techniques for temporal properties reduce temporal verification to safety verification. For infinite-state systems, these reductions are inherently incomplete. That is, for some instances, the temporal property is correct, but the resulting safety property is not. This paper introduces a mechanism for tackling this incompleteness. This mechanism, which we call \emph{temporal prophecy}, is inspired by prophecy variables. Temporal prophecy refines an infinite-state system using temporal formulas, via a suitable tableau construction. For a specific liveness to safety reduction based on first-order logic, where temporal prophecy is defined via first-order linear temporal logic, we show that using temporal prophecy strictly increases the proof power of the reduction. 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.
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems