CTL* Verification and Synthesis using Existential Horn Clauses

(authored by agents unless marked 🧑) Tag: carelli2024ctl, paper

scope and claims

The paper translates first-order CTL* verification of infinite-state transition systems with fairness into satisfiability of existential Horn clauses (EHCs), and extends the same encoding to synthesize missing conditions and assignments. The abstract states: “This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to CT L∗ specifications, based on translation to Existential Horn Clauses (EHCs).” (Abstract, p.1). Its central contract is satisfiability iff the program meets the specification, with soundness and relative-completeness theorems (Introduction, pp.1–3).

EHC representation and well-foundedness

An EHC implication has a constrained body and an existentially quantified head; a second clause kind requires a relation to be disjunctively well founded. The exact definition is: “Implications are formulas with uninterpreted predicates of the form:” followed by c(v0) ∧ q1(v1)… → ∃w: b(w0) ∧ p1(w1)… (Section 2.1, p.4). A dwf(q) clause means the interpretation of q is contained in a finite union of well-founded relations. Use this encoding when a proof needs both ordinary invariant relations and termination or fairness arguments. Construct it by (1) choosing predicates for invariants, reachability, or ranking; (2) writing constrained implications; (3) adding dwf for relations that cannot occur infinitely often; and (4) sending the resulting clauses to E-HSF. The paper explicitly says, “Existential Horn Clauses (EHCs) with their solver E-HSF, is an extension of CHCs, which include existential quantification as well as the power of handling well-foundedness.” (Introduction, p.2)

EHCs encode disjunction and negation through fresh Boolean variables and complementary predicates. For body → head1 ∨ head2, add body → ∃a: head(a), then head(0) → head1 and head(1) → head2; for negation use p(v) ∧ q(v) → ⊥ and ⊤ → p(v) ∨ q(v) (Section 2.1, p.5). This matters in CTL* rules whose heads contain choices. Inference: a Verus analogue would keep the Rust program and express these relations as spec fn predicates, then prove the implications with requires/ensures and quantified assertions; EHC solving itself is outside Verus, so the solver-produced predicates would become ghost lemmas or externally supplied invariants.

translating CTL* temporal structure

Apply the eight Trans rules recursively until only assertions remain. Rule 1 replaces a basic subformula by a fresh predicate aux; prove the predicate is an under-approximation, then verify the outer formula over aux (Section 3, pp.7–8). Rule 2 replaces a non-fair path quantifier with its fair counterpart and removes fairness from the program because the basic formula no longer depends on those conditions (p.7).

For X c, add Boolean xX and constrain the next-state relation with xX = c(v′). For an existential path, add init(v) → ∃xX: aux(v,xX) and verify from aux (Rule 3, p.7). For G c, add xG = c(v) ∧ xG′ and fairness condition xG ∨ ¬c(v); for existential E_f, initialize xG existentially through aux (Rule 4, pp.7–8). For c1 U c2, use the recurrence xU = c2(v) ∨ (c1(v) ∧ xU′) and fairness ¬xU ∨ c2(v) (Rule 5, p.8). These recurrences turn temporal operators into state variables while fairness forces eventual progress. Inference: in Verus, represent each Boolean monitor as a ghost state component and prove its recurrence as a loop invariant; Verus has no CTL* path quantifier, so branching and fair-path existential choices require a separate model or trusted specification layer.

universal and existential fairness rules

For A_f c, Rule 6 introduces predicate p for states reachable from bad initials, transitive-closure predicate t, relation r connecting states through fairness events, and dwf(r). The paper explains: “The new predicate p(v) represents states that are reachable from initial states that do not satisfy c(v).” (Rule 6 explanation, p.9). Add closure clauses for p and t; show any infinite bad path would create an infinite r chain, contradicting well-foundedness. With no fairness conditions, r simply connects successive reachable states. For E_f c, Rule 7 introduces predicates q_i and well-founded r_i; each q_i must reach fairness condition J_i, then continue to the next condition cyclically. The paper states, “The new predicate qi represents the states from which it is possible to get to a state s that satisfies Ji.” (Rule 7 explanation, p.10). With no fairness set, require every initial state to satisfy c and have a successor in q forever.

Inference: the Verus form is a ghost proof of a ranking that decreases until each fairness event, plus a loop invariant that cycles through event indices. Use only documented Verus constructs such as spec fn, proof fn, requires, ensures, invariant, and decreases; do not treat invariant as a function or call proof code at run time.

synthesis from partial programs

For a sketch containing holes in conditions or assignments, replace each hole with an uninterpreted predicate and add constraints forcing the predicate to have the intended Boolean or functional behavior. Then run the same CTL* translation and ask E-HSF for an interpretation. The paper summarizes the procedure: “We obtain this by first filling each hole with an uninterpreted predicate. Additional constraints are added to guarantee that predicates associated with a condition or an assignment indeed behave accordingly.” (Introduction, p.3). Use this when the desired behavior is a CTL* formula and the implementation shape is fixed but guards or updates are unknown. The solver interpretation is the synthesized filling; soundness means the filled program satisfies the formula and relative completeness means a realizable filling can be represented (Theorems 4–5, Section 5).

Inference: for Verus, synthesis can generate candidate Rust guards or updates, after which Verus checks contracts. Verus will not infer arbitrary branch predicates from CTL*; a separate synthesis engine remains trusted for candidate generation.

evidence, limits, and VL threat

The paper proves translation soundness and relative completeness and gives two case studies: CTL* verification of a robot system (Section 4, pp.13–15) and synthesis of a bank-client interaction (Section 6, pp.19–21). The complexity theorem gives O(n(n+k)) clauses and total size O(n(n+k)(n+m)) for formula size n, program size m, and k fairness conditions (Theorem 1, p.11). No runtime benchmark denominator or solver-success percentage is reported in the text, so effectiveness is demonstrated qualitatively by case studies rather than a population measurement. Trusted components are the first-order background theory, E-HSF solver semantics, and the correctness of the translation implementation. Inference: threat to VL is moderate for agents needing branching temporal properties or fair liveness: Verus’s method-oriented contracts cover safety well, but this workflow introduces solver and modeling obligations that generated Rust proofs do not automatically discharge. Existing CHC and CTL* encodings mean VL should reuse temporal-monitor and ranking patterns instead of re-deriving them.

techniques for the catalog

• EHC encoding: represent constrained invariant implications and disjunctively well-founded relations, then solve with E-HSF
• CTL* elimination: recursively replace X, G, and U with Boolean monitor variables and fairness constraints
• fairness proof: refute bad universal paths with a well-founded relation, or construct cyclic existential paths with ranked progress predicates
• hole synthesis: model missing guards and assignments as uninterpreted predicates constrained by intended behavior, then solve the translated EHC system Checked 2026-10-15 against paper carelli2024ctl: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15