English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Various verification techniques for temporal properties transform temporalverification to safety verification. For infinite-state systems, thesetransformations are inherently imprecise. That is, for some instances, thetemporal property holds, but the resulting safety property does not. This paperintroduces a mechanism for tackling this imprecision. This mechanism, which wecall temporal prophecy, is inspired by prophecy variables. Temporal prophecyrefines an infinite-state system using first-order linear temporal logicformulas, via a suitable tableau construction. For a specificliveness-to-safety transformation based on first-order logic, we show thatusing temporal prophecy strictly increases the precision. Furthermore, temporalprophecy leads to robustness of the proof method, which is manifested by a cutelimination theorem. We integrate our approach into the Ivy deductiveverification system, and show that it can handle challenging temporalverification examples.

Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems