cs.CLOct 14, 2026

MakSafe: A Spatiotemporal Semantic Framework for Formal Specification and Compliance Checking of Road Vehicle Safety Rules

Authors: Maksym Labzhaniia, Julien Deantoni, Marie-Agn{è}s Peraldi-Frati, Fr{é}d{é}ric Mallet

Organizations: UniCA, Laboratoire I3S - COMRED, KAIROS · Laboratoire I3S - COMRED, I3S, KAIROS, UniCA

Abstract

Scenario-based validation is essential for automated road vehicles but cannot cover the full variability of openworld traffic. We present MakSafe, a formal spatiotemporal framework for specifying and checking road vehicle safety rules through semantic zones, action-based forecasting, and trace-tree reasoning, avoiding uniform time discretization. We formalize the road network, vehicle states, and occupancy zones, then build executable rules for front-vehicle identification and timeto-collision (TTC) verification. The evaluation combines a tracedependent case study with a scalability benchmark over traffic density (N ), horizon (H), and branch factor (B). MakSafe yields branch-specific verdicts, deriving safe and unsafe outcomes from the same initial scene, and re-evaluates a scenario after a control update. A single rule check stays well below a millisecond across the reported sweep, and longer horizons slow the TTC check.

Explore similar work

CardsList
  1. Scenario-Based Compositional Statistical Model Checking for Safety Specifications

    Oct 4, 2026Abhinav Pomalapally, Arya Raeesi, Kevin Kai-Chun Chang +2Statistical Model CheckingFormal Verification

  2. The Field of Safe Motion: Operationalizing Affordances in the Field of Safe Travel Using Reachability Analysis

    Apr 29, 2026Leif Johnson, Trent Victor, Johan EngströmCollision AvoidanceSafe Motion Planning

  3. TrafficSignBench: Rule-Centric Closed-Loop Evaluation of Traffic-Sign Compliance in Autonomous Driving

    Sep 29, 2026Victoria Smirnova, Viktoriia Zinkovich, Gregorii Bukhtuev +4Autonomous Driving BenchmarksAutonomous Driving Safety Evaluation