New Frontiers for LTL

We describe a new algorithm for proving linear temporal properties of infinite-state systems. Our approach takes advantage of the fact that state-based (a.k.a. branching-time) proof methods can sometimes be used to prove linear temporal properties more efficiently than known trace-based (a.k.a. linear-time) techniques can. The caveat is that, in certain instances, nondeterminism in the system’s transition relation can cause state-based methods to report counterexamples that are spurious in the linear temporal logic’s semantics. To address this problem I will describe an algorithm that, as it attempts to apply state-based proof methods, finds and then removes problematic non-determinism via an analysis on the spurious counterexamples. Problematic nondeterminism is characterized using decision predicates, and removed using a partial determinization procedure that introduces new prophecy variables to predict the future outcome of the decisions. Time permitting I'll also discuss a curious consequence of this idea to the area of proving recursive programs terminating.