基于距离函数的可达性与安全性反事实因果性
计算机科学中的逻辑
2023-08-23 v1
摘要
对运行系统的因果性研究旨在提供人类可理解的解释，说明系统为何表现出其行为。尤其存在一种需求，即解释在给定的反例执行上出了什么问题，该反例表明系统不满足给定规约。为此，本文基于 Stalnaker 与 Lewis 的反事实可能世界最相似语义，研究迁移系统中的反事实因果性概念，并引入双人博弈中相应的新颖反事实因果性概念。利用迁移系统中路径间的距离函数，该概念定义了到达某状态集合是否构成对可达性或安全性性质违反的原因。类似地，利用可达性与安全性博弈中无记忆策略间的距离函数，定义到达某状态集合是否构成所研究玩家给定策略失败的原因。本文的贡献有两方面：在迁移系统中，证明了对于三种显著的路径间距离函数，反事实因果性可在多项式时间内检验。在双人博弈中，所引入的反事实因果性概念对于两种自然的策略间距离函数被证明可在多项式时间内检验。此外，定义了一种可从反事实原因中提取的解释，其精确指出为将给定策略转化为获胜策略所需做的更改。对于所考虑的两种距离函数，判定此类解释相对于所用距离函数是否仅对给定策略施加最小必要更改的问题，分别被证明为 coNP-complete，且在 P ≠ NP 时无法在多项式时间内求解。
引用
@article{arxiv.2308.11385,
title = {Counterfactual Causality for Reachability and Safety based on Distance Functions},
author = {Julie Parreaux and Jakob Piribauer and Christel Baier},
journal= {arXiv preprint arXiv:2308.11385},
year = {2023}
}
备注
This is the extended version of a paper accepted for publication at GandALF 2023