Tracy, traces, and transducers: computable counterexamples and explanations for HyperLTL model-checking

HyperLTL model-checking enables the automated verification of information-flow properties for security-critical systems. However, it only provides a binary answer. Here, we consider the problem of computing counterexamples and explanations for HyperLTL model-checking, thereby considerably increasing its usefulness. Based on the maxim “counterexamples/explanations are Skolem functions for the existentially quantified trace variables”, we consider (Turing machine) computable Skolem functions. As not every finite transition system and formula have computable Skolem functions witnessing that the system satisfies the formula, we consider the problem of deciding whether such functions exist. Our main result shows that this problem is decidable by reducing it to solving multiplayer games with hierarchical imperfect information. Furthermore, our algorithm also computes transducers implementing such functions, if they exist.