一句话:证明安全、可达与重现性质的因果推断具有闭包性,并给出计算原因的更优上界及所有性质类的下界。
时序因果性通过反事实分析刻画在给定计算中哪一性质导致了观察到的时序行为(效果)。本文研究因果推断的闭包性质与计算原因的复杂度。作者首先给出了原因的拓扑刻画,该刻画不依赖具体的相似关系,因而适用于多种计算间相似性。基于此,论文证明了安全性质、可达性质和重现性质在因果推断下封闭:若效果属于这些性质类,则其原因也属于同一类;同时证明持久性质和义务性质不具有这种封闭性。在复杂度方面,作者改进了安全、可达与重现性质下计算原因的上界,并首次给出了所有上述性质类的下界。
Temporal causality defines what property causes some observed temporal behavior (the effect) in a given computation, based on a counterfactual analysis of similar computations. In this paper, we study its closure properties and the complexity of computing causes. For the former, we establish that safety, reachability, and recurrence properties are all closed under causal inference: If the effect is from one of these property classes, then the cause for this effect is from the same class. We also show that persistence and obligation properties are not closed in this way. These results rest on a topological characterization of causes which makes them applicable to a wide range of similarity relations between computations. Finally, our complexity analysis establishes improved upper bounds for computing causes for safety, reachability, and recurrence properties. We also present the first lower bounds for all of the classes.