Automated Repair of Unrealisable LTL Specifications Guided by Model Counting

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

problem and result

AuRUS searches for a realisable Linear-Time Temporal Logic (LTL) variant when no controller satisfies the input assume-guarantee specification. The paper defines two similarity objectives: shared subformulas (syntactic) and preserved behaviours (semantic). Its abstract says: “We empirically assess AuRUS on many unrealisable specifications taken from different benchmarks and show that it can successfully repair all of them.” (Abstract, p. 1). The method changes assumptions and guarantees, unlike approaches that add assumptions only (Section 1, pp. 1–2).

technique 1: genetic search over LTL repairs

When to use it. Use this when a specification is unsatisfiable or unrealisable but engineers need close alternatives rather than a single diagnosis. Unrealisability means no system strategy wins against all environment traces (Section 2.2, p. 2).

Steps. (1) Represent each candidate as S=(A,G), assumptions and guarantees. (2) Initialize a population by adding input-only assumptions drawn from reactivity patterns (□◇x, □¬(x0∧…∧xn), □◇(x0∧…∧xn)), so trivial solutions such as □y on outputs are avoided (Section 4.1, p. 3). (3) Apply LTL-aware crossover and mutation to subformulas. (4) Check satisfiability of A’∧G’ and realisability of A’→G’ with Polsat and Strix (Section 4.5, p. 5). (5) Score status, syntactic similarity, and semantic similarity. (6) Select the fittest candidates, repeat until 1000 individuals or two hours. The experimental configuration was population 100, model-counting bound k=20, best selector, crossover on 10% of individuals, mutation applied to each individual with probability 1/N per gene (N is the formula size), and 10 independent runs (Section 6, p. 6).

Crossover takes assumptions and guarantees from either parent, optionally replacing or combining subformulas. Mutation recursively changes constants, propositions, unary operators, and binary operators. For example, a leaf can flip true/false, replace a proposition, or add a unary operator; a binary formula can mutate one or both children and operators (Section 4.2, p. 4). The paper states: “The crossover operator combines two LTL specifications, namely S1 = (A1, G1) and S2 = (A2, G2), to create a new specification S3 = (A3, G3).” (Section 4.2, p. 4).

Verus form. Inference: use an AST enum for a restricted specification language, pure recursive mutation functions, and a proof that mutation preserves syntax well-formedness. Realisability is an external synthesis property; a Verus proof can check the repair scorer and AST transformations, while a trusted solver or executable checker supplies the realisability result.

technique 2: multi-objective fitness and status ordering

The fitness is f(S’)=α·status(S’)+β·synSim(S,S’)+γ·semSim(S,S’). Status is 1 when satisfiable and realisable, 0.5 when satisfiable but unrealisable, 0.2 when the conjunction is unsatisfiable but each side is satisfiable, 0.1 when only assumptions are satisfiable, and 0 when assumptions are unsatisfiable (Section 4.3, p. 4). The syntactic score averages two fractions: shared subformulas over the original’s subformulas, and over the candidate’s subformulas (Section 4.3, p. 4). Inference: averaging both fractions stops a candidate from scoring well just by being a superset of the original or by being a small subset of it.

