Explaining Hyperproperty Violations

TL;DR

This paper introduces an explanation method for hyperproperty violations in system models, extending causality concepts to sets of traces, thereby aiding debugging of complex system specifications.

Contribution

It extends Halpern and Pearl's causality framework to hyperproperties, enabling trace-based explanations for HyperLTL violations, and demonstrates improved analysis of counterexamples.

Findings

Significantly improves counterexample analysis for HyperLTL violations

Extends causality concepts to sets of traces in hyperproperties

Provides an implementation that outperforms previous methods

Abstract

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.