Test-free PDL does not have Craig interpolation

This file gives a valid implication between test-free PDL formulas that has no test-free interpolant. The statement is purely semantic: it does not depend on the tableau system or on the method used to construct interpolants elsewhere in this project.

Write p, q, s for the proposition letters ·0, ·1, ·2 and a for the atomic program ·0, and let

• Γ₁ = { s, [a*]((p ∧ s) → (⟨a⟩⊤ ∧ [a]s)) }

• Γ₂ = { [a*](q → p), [a*](⟨a⟩q → q), ⟨a*⟩(q ∧ [a]⊥) }

Both sets are test-free. The common vocabulary is {a, p}; the s occurs only in Γ₁, the q only in Γ₂.

Γ₁ ∪ Γ₂ is unsatisfiable (gammaOne_gammaTwo_unsat), i.e. ⋀Γ₁ → ¬⋀Γ₂ is valid: the last formula of Γ₂ gives a path to a q-state without successors; by [a*](⟨a⟩q → q) every state on that path is a q-state, and by [a*](q → p) also a p-state. By induction along the path, using s at the start and p ∧ s → ⟨a⟩⊤ ∧ [a]s from Γ₁, every state on the path satisfies s; so the last state satisfies p ∧ s and must have a successor, which it does not.

After projecting away the private letters, Γ₁ says "along every a-path, as long as p has held there is a further a-step" (no all-p path ends in a dead end) and Γ₂ says "some all-p path ends in a dead end". An interpolant has to separate these two "until"-like properties, which needs a test: [(p?;a)*](p → ⟨a⟩⊤) is an interpolant (withTest_Interpolant), but no test-free formula is. We make this precise with a single Kripke model MG and two of its states m and v j such that

• (MG, m) ⊨ Γ₁ (gammaOne_at_m),

• (MG, v j) ⊨ Γ₂ for every j (gammaTwo_at_v),

• m and v j satisfy the same test-free formulas over {a, p} of modal depth ≤ j (depth_equiv).

Hence no test-free formula θ over {a, p} satisfies Γ₁ ⊨ θ and Γ₂ ⊨ ¬θ (no_interpolant). Three letters are the minimum for this kind of example: a side without private vocabulary is, up to negation, itself an interpolant.

The model MG

(A picture of the model can be found in the paper.)

MG has the states u, m, w i and v i for i : ℕ. The only atomic program with a nonempty relation is a; its relation R is

• u → x for every state x off the chain, that is, for every x other than the v i,

• m → u, m → m,

• w (i+1) → u, w i and v (i+1) → u, v i,

• w 0 and v 0 have no successors.

Valuation: p at m, at every w i and at every v i; s at m and u; q at every v i (nothing else at u).

The chain v j → v (j-1) → … → v 0 is an all-p path to the dead end v 0, and no edge leads from a state off the chain into it, so q := {v i} satisfies Γ₂ at v j. The states off the chain are therefore exactly those reachable from m, and there, with s := {m, u}, Γ₁ holds at m.

Why m and v j agree on test-free formulas of depth ≤ j

With a single atomic program, a test-free program α relates w to v iff for some n such that α can be executed by exactly n actual steps (L α n), there is a path of exactly n steps from w to v (relate_iff). So [α]ψ at w quantifies over the states reachable in exactly n steps, for those n (box_iff). These sets are

\begin{array}{llll} n & \text{from } m & \text{from } v_k \\ \hline 0 & \{ m \} & \{ v_k \} \\ 1 & \{ m, u \} & \{ u, v_{k-1} \} \\ 2 \ldots k & \{ m, u \} \cup \text{all $w_i$} & \{ m, u, v_{k-n} \} \cup \text{all $w_i$} \\ k+1 \ldots & \{ m, u \} \cup \text{all $w_i$} & \{ m, u \} \cup \text{all $w_i$} \\ \end{array}

since u reaches every state off the chain in every number ≥ 1 of steps, while v 0 reaches nothing. The relation Z relating every state to itself and moreover w i to v i is a bisimulation of MG with itself for the vocabulary {a, p} (Z_isBisim), and bisimilar states satisfy the same formulas over that vocabulary (IsBisim.evaluate from Pdl.Bisimulation, which does allow tests). Hence, by induction on ψ with mdepth ψ + 1 ≤ j (so j ≥ 1), in each row the witnesses on both sides are matched: the states off the chain occur on both sides, the chain states v j and v (j-1) are equivalent to m by the induction hypothesis, and v (j-n) (for n ≥ 2) is equivalent to w (j-n) by Z, which is reachable from m in the same number of steps. So [α]ψ has the same truth value at m and at v j.

The depth bound is sharp: the test-free formula ⟨a⟩(p ∧ ⟨a⟩(p ∧ … ⟨a⟩(p ∧ [a]⊥))) with j nested diamonds has depth j+1, is true at v j, and is false at m. The test-freeness cannot be dropped either: [(p?;a)*](p → ⟨a⟩⊤) is false at every v j and true at m.

The two sets of formulas

The implication is valid