Fully-Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets

Reachability analysis is a formal method to guarantee safety of dynamical systems under the influence of uncertainties. A major bottleneck of all reachability algorithms is the requirement to adequately tune certain algorithm parameters such as the time step size, which requires expert knowledge. In this work, we solve this issue with a fully-automated reachability algorithm that tunes all algorithm parameters internally such that the reachable set enclosure satisfies a user-defined accuracy in terms of distance to the exact reachable set. Knowing the distance to the exact reachable set, an inner-approximation of the reachable set can be efficiently extracted from the outer-approximation using the Minkowski difference. Finally, we propose a novel verification algorithm that automatically refines the accuracy of the outer- and inner-approximation until specifications given by time-varying safe and unsafe sets can either be verified or falsified. The numerical evaluation demonstrates that our verification algorithm successfully verifies or falsifies benchmarks from different domains without any requirement for manual tuning.Comment: 16 page