TY - GEN
T1 - Multi-armed Bandits for Boolean Connectives in Hybrid System Falsification
AU - Zhang, Zhenya
AU - Hasuo, Ichiro
AU - Arcaini, Paolo
N1 - Funding Information:
The authors are supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST.
Publisher Copyright:
© The Author(s). 2019.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85069874744&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85069874744&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-25540-4_23
DO - 10.1007/978-3-030-25540-4_23
M3 - Conference contribution
AN - SCOPUS:85069874744
SN - 9783030255398
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 401
EP - 420
BT - Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings
A2 - Dillig, Isil
A2 - Tasiran, Serdar
PB - Springer Verlag
T2 - 31st International Conference on Computer Aided Verification, CAV 2019
Y2 - 15 July 2019 through 18 July 2019
ER -