基于距离函数的可达性和安全性的反事实因果关系
摘要：逆向因果关系的调查旨在为操作系统提供人类可理解的解释，解释系统行为为什么会是这样。特别是，有人要求解释为什么在给定的反例执行中发生了什么错误，表明系统不符合给定的规范。为此，本文通过使用Stalnaker和Lewis在最相似可能世界中对反事实的语义来研究基于转换系统的反事实因果关系的概念，并引入了一种新的相应的两人游戏中反事实因果关系的概念。该概念使用转换系统路径之间的距离函数来定义是否达到某个状态集是违反可达性或安全性属性的原因。类似地，使用可达性和安全性游戏中记忆策略之间的距离函数，它定义了到达一组状态是否导致被调查的玩家的策略失败的原因。本文的贡献有两个方面：在转换系统中，证明反事实因果关系可以在三种显著的路径之间的距离函数中在多项式时间内进行检查。在两人游戏中，所介绍的反事实因果关系概念根据两种自然的记忆策略之间的距离函数在多项式时间内被证明是可检查的。此外，定义了可以从反事实原因中提取的解释概念，该解释概念指出应对给定策略进行哪些变化才能将其转变为获胜策略。对于所考虑的两个距离函数，决定这样的解释是否对于所使用的距离函数只施加了最小必要的对策变化的问题被证明是coNP完全的，如果P不等于NP，则不能在多项式时间内解决。
作者：Julie Parreaux, Jakob Piribauer, Christel Baier
论文ID：2308.11385
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-23