  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.
