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

arXiv: https://arxiv.org/abs/2610.19735 · HTML: https://mlsanity.com/paper/2610.19735/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 19 references that are in the map.
- First posted on arXiv 14 Oct 2026.

## Builds on (most cited first, 7 of 7)

- [Scenarios for Development, Test and Validation of Automated Vehicles](https://mlsanity.com/paper/1801.08598/) (2018)
- [Liability, Ethics, and Culture-Aware Behavior Specification using Rulebooks](https://mlsanity.com/paper/1902.09355/) (2019)
- [LawBreaker: An Approach for Specifying Traffic Laws and Fuzzing Autonomous Vehicles](https://mlsanity.com/paper/2208.14656/) (2022)
- [Formalizing Traffic Rules for Machine Interpretability](https://mlsanity.com/paper/2007.00330/) (2020)
- [Safety of the Intended Driving Behavior Using Rulebooks](https://mlsanity.com/paper/2105.04472/) (2021)
- [SceML - A Graphical Modeling Framework for Scenario-based Testing of Autonomous Vehicles](https://mlsanity.com/paper/2102.04241/) (2021)
- [Concretization of Abstract Traffic Scene Specifications Using Metaheuristic Search](https://mlsanity.com/paper/2307.07826/) (2023)

## Abstract (arXiv)

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.