Benchmark: Reachability on a model with holes

Abstract

The benchmark presented in this paper is an example for verification of a hybrid system model with so-called holes, i.e. part of the system behaviour is not specified. Verification of such a model allows 3rd parties to plug a specific behaviour into a hole without changing desirable properties of the system. The particular example is based on an open-source robotics application, namely a self-balancing two-wheeled robot which is essentially modeled as an inverted pendulum. The balance controller provides two input signals for translational (forward/backward) and rotational (left/right turn) motion which can be driven by arbitrary path planning applications. Examples for such applications are line following and pursuit-evasion algorithms as well as a remote control which allows trajectories to be defined externally. These motion trajectories may or may not yield a state from which the balance controller is unable to recover, which means that the robot falls over. Hence, the verification goal is to prove the safety property that the body pitch angle is bounded under motion trajectories.