Abstract

We describe a new algorithm for proving linear temporal properties of infinite-state systems. Our approach takes advantage of the fact that branching-time proof methods can sometimes be used to prove linear-time properties more efficiently than standard linear-time techniques can. The caveat is that, in certain instances, nondeterminism in the transition relation can cause branching-time methods to report counterexamples that are spurious in the linear-time semantics. To address this problem we describe an algorithm that, as it attempts to apply branching-time proof methods, finds and then removes problematic non-determinism via an analysis on the spurious counterexamples. Problematic nondeterminism is characterized using predicates, and removed using a predicate-based partial determinization procedure. Our method is sound and relatively complete.We demonstrate that our method can yield orders of magnitude performance improvements over native linear-time methods.