Abstract

Modern software and cyberphysical systems face open-ended tasks in complex environments, rendering accountability in the event of harm or injury an ever-growing challenge for both social and technical processes. Although well-understood techniques can judge whether programs obey formal properties, the real-world assurance that this process provides depends on its scope and precision. Harms can even occur when every agent operates correctly according to its model of the system and knowledge of its state. An understanding of the contribution of autonomous agents to a harm is necessary in order to consider counterfactuals and verify whether those agents acted appropriately. Philosophy and law employ decision artifacts such as beliefs, desires, and intentions as the basis for such assessments, motivating an understanding of how they arise within modern software systems. In this talk we will describe how to use formal reasoning to assure the machine analogues of these decision artifacts will be faithfully recorded for accountability processes.