Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle Obligations

TL;DR

This paper introduces a formal framework using deontic logic to specify and verify social and ethical obligations of autonomous systems, demonstrated through self-driving car safety standards.

Contribution

It formalizes obligations in autonomous systems with a new logic, DAU, and provides algorithms for automatic verification, addressing gaps in existing deontic logic applications.

Findings

Formalized a subset of Responsibility-Sensitive Safety in DAU

Developed a model-checking algorithm for DAU formulas

Verified obligations of a self-driving car controller

Abstract

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.