Abstract:Cyber-physical system (CPS) is widely employed in safety-critical domains, making its safety assurance a critical concern. Formal verification serves as an effective approach for proving system safety but encounters challenges when applied to complex real-world CPS. Falsification has been proposed as an alternative, aiming to demonstrate system unsafety by identifying counterexample behaviors that violate specified safety properties. Existing path-oriented falsification methods for CPS utilize divide-and-conquer strategies to explore system behaviors along individual paths, effectively uncovering unsafe behaviors. However, in large-scale CPS, these methods are hindered by the path explosion problem, where the number of paths grows exponentially with the system’s discrete system modes, leading to significant reductions in falsification efficiency and performance. To address the path explosion issue in path-oriented falsification, this study introduces two novel techniques based on system models and specifications: path filtering and dynamic path selection. First, a specification-driven path filtering method is proposed to rapidly eliminate paths unlikely to contain unsafe behaviors by analyzing the syntax tree of system specifications and the behavioral constraints of each path. Second, a multi-armed bandit algorithm is adopted to guide the dynamic selection of paths during the falsification process, adaptively reallocating computational resources to optimize performance. Experimental evaluations on several classical benchmark cases demonstrate that the proposed techniques effectively mitigate the path explosion problem, significantly enhancing the efficiency and performance of CPS falsification. The success rate of identifying unsafe system behaviors improves by more than twofold.