  We consider the pressing question of how to model, verify, and ensure that
autonomous systems meet certain \textit{obligations} (like the obligation to
respect traffic laws), and refrain from impermissible behavior (like recklessly
changing lanes). Temporal logics are heavily used in autonomous system design;
however, as we illustrate here, temporal (alethic) logics alone are
inappropriate for reasoning about obligations of autonomous systems. This paper
proposes the use of Dominance Act Utilitarianism (DAU), a deontic logic of
agency, to encode and reason about obligations of autonomous systems. We use
DAU to analyze Intel's Responsibility-Sensitive Safety (RSS) proposal as a
real-world case study. We demonstrate that DAU can express well-posed RSS
rules, formally derive undesirable consequences of these rules, illustrate how
DAU could help design systems that have specific obligations, and how to
model-check DAU obligations.
