Explaining Hyperproperty Violations

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Contributors

  • Norine Coenen - , CISPA - Helmholtz Center for Information Security (Author)
  • Raimund Dachselt - , Chair of Multimedia Technology (Author)
  • Bernd Finkbeiner - , CISPA - Helmholtz Center for Information Security (Author)
  • Hadar Frenkel - , CISPA - Helmholtz Center for Information Security (Author)
  • Christopher Hahn - , CISPA - Helmholtz Center for Information Security (Author)
  • Tom Horak - , elevait GmbH & Co. KG (Author)
  • Niklas Metzger - , CISPA - Helmholtz Center for Information Security (Author)
  • Julian Siber - , CISPA - Helmholtz Center for Information Security (Author)

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.

Details

Original languageEnglish
Title of host publicationComputer Aided Verification
EditorsSharon Shoham, Yakir Vizel
PublisherSpringer Science and Business Media B.V.
Pages407-429
Number of pages23
ISBN (electronic)978-3-031-13185-1
ISBN (print)978-3-031-13184-4
Publication statusPublished - 2022
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13371 LNCS
ISSN0302-9743

Conference

Title34th International Conference on Computer Aided Verification, CAV 2022
Duration7 - 10 August 2022
CityHaifa
CountryIsrael

External IDs

ORCID /0000-0002-2176-876X/work/159171489

Keywords