Randomized Generation of Arbitrarily Difficult Verification Benchmarks for Linear Time-Invariant Systems

Benchmark proposal: The verification of uncertain linear systems is a fundamental building block for the analysis of complex cyber-physical systems. While there exist many advanced tools for numerical analysis, their evaluation is to date limited by selected bench- marks. To better understand the strengths and weaknesses of formal verification algorithms for linear systems, we propose a randomized generation of verification benchmarks in this paper. To this end, we leverage a reachability algorithm that can compute reachable sets with arbitrary precision. By placing unsafe sets exactly at the boundary of the computed outer and inner approximations, we are able to generate random verification tasks of ar- bitrary difficulty by changing the precision of the reachability analysis. We validate our approach by verifying and falsifying increasingly complex generated benchmarks using a state-of-the-art verification algorithm.