TY - JOUR
T1 - Falsification of Hybrid Systems Using Adaptive Probabilistic Search
AU - Ernst, Gidon
AU - Sedwards, Sean
AU - Zhang, Zhenya
AU - Hasuo, Ichiro
N1 - Funding Information:
The work is supported by JST ERATO HASUO Metamathematics for Systems Design Project (Grant No. JPMJER1603). Authors’ addresses: G. Ernst, Ludwig-Maximilians-University, Oettingenstraße 67, 80538 Munich, Germany; email: gidon. ernst@lmu.de; S. Sedwards, University of Waterloo, 200 University Avenue West, Waterloo, ON, Canada N2L 3G1; email: sean.sedwards@uwaterloo.ca; Z. Zhang and I. Hasuo, National Institute of Informatics, Palace Side Building 3F, Hitotsub-ashi 1-1-1, Tokyo 100-0003, Japan; emails: {zhangzy, hasuo}@nii.ac.jp. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. © 2021 Copyright held by the owner/author(s). Publication rights licensed to ACM. 1049-3301/2021/07-ART18 $15.00 https://doi.org/10.1145/3459605
Publisher Copyright:
© 2021 ACM.
PY - 2021/7
Y1 - 2021/7
N2 - We present and analyse an algorithm that quickly finds falsifying inputs for hybrid systems. Our method is based on a probabilistically directed tree search, whose distribution adapts to consider an increasingly fine-grained discretization of the input space. In experiments with standard benchmarks, our algorithm shows comparable or better performance to existing techniques, yet it does not build an explicit model of a system. Instead, at each decision point within a single trial, it makes an uninformed probabilistic choice between simple strategies to extend the input signal by means of exploration or exploitation. Key to our approach is the way input signal space is decomposed into levels, such that coarse segments are more probable than fine segments. We perform experiments to demonstrate how and why our approach works, finding that a fully randomized exploration strategy performs as well as our original algorithm that exploits robustness. We propose this strategy as a new baseline for falsification and conclude that more discriminative benchmarks are required.
AB - We present and analyse an algorithm that quickly finds falsifying inputs for hybrid systems. Our method is based on a probabilistically directed tree search, whose distribution adapts to consider an increasingly fine-grained discretization of the input space. In experiments with standard benchmarks, our algorithm shows comparable or better performance to existing techniques, yet it does not build an explicit model of a system. Instead, at each decision point within a single trial, it makes an uninformed probabilistic choice between simple strategies to extend the input signal by means of exploration or exploitation. Key to our approach is the way input signal space is decomposed into levels, such that coarse segments are more probable than fine segments. We perform experiments to demonstrate how and why our approach works, finding that a fully randomized exploration strategy performs as well as our original algorithm that exploits robustness. We propose this strategy as a new baseline for falsification and conclude that more discriminative benchmarks are required.
UR - http://www.scopus.com/inward/record.url?scp=85113861133&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85113861133&partnerID=8YFLogxK
U2 - 10.1145/3459605
DO - 10.1145/3459605
M3 - Article
AN - SCOPUS:85113861133
SN - 1049-3301
VL - 31
JO - ACM Transactions on Modeling and Computer Simulation
JF - ACM Transactions on Modeling and Computer Simulation
IS - 3
M1 - 3459605
ER -