ModelPlex uses theorem proof and differential dynamic logic to generate a safe condition offline. In the online part, such a condition can be used as a monitor to check state for model compliance and check the safety of the control. However, such a condition is normally conservative. In our RL-based Dubins path-following control problem, it requires the vehicle to follow a path with very small deviations. In this work, we allow the controller to mildly violate the safety condition, but do not allow a large violation. Forward reachability analysis is used to predict whether the violation will lead the vehicle to enter a forbidden state in the short-term future. We also leverage a robust model predictive controller to recover the vehicle’s pose from potentially dangerous situations to the safe zone defined by the ModelPlex monitor.

To sum up: 1) If we only use the ModelPlex monitor, we can have safety and liveness (i.e., the waypoint will eventually be reached) guarantees. But the safe condition is over-conservative, so a fallback controller will be frequently invoked even for a small violation. 2) If we only use reachability analysis, we can only have a short-term safety guarantee. Our integration work simultaneously provides a safety guarantee and mitigates the over-conservativeness problem with minimum fallback control interventions.

Keywords:  ModelPlex monitor; forward reachability analysis; recovery tube; robust tube MPC