A Deontic Logic Analysis of Autonomous Systems' Safety

TL;DR

This paper introduces a deontic logic framework using Dominance Act Utilitarianism (DAU) to model, analyze, and verify obligations of autonomous systems, addressing limitations of traditional temporal logics.

Contribution

It proposes DAU as a novel approach for formalizing and reasoning about autonomous system obligations, demonstrated through analysis of Intel's RSS safety proposal.

Findings

DAU can effectively encode autonomous system obligations.

Formal derivation of undesirable outcomes from RSS rules.

DAU facilitates system design and model-checking of obligations.

Abstract

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.