Background Theory

Given a HyperLTL formula \(\varphi\), a bound \(k\), and a set of Kripke structures \(\mathcal{K}\), the goal is to construct a \(\text{QBF}\) formula \(⟦ \mathcal{K}, \varphi ⟧_k\) whose satisfiability reflects whether \(\mathcal{K} \models \varphi\) holds within bound \(k\).

Encoding the Kripke Structures

To reduce model checking to QBF, each Kripke structure is encoded as a Boolean formula representing all its valid traces up to a fixed bound \(k\).

  • States are encoded using fresh Boolean variables \(n_0, n_1, \dots\), added to the set of atomic propositions: \(\mathit{AP}^* = \mathit{AP} \cup \{n_0, n_1, \dots\}\).

  • The initial condition is a formula \(I_A\) over \(\mathit{AP}^*\)

  • The transition relation is encoded as \(R_A(x, x')\), where \(x\) and \(x'\) represent states at consecutive time steps.

  • For each position \(i = 0\) to \(k\), a copy \(x_A^i\) of the variables is introduced. For a structure \(K_A\) and bound \(k\), the unrolled encoding is:

    \[⟦K_A⟧_k = I_A(x_A^0) \land R_A(x_A^0, x_A^1) \land \dots \land R_A(x^{k-1}_A,x^k_A)\]

This formula represents all traces of length \(k\) from the Kripke structure, and provides the basis for checking temporal properties using QBF.

Encoding the Inner LTL Formula

The inner LTL formula is translated into a Boolean formula over the unrolled trace, using standard bounded model checking (BMC) techniques with semantic variations.

  • The formula is encoded inductively as \(⟦ \psi ⟧_i^k\), where \(i\) is the current time step and \(k\) is the bound.

  • There are four variants depending on semantics: pessimistic, optimistic, halting pessimistic, and halting optimistic.

Inductive rules (common to all semantics):

\[\begin{split}\begin{align} &⟦p_\pi⟧^{*}_{i,k} &:=\ &p_\pi^i \\ &⟦\neg p_\pi⟧^{*}_{i,k} &:=\ &\neg p_\pi^i \\ &⟦\psi_1 \lor \psi_2⟧^{*}_{i,k} &:=\ &⟦\psi_1⟧^{*}_{i,k} \lor ⟦\psi_2⟧^{*}_{i,k} \\ &⟦\psi_1 \land \psi_2⟧^{*}_{i,k} &:=\ &⟦\psi_1⟧^{*}_{i,k} \land ⟦\psi_2⟧^{*}_{i,k} \\ &⟦\psi_1 \mathcal{U} \psi_2⟧^{*}_{i,k} &:=\ &⟦\psi_2⟧^{*}_{i,k} \lor (⟦\psi_1⟧^{*}_{i,k} \land ⟦\psi_1 \mathcal{U} \psi_2⟧^{*}_{i+1,k}) \\ &⟦\psi_1 \mathcal{R} \psi_2⟧^{*}_{i,k} &:=\ &⟦\psi_2⟧^{*}_{i,k} \land (⟦\psi_1⟧^{*}_{i,k} \lor ⟦\psi_1 \mathcal{R} \psi_2⟧^{*}_{i+1,k}) \\ &⟦\bigcirc \psi⟧^{*}_{i,k} &:=\ &⟦\psi⟧^{*}_{i+1,k} \end{align}\end{split}\]

Base cases depend on the semantic variant and define the value beyond bound \(k\):

\[\begin{split}\begin{align} &⟦\psi⟧^{\text{pes}}_{k+1,k} := \text{false} &&⟦\psi⟧^{\text{opt}}_{k+1,k} := \text{true} \\ &⟦\psi⟧^{\text{hpes}}_{k+1,k} := ⟦\text{halted}⟧^{\text{hpes}}_{k,k} \land ⟦\psi⟧^{\text{hpes}}_{k,k} &&⟦\psi⟧^{\text{hopt}}_{k+1,k} := ⟦\text{halted}⟧^{\text{hopt}}_{k,k} \rightarrow ⟦\psi⟧^{\text{hopt}}_{k,k} \end{align}\end{split}\]

These base cases affect how temporal operators are evaluated at the final unrolling step.

Combining the Encodings

Let \(\varphi = \mathbb{Q}_A \pi_A. \mathbb{Q}_B \pi_B. \dots \mathbb{Q}_Z \pi_Z. \psi\) be a HyperLTL formula, and let each \(\pi_j\) be associated with a Kripke structure \(K_j\).

The full QBF encoding is:

\[⟦\mathcal{K}, \varphi⟧^{*}_k = \mathbb{Q}_A \overline{x_A} \cdot \mathbb{Q}_B \overline{x_B} \cdots \mathbb{Q}_Z \overline{x_Z} \left( ⟦K_A⟧_k \circ_A ⟦K_B⟧_k \circ_B \cdots ⟦K_Z⟧_k \circ_Z ⟦\psi⟧^{*}_{0,k} \right)\]
Where:

  • \(⟦ K_j ⟧_k\) is the unrolling of Kripke structure \(K_j\)

  • \(\circ_j = \wedge\) if \(\mathbb{Q}_j = \exists\), and \(\rightarrow\) if \(\mathbb{Q}_j = \forall\) for \(\in \mathit{Vars}(\varphi)\)

  • \(⟦ \psi ⟧_0^k\) is the encoding of the LTL subformula under the chosen semantics

This combined formula allows a QBF solver to decide whether the HyperLTL formula holds for all (or some) traces up to bound \(k\).

References

A more detailed explanation can be found in the paper Bounded Model Checking for Hyperproperties Tzu-Han Hsu, César Sánchez, and Borzoo Bonakdarpour