A Hybrid Automaton-Based Vehicle Digital Twin for Verifiable Pedestrian Protection

Autonomous vehicles must make reliable safety decisions despite perception noise and tighttiming constraints. This work presents a Vehicle Digital Twin (VDT) architecture that incorporates a formallyverified hybrid automaton as its supervisory controller. The automaton specifies discrete safety modes,continuous timing variables, and perception-driven transitions, and is verified offline using SMT-based LTLmodel checking to ensure determinism, freedom from deadlock, and bounded reaction time. At runtime,buffered perception inputs and staleness checks are used to trigger only those transitions consistent withthe verified model, maintaining robustness to noisy or transient detections. We instantiate the approach forpedestrian-protection and evaluate it on standardized Euro NCAP scenarios within CARLA. The systemconsistently produces stable and interpretable braking decisions and maintains reaction times within theverified bounds, including under perception uncertainty. These results indicate that integrating a verifiedhybrid automaton directly into the VDT’s operational loop is a practical route toward runtime-assured safetysupervision in perception-driven vehicle systems.