Property-Guided Cyber-Physical Reduction and Surrogation for Safety Analysis in Robotic Vehicles

TL;DR

The paper tackles the verification bottleneck in cyber-physical robotic systems by introducing a property-guided reduction framework that yields a property-specific surrogate combining cyber-space pruning with physical model simplification. It formalizes a two-pronged reduction using hybrid dynamical systems for control logic and static condensation for physical dynamics, ensuring trace-level equivalence with respect to the target property. A temporal logic oracle guides falsification over the reduced model, and a co-reduction workflow enables efficient, property-targeted fuzzing validated on a drone parachute deployment case. Empirically, the surrogate reproduces the full-system safety violations with dramatically lower runtime, enabling scalable analysis and actionable diagnostics, while preserving semantic fidelity across the property-relevant slice of the system.

Abstract

We propose a methodology for falsifying safety properties in robotic vehicle systems through property-guided reduction and surrogate execution. By isolating only the control logic and physical dynamics relevant to a given specification, we construct lightweight surrogate models that preserve property-relevant behaviors while eliminating unrelated system complexity. This enables scalable falsification via trace analysis and temporal logic oracles. We demonstrate the approach on a drone control system containing a known safety flaw. The surrogate replicates failure conditions at a fraction of the simulation cost, and a property-guided fuzzer efficiently discovers semantic violations. Our results suggest that controller reduction, when coupled with logic-aware test generation, provides a practical and scalable path toward semantic verification of cyber-physical systems.

Figures (3)

• Figure 1: Overview of our cyber-physical reduction methodology for safety analysis of robotic vehicles. The approach combines control logic reduction with physical model reduction through static condensation to create an efficient, property-specific surrogate system.
• Figure 2: Full-System Flight Trajectory. PyBullet-based simulation trace showing 3D descent profile after battery low warning. But the drone does not deploy the parachute due to a bug in the emergency controller. Simulation took 24.7 seconds and required complete system execution.
• Figure 3: Battery safety margin vs. altitude-directed safety margin for 200 autonomous runs. Each point is one run: green circles indicate that the safety property was satisfied, and orange crosses indicate a violation (80/200 runs, 40%). The battery safety margin on the $x$-axis is the observed battery level relative to the mission low-battery threshold ($M_{\mathrm{bat}} = \text{battery level} - \text{threshold}$); larger values indicate more remaining battery. The altitude-directed margin on the $y$-axis is the signed distance to the nearest allowed deployment altitude limit; positive values indicate that the vehicle is above the maximum allowed deployment altitude, negative values indicate that it is below the minimum allowed deployment altitude, and $0$ corresponds to contact with a limit. Dashed lines mark the controller's battery threshold (vertical) and safe-altitude boundary (horizontal). Shaded quadrants ($Q1$--$Q4$) separate high/low battery and high-/low-side altitude regimes. Violations cluster where the battery margin is low and the vehicle is outside the allowed altitude band (either too low or too high), showing that the parachute deployment logic is incorrectly inhibited whenever altitude is out of range, even under critical battery conditions where deployment should be unconditional.