MakSafe: A Spatiotemporal Semantic Framework for Formal Specification and Compliance Checking of Road Vehicle Safety Rules
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 ver...
| Authors | Maksym Labzhaniia, Julien Deantoni, Marie-Agn{è}s Peraldi-Frati et al. |
|---|---|
| Primary category | cs.CL |
| Published | 14 October 2026 |
| Last updated at source | 14 October 2026 |
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 15 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.