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

TL;DR

The problem of computing counterexamples and explanations for HyperLTL model-checking is considered, thereby considerably increasing its usefulness and showing that the problem is decidable by reducing it to solving multiplayer games with hierarchical imperfect information.

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.

Figures (2)

• Figure 1: The evolution of a play of $\mathcal{G}(\mathfrak{T}, \varphi)$ for a sentence $\varphi$ with six variables. Each gray shape is a subround, consisting of a move of Player $U$ or a move of one variable player. We have $\Delta_5 = 1$, $\Delta_4 = \Delta_3 = 2$, $\Delta_2 = \Delta_1= 3$, and $\Delta_0 = 4$, which corresponds to the number of blocks picked by the player in charge of variable $\pi_i$ in round $0$.
• Figure 2: Illustrating configurations for a formula with six variables, where a filled circle denotes an element in the domain, and an unfilled circle an element that is not in the domain. The upper row shows initial $i$-configurations for $i=0,1,2,\ldots, 5$ (from left to right), the lower row shows looping $i$-configurations for $i=0,1,2,\ldots, 5$ (from left to right), and the configuration on the right in between the rows is full. Solid arrows show the effect of extending and shifting configurations. The shifting operation is illustrated using the numbers in the circles. Finally, in a play of $\mathcal{G}(\mathfrak{T},\varphi)$ the configurations stored in positions follow the solid arrows, but take the dashed shortcuts avoiding full configurations.

Theorems & Definitions (21)

• Remark 1
• Remark 2
• Remark 3
• Example 1
• Lemma 1
• proof
• Proposition 1: FWjournal
• Theorem 1
• proof
• Example 2