# Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle Obligations

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 46 references that are in the map.
- First posted on arXiv 6 May 2021.

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

- [On a Formal Model of Safe and Scalable Self-driving Cars](https://mlsanity.com/paper/1708.06374/) (2017)
- [A Deontic Logic Analysis of Autonomous Systems' Safety](https://mlsanity.com/paper/2009.00738/) (2020)

## Built on by (most cited first, 3 of 3)

- [Attention-Based Real-Time Defenses for Physical Adversarial Attacks in Vision Applications](https://mlsanity.com/paper/2311.11191/) (2023)
- [Deontic Temporal Logic for Formal Verification of AI Ethics](https://mlsanity.com/paper/2501.05765/) (2025)
- [A Real-Time Neuro-Symbolic Ethical Governor for Safe Decision Control in Autonomous Robotic Manipulation](https://mlsanity.com/paper/2603.14221/) (2026)

## Abstract (arXiv)

We develop a formal framework for automatic reasoning about the obligations of autonomous cyber-physical systems, including their social and ethical obligations. Obligations, permissions and prohibitions are distinct from a system's mission, and are a necessary part of specifying advanced, adaptive AI-equipped systems. They need a dedicated deontic logic of obligations to formalize them. Most existing deontic logics lack corresponding algorithms and system models that permit automatic verification. We demonstrate how a particular deontic logic, Dominance Act Utilitarianism (DAU), is a suitable starting point for formalizing the obligations of autonomous systems like self-driving cars. We demonstrate its usefulness by formalizing a subset of Responsibility-Sensitive Safety (RSS) in DAU; RSS is an industrial proposal for how self-driving cars should and should not behave in traffic. We show that certain logical consequences of RSS are undesirable, indicating a need to further refine the proposal. We also demonstrate how obligations can change over time, which is necessary for long-term autonomy. We then demonstrate a model-checking algorithm for DAU formulas on weighted transition systems, and illustrate it by model-checking obligations of a self-driving car controller from the literature.