Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input
For engineers verifying safety-critical hybrid systems, this method offers a more efficient falsification tool.
The paper presents a probabilistically adaptive algorithm for falsifying hybrid systems against temporal logic requirements, achieving significantly faster falsification than existing techniques on standard benchmarks.
We present an algorithm that quickly finds falsifying inputs for hybrid systems, i.e., inputs that steer the system towards violation of a given temporal logic requirement. Our method is based on a probabilistically directed search of an increasingly fine grained spatial and temporal discretization of the input space. A key feature is that it adapts to the difficulty of a problem at hand, specifically to the local complexity of each input segment, as needed for falsification. In experiments with standard benchmarks, our approach consistently outperforms existing techniques by a significant margin. In recognition of the way it works and to distinguish it from previous work, we describe our method as a "Las Vegas tree search".