Periodically controlled hybrid systems: Verifying a controller for an autonomous vehicle

Abstract. This paper introduces Periodically Controlled Hybrid Au-tomata (PCHA) for describing a class of hybrid control systems. In a PCHA, control actions occur roughly periodically while internal and in-put actions, may occur in the interim changing the discrete-state or the setpoint. Based on periodicity and subtangential conditions, a new suf-ficient condition for verifying invariance of PCHAs is presented. This technique is used in verifying safety of the planner-controller subsystem of an autonomous ground vehicle, and in deriving geometric properties of planner generated paths that can be followed safely by the controller under environmental uncertainties