Logic-Guided Optimization Metaheuristics in Hybrid System Falsification and Parameter Tuning

Hybrid system falsification attracts industrial attention as a black-box quality assurance method for cyber-physical systems. It is a search-based testing technique where one searches for counterexample input using optimization metaheuristics; notably, the search is with respect to a logical specification translated to a quantitative “robustness” function. In the talk, I will exhibit our recent work that exploits logical structures not only for formulating objectives but also in search heuristics. Our basic strategy is layered optimization: on top of the continuous optimization metaheuristics commonly employed for hybrid system falsification (e.g. stochastic hill-climbing), we add a discrete optimization layer that exploits logical structures and gives high-level structural guidance to the lower-level optimization engine. I believe this is one of the emerging usages of logic in the era of cyber-physical systems where white-box system models are a rarity. The talk is based on the following papers:

• Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini: Multi-armed Bandits for Boolean Connectives in Hybrid System Falsification. CAV (1) 2019: 401-420
• Zhenya Zhang, Gidon Ernst, Sean Sedwards, Paolo Arcaini, Ichiro Hasuo: Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(11): 2894-2905 (2018) (Proc. EMSOFT 2018)
• Sota Sato, Atsuyoshi Saimen, Masaki Waga, Kenji Takao, Ichiro Hasuo: Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: A Gas Turbine Case Study. FM 2021: 313-329

(The talk might not be especially long, perhaps 30-45 minutes.)

Zoom link: