We use automata on infinite words to reduce the verification of linear temporal logic (\ltl) properties over infinite-state systems to the proof of first-order verification conditions and an algorithmic language inclusion check. The automaton serves as a temporal abstraction of the system, preserving a subset of both safety and liveness properties. The first-order verification conditions prove that the abstraction is conservative; the algorithmic check verifies that the abstraction satisfies the property. Automata precisely separate the combinatoric from the logic part of the proof, such that the combinatoric part can be handled completely by algorithmic methods.
In Proceedings of the7th Monterey Workshop: Modelling Software Systems Structures in a Fastly Moving Scenario, pp 226-237, Santa Margherita, 2000.