Control Rules for Reactive System Games

Matteo Slanina

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.