We use alternating automata on infinite words to reduce the verification of linear temporal logic LTL safety properties over infinite-state systems to the proof of first-order verification conditions. This method generalizes the traditional deductive verification approach of providing verification rules for particular classes of formulas, such as invariances, nested precedence formulas, etc. It facilitates the deductive verification of arbitrary safety properties without the need for explicit temporal reasoning.
In Proc. 27th Intl. Colloq. Aut. Lang. Prog., LNCS 1853, Springer-Verlag, pp 429-450, 2000.
Postscript, PDF. © 2000, Springer Verlag.