Abstract. The algorithmic design of least restrictive controllers for hybrid systems that satisfy reachability specifications has received much attention recently. Despite the importance of algorithmic approaches to controller design for hybrid systems, results that guarantee termination of the algorithms have been limited. In this paper, we extend recent decidability results on controller synthesis for classes of linear hybrid systems to semi-decision procedures for triangular hybrid systems which can be used to model nonholonomic systems after a transformation. Our results are then applied to verification of a conflict resolution maneuver from air traffic control.
Omid Shakernia, George J. Pappas, Shankar Sastry