This paper presents a deductive approach to the control problem for infinite-state reactive systems. It describes three proof rules, sound and relatively complete for formulas in the first two levels of the hierarchy of linear temporal logic---safety and response. The control conditions forming the premises of the rules are Π^0_2 first-order formulas. If a subroutine can prove their validity constructively, the extracted programs can be used to synthesize a winning strategy for the controller.
In 2002 AAAI Spring Symposium on Logic-Based Program Synthesis. AAAI Spring Symposium Technical Report SS-02-05, ISBN 1-57735-150-9, pp. 95–104.