Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle
  Obligations
  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.
