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.

翻译：时间特性的各种核查技术将时间核查转换为安全核查。 对于无限状态系统来说,这些转换本质上是不精确的。 在某些情况下, 时间属性持有, 但由此产生的安全属性并不精确。 本文引入了处理这种不精确性的机制。 我们称之为时间预言的这一机制受预言变量的启发。 时空预言通过一个合适的排列式构造, 利用一阶线性时间逻辑公式完善一个无限状态系统。 对于基于一阶逻辑的特定生存- 安全转换, 我们显示使用时间预言严格地提高了精确度。 此外, 时间预言导致证据方法的稳健性, 其表现为切除理论。 我们将我们的方法融入了常春化的参数核查系统, 并表明它能够处理具有挑战性的时间验证实例 。