Hyperproperties relate multiple computation traces to each other. Model checkers for hyperproperties thus return, in case a system model violates the specification, a set of traces as a counterexample. Fixing the erroneous relations between traces in the system that led to the counterexample is a difficult manual effort that highly benefits from additional explanations. In this paper, we present an explanation method for counterexamples to hyperproperties described in the specification logic HyperLTL. We extend Halpern and Pearl's definition of actual causality to sets of traces witnessing the violation of a HyperLTL formula, which allows us to identify the events that caused the violation. We report on the implementation of our method and show that it significantly improves on previous approaches for analyzing counterexamples returned by HyperLTL model checkers.

翻译：超异性性能的模型检查器将多重超异性性性能的多重计算痕迹相互联系起来。 因此,当系统模型违反规格时,将一组痕量作为反示例返回。 纠正导致反例的系统中痕量之间的错误关系是一项艰巨的人工工作,从更多的解释中得益匪浅。 在本文中,我们给出了对超超超LTL逻辑描述的超异性性性性能的反抽样的解释方法。 我们将Halpern和Pearl关于实际因果性的定义扩大到目睹超超LTL公式被违反的几组痕量,这几组痕量使我们得以识别造成违反该公式的事件。 我们报告我们的方法的实施情况,并表明它大大改进了以往分析超LTL模式检查器返回的反异性性能的方法。