Robust Spatio-Temporal Logic Semantics for Autonomous Driving Systems Falsification

Traditional industrial testing methods often fail to guarantee that a system behaves as expected due to the resource cost of exhaustively searching for defects. To minimize this cost, a promising alternative called robustness-guided falsification is emerging as a less exhaustive method that can handle the increasing complexity of autonomous driving systems. This approach attempts to identify counterexamples to a given system property by treating testing as an optimization problem with a robustness function to be minimized. This function quantifies how well the system satisfies a given property encoded as a logical formula, with values that indicate how close the system is to violating the property. In this paper, we apply robustness-guided falsification to a particular type of spatio-temporal logic, LTL × MS^≤, which integrates both temporal and spatial modalities to describe system behavior across time and space. We establish a correspondence between the Boolean semantics of the “subset or equal” relation and the degrees of robustness with signed Hausdorff distances, propose a robust semantics for LTL × MS^≤, and demonstrate how robustness-guided falsification can be applied to properties expressed in this logic. To evaluate our approach, we conducted an empirical case study in a traffic scenario. The results demonstrate the feasibility of this approach in falsifying spatio-temporal properties and support the adoption of counterexample generation for the verification of defects in realistic autonomous driving systems.