Use the semantic score to measure overlap of behaviours. For bound k, count models of S, S’, and S∧S’ and average the two ratios: semSim(S,S’)=0.5·(#(S∧S’,k)/#(S,k)+#(S∧S’,k)/#(S’,k)) (Section 4.3, p. 4). When S∧S’ is unsatisfiable, semSim is 0. The paper reports that better performance is reached when the semantic weight is greater than or equal to the syntactic weight, and that configurations (α=.7,β=.1,γ=.2), (α=.8,β=.07,γ=.13), and (α=.9,β=.05,γ=.05) typically reach better performance (Section 6, p. 6).

Verus form. Inference: encode scores as rational-number specs or scaled integers; prove denominator nonzero under a satisfiable-model-count precondition, and prove that status dominates only through explicit weight bounds. Keep solver-produced counts as input data with a trust boundary.

technique 3: automata and transfer-matrix model-count approximation

LTL model counting is restricted to bounded models, since a satisfiable formula has infinitely many models (Section 2.1, p. 2). AuRUS first translates φ to a nondeterministic automaton Aφ. It counts finite paths of length k reaching an accepting state as a proxy for prefixes of accepting infinite traces. It then builds an N×N transfer matrix Tφ, where entry [i,j] is the number of transitions from state i to j, and computes I×Tφ^k×F for initial vector I and accepting vector F (Section 5, p. 5). The paper cautions that this is approximate: reachable accepting states that do not loop overestimate, while accepting states on multiple loops can cause underestimation.

The worked formula ψ=□(p→○q) with k=4 gives 108 by matrix multiplication, although exactly 351 lasso traces exist; 108 counts prefixes (Section 5, p. 5). The paper says: “Actually, there are exactly 351 lasso traces of length 4 for ψ but our approach reports 108 (i.e., the approximate number of prefixes for these traces).” (Section 5, p. 5).

Verus form. Inference: model the automaton as a finite Rust transition relation and prove matrix-path counting by induction on k. Verus can verify arithmetic and correspondence of a bounded path enumerator to the matrix recurrence; the automaton construction and the interpretation of counts remain trusted unless separately proved.

evidence, limits, and product implications

The experimental population has 26 unrealisable specifications: 5 literature, 13 SYNTCOMP, and 8 SYNTECH15 (Section 6, Table 1, p. 5). Each case is run 10 times. With the best-performing configuration per case, AuRUS finds satisfiable and realisable repairs in 100% of runs (Section 6.1, p. 6). Four cases yielded few repairs on average: 4 (Full Arbiter), 13 (Prioritized Arbiter), 3 (Humanoid503), and 3 (PCarV2-888) (Section 6.1, p. 6). In Table 2 (p. 6), Humanoid503, Humanoid531, Humanoid741, Humanoid742, and PCarV2-888 show a time of 7400 s (the two-hour limit), whereas Full Arbiter shows 3805 s and Prioritized Arbiter 4205 s. Against random generation of 1000 variants, random produced on average 23 times fewer repairs than AuRUS; random nevertheless produced more in Full Arbiter, Prioritized Arbiter, and PCarV2-888, with Vargha–Delaney Â12 values 33.3%, 10.5%, and 33.3% respectively (Section 6.2, p. 6). Inference: Â12 values compare the 10 runs of two configurations, so they are not success rates.

For model-count ranking at bound k=10, ApMC matched exact rankings in 9/10 random formula sets and misclassified 2/50 formulas in the remaining set; regular-expression counting misclassified 8 formulas per set on average. Exact counting took 470 seconds at k=6 and up to 6000 seconds at k=10 per set; ApMC took 2 seconds per set. Exact counting became infeasible on the 26 specifications, the regular-expression method failed on 22/26, and ApMC succeeded on all 26 (Section 6.5, p. 8). The 470 and 6000 second figures are averages per set. The denominator and bound matter: these are sets or specifications at stated k, not unbounded-model guarantees.

The paper states that “AuRUS guarantees satisfiability and realisability of its generated repairs, checked using Polsat [35] and Strix [43], respectively” and that “AuRUS uses a non-exhaustive search and may not consider all possible repairs” (Section 4.5, p. 5). It gives no guarantee that the search finds the closest repair. Its approximation can mis-rank: ApMC misclassified 2/50 formulas in one of ten sets (Section 6.5, p. 8). The paper also notes that a negating mutation, a single syntactic change, “can completely reverse the behaviors described by the original formula” (Section 4.3, p. 4). Inference: for VL, this is useful for proposing repaired Verus specifications or contracts, but a candidate must still pass Verus verification. Threat is moderate: a search can optimize similarity while silently weakening safety, so status and final proof must remain mandatory.

what prior work makes unnecessary

The paper says the prior repair techniques “attempt to repair the specifications just by adding assumptions” built from counter-strategy information and the current specification, and that they “impose syntactical restrictions on how specifications are written, limiting their application to particular patterns (e.g., GR(1), a subset of LTL)” (Section 1, pp. 1–2). Inference: AuRUS’s ability to mutate guarantees as well as assumptions is the part worth transferring. Inference: VL should not rebuild a generic genetic algorithm merely to diagnose a failed proof if a counterexample and direct contract revision suffice; reuse the model-counting idea only when many plausible repairs need ranking.

techniques for the catalog

• LTL genetic repair — Evolve assumption/guarantee ASTs with crossover and mutation, checking satisfiability and realisability
• status-plus-similarity fitness — Rank candidates by realisability status, shared syntax, and bounded behavioural overlap
• transfer-matrix counting — Approximate bounded LTL model counts by automata paths and matrix powers Checked 2026-10-18 against the full paper by a Claude agent (mid-paper quote: “The development set is meant to support us in setting the parameters of our algorithm, with the hope that the best-performing configuration for the development set, will generalise to the evaluation set.”): read the full text (reading-order extraction, all 9 pages); checked every quotation, number (fitness weights and status values, 108/351 example, Table 1 counts, Tables 2 and 4 figures, A12 values, configuration), section and page reference, and technique step against the paper; changed page references (Sections 4.2, 4.3, 5, 6, 6.1, 6.2, 6.5, Table 1), added initial-population detail, corrected the two-hour claim (Full Arbiter and Prioritized Arbiter did not reach the limit in Table 2), corrected “23 times more” to random producing 23 times fewer repairs, replaced “proves” with the paper’s guarantee and non-exhaustive-search wording, and marked own conclusions as Inference; did not check the cited external works, Figure 3 values, Table 3, or the replication package, and the Verus-form paragraphs are inference only.

Last edited: 2026-10-18