Control Rules for Reactive System Games

Logic-Based Program Synthesis: State of the Art and Future Trends

Volume

Papers from the 2002 AAAI Spring Symposium

Contents

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 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.