Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification (Extended Version)
For researchers and practitioners in cyber-physical system verification, this work provides a solution to a known bottleneck in falsification, though the improvement is incremental.
The paper addresses the scale problem in hybrid system falsification, where different scales of quantities can mask each other's contribution to robustness. The authors integrate multi-armed bandit algorithms with a new reward notion called hill-climbing gain, and show that their approach outperforms a state-of-the-art falsification tool in robustness under scale changes.
Hybrid system falsification is an actively studied topic, as a scalable quality assurance methodology for real-world cyber-physical systems. In falsification, one employs stochastic hill-climbing optimization to quickly find a counterexample input to a black-box system model. Quantitative robust semantics is the technical key that enables use of such optimization. In this paper, we tackle the so-called scale problem regarding Boolean connectives that is widely recognized in the community: quantities of different scales (such as speed [km/h] vs. RPM, or worse, RPH) can mask each other's contribution to robustness. Our solution consists of integration of the multi-armed bandit algorithms in hill climbing-guided falsification frameworks, with a technical novelty of a new reward notion that we call hill-climbing gain. Our experiments show our approach's robustness under the change of scales, and that it outperforms a state-of-the-art falsification tool.