权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

DASS: Accountability from Attention, not Assumption

DASS：责任源于注意力，而非假设

基本信息

批准号：
2131476
负责人：
Ruzica Piskac
金额：
$ 75万
依托单位：
Yale University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2021
资助国家：
美国
起止时间：
2021-11-01 至 2024-10-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2131476&HistoricalAwards=false
关键词：
DASS Accountability Attention Assumption

项目摘要

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.

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

项目成果

期刊论文数量（6）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Checking equivalence in a non-strict language

检查非严格语言的等价性

DOI：
10.1145/3563340
发表时间：
2022
期刊：
Proceedings of the ACM on Programming Languages
影响因子：
0
作者：
Kolesar, John C.;Piskac, Ruzica;Hallahan, William T.
通讯作者：
Hallahan, William T.

Analyzing Intentional Behavior in Autonomous Agents under Uncertainty

分析不确定性下自主主体的意图行为

DOI：
10.24963/ijcai.2023/42
发表时间：
2023
期刊：
International Joint Conferences on Artificial Intelligence Organization
影响因子：
0
作者：
Cano Córdoba, Filip;Judson, Samuel;Antonopoulos, Timos;Bjørner, Katrine;Shoemaker, Nicholas;Shapiro, Scott J.;Piskac, Ruzica;Könighofer, Bettina
通讯作者：
Könighofer, Bettina

An Algebra of Alignment for Relational Verification

关系验证的对齐代数

DOI：
10.1145/3571213
发表时间：
2023
期刊：
Proceedings of the ACM on Programming Languages
影响因子：
0
作者：
Antonopoulos, Timos;Koskinen, Eric;Le, Ton Chanh;Nagasamudram, Ramana;Naumann, David A.;Ngo, Minh
通讯作者：
Ngo, Minh

Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata

使用 Mod 2 多重自动机表示无限字的正则语言