Verification of Hybrid Systems: Monotonicity in the AHS Control System

Numerous approaches to verifying the safety of vehicles in the AHS architecture of PATH have been proposed (see [1] and [2]). One approach involves finding a boundary between safe and unsafe initial conditions. This task is significantly easier if we can guarantee that the severity of an accident is monotonic in the initial conditions. Simulation results are presented in which it is shown that this condition does not hold for the design of [1], and a hybrid automaton model explaining this situation is presented. Finally, some attempts to modify the control laws to obtain monotonicity are presented