Tracy, Traces, and Transducers: Computable Counterexamples and Explanations for HyperLTL Model-Checking

TL;DR

This paper introduces two methods for generating counterexamples and explanations in HyperLTL model-checking, enhancing its diagnostic capabilities by leveraging Skolem functions, with one method being complete for certain traces and the other more general but incomplete.

Contribution

It proposes two paradigms for computing counterexamples and explanations in HyperLTL model-checking, using Skolem functions, including a complete method for ultimately periodic traces and a more general, computable approach.

Findings

The first paradigm is complete for ultimately periodic traces.

The second paradigm uses computable Skolem functions and is more general.

It is decidable whether a system admits computable Skolem functions.

Abstract

HyperLTL model-checking enables the automated verification of information-flow properties for security-critical systems. However, it only provides a binary answer. Here, we introduce two paradigms to compute counterexamples and explanations for HyperLTL model-checking, thereby considerably increasing its usefulness. Both paradigms are based on the maxim ``counterexamples/explanations are Skolem functions for the existentially quantified trace variables''. Our first paradigm is complete (everything can be explained), but restricted to ultimately periodic system traces. The second paradigm works with (Turing machine) computable Skolem functions and is therefore much more general, but also shown incomplete (not everything can computably be explained). Finally, we prove that it is decidable whether a given finite transition system and a formula have computable Skolem functions witnessing that the system satisfies the formula. Our algorithm also computes transducers implementing computable Skolem functions, if they exist.