DASS: Accountability from Attention, not Assumption

现代软件和网络物理系统在复杂的环境中面临着开放式的任务，这使得在发生伤害或伤害时的问责制成为社会和技术过程中日益增长的挑战。虽然很好理解的技术可以判断程序是否遵守形式属性，但是这个过程提供的真实世界的保证取决于它的范围和精度。当每个主体根据其系统模型和对其状态的了解正确操作时，危害甚至可能发生。了解自主主体对伤害的贡献是必要的，以便考虑反事实并验证这些主体是否采取了适当的行动。哲学和法律使用诸如信念、欲望和意图之类的决策工件作为评估的基础，促使人们理解它们是如何在现代软件系统中产生的。该项目的新颖之处在于：(i)使用正式推理来确保这些决策工件的机器模拟将被忠实地记录在问责制过程中；以及（ii）对如何使用这些工件来指导更适合于责任评估的软件开发的调查。该项目的影响包括：(i)开发正式方法，以确保保留的信息和编程语言结构的充分性，以帮助开发人员实现这一目标；（ii）构建框架，以适应性强、价值中立的方式对责任进行评估。更具体地说，这个项目的目的是评估如何使用认知和其他模态逻辑的工具来指导行为、欲望、信念和意图背后的信息的形式化，并开发可验证的跟踪属性——可逆性——这保证了有关这些决策工件的必要信息以有利于回顾性分析的方式记录下来。此外，该项目努力将信息如何被指定与不同哲学流派（如义务论或功利主义伦理学）如何解释潜在的人工制品分离开来。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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. The project's novelties are (i) the use of formal reasoning to assure the machine analogues of these decision artifacts will be faithfully recorded for accountability processes; and (ii) an investigation of how these artifacts can be used to guide development of software more amenable to responsibility assessment. The project's impacts include (i) the development of formal methods to assure the sufficiency of retained information and programming languages constructs that assist developers to that end, and (ii) the construction of frameworks that contribute to the assessment of responsibility in an adaptable, value-neutral manner.More specifically, the aim of this project is to evaluate how the tools of epistemic and other modal logics can be used to guide formalization of the information underlying the actions, desires, beliefs and intentions of an agent, and to develop a verifiable trace property -- reversibility -- which guarantees that the necessary information regarding those decision artifacts is recorded in a manner conducive to retrospective analysis. Furthermore, this project strives to decouple how information is specified from how the underlying artifacts are interpreted by the different philosophical schools, such as deontological or utilitarian ethics.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.