Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search

Few real-world hybrid systems are amenable to formal verification, due to their complexity and black box components. Optimization-based falsification-a methodology of search-based testing that employs stochastic optimization-is thus attracting attention as an alternative quality assurance method. Inspired by the recent work that advocates coverage and exploration in falsification, we introduce a two-layered optimization framework that uses Monte Carlo tree search (MCTS), a popular machine learning technique with solid mathematical and empirical foundations (e.g., in computer Go). MCTS is used in the upper layer of our framework; it guides the lower layer of local hill-climbing optimization, thus balancing exploration and exploitation in a disciplined manner. We demonstrate the proposed framework through experiments with benchmarks from the automotive domain.