Bounded Synthesis of Reactive Programs

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

scope and result

The paper synthesizes structured reactive programs from an LTL specification. It targets Madhusudan’s small imperative language, whose syntax includes Boolean expressions, assignments, conditionals, loops, and input/output statements. The motivating problem is that finite-state-machine synthesis flattens structure: “The synthesized code lacks control structures, such as while loops, and symbolic operations on program variables” (Section 1, p. 2). The contribution is a bounded search over program-tree size, reduced to SAT, with two encodings that produce the same programs.

The paper’s first technique is a two-way universal tree-automaton encoding (Sections 3–4, pp. 4–8). Translate the LTL specification to a universal co-Büchi automaton, then to a two-way universal Streett automaton over program trees. A run graph has vertices (automaton state, program-tree node, direction) and edges induced by tree movement and automaton transitions. For every Büchi, co-Büchi, or Streett acceptance condition, assign bounded natural-number annotations to reachable vertices. An annotation relation decreases on rejecting states and is nonincreasing or unconstrained on accepting states. Theorem 4 states that valid annotations exist exactly when every run satisfies acceptance. Encode the tree labels, left/right successors, reachability, and annotations as Boolean variables; constrain the root to be reachable, successors to follow the chosen syntax, and every edge to satisfy the annotation relation. Increase the bound until SAT returns a tree. Theorem 5 gives the exact bound relationship: a satisfiable formula yields a program tree of size at most floor(c/|A|).

The paper’s second technique avoids the two-way automaton detour (Section 5, pp. 9–10). Its four explicit phases are: (1) guess a syntactically correct program tree; (2) for every input at every reachable InOut node, simulate deterministic program execution until the next InOut; (3) compress the execution graph into direct input-labelled transitions and output states, using shortcut successors and a ranking that bounds the number of internal steps; (4) verify this simplified structure with a standard bounded-synthesis run graph and universal co-Büchi automaton. The authors call the shortcut an inductive chain: if a successor is already InOut, use it; otherwise use the successor’s shortcut. The rank supplies the induction base. Inference: this decomposition is the most directly reusable algorithmic lesson: separate syntax, deterministic evaluation, graph compression, and temporal verification.

how to apply and Verus translation

Use the first encoding when an existing automata library and a uniform SAT backend are available. Use the two-wayless encoding when direct execution constraints are smaller and the implementation language has deterministic local semantics. In either case, enumerate a finite syntax-tree bound, encode candidate labels and control-flow links, add acceptance witnesses, solve, and extract the tree. The paper’s concrete synthesized examples include while(tt){ out = in; InOut }, a latch, and a two-bit arbiter (Table 2, p. 10).

Inference: Verus does not synthesize arbitrary Rust syntax from LTL. A practical Verus analogue is to write a bounded controller skeleton in Rust, represent the finite control state with an enum or integer, and prove an inductive temporal invariant with spec fn, requires, ensures, loop invariant, and assert. A SAT-produced tree can be treated as input data, after which Verus proves that the interpreter for that tree preserves the safety invariant. Inference: the paper’s automaton annotations become ghost state and ranking functions; its SAT constraints become Verus proof obligations. Inference: liveness and fairness acceptance are not automatically supplied by ordinary Verus contracts, so a separate well-founded ranking or an explicit finite-state transition-system proof is needed. Verus constructs must remain those documented for Verus: spec fn is non-executable, proof fn is erased, and loop invariants are annotations rather than calls.

evidence, assumptions, and limits

The prototype comparison uses four benchmarks (Table 1, p. 10), reporting syntax-tree states, extra variables, automaton size, and solving time. For in ↔ out with 6 states, the two-way encoding took 16 seconds versus 2 seconds for two-wayless; with 9 states, 11m29s versus 8m34s. The latch took more than 120 minutes versus 8m07s, and the 2-bit arbiter took 66m48s versus 14m18s. Inference: these are one run per benchmark on the authors’ prototype; no hardware denominator or repeated-run variance is reported. The paper concludes that “our experiments with a prototype implementation indicate a strong advantage for the second approach” (Section 1, p. 3). It also explicitly limits the claim: “no method has a clear theoretical advantage over the other” (Section 1, p. 3).

What is proved is the equivalence of the encoding constraints and acceptance of a bounded program under Büchi, co-Büchi, or Streett conditions. What remains trusted includes the LTL-to-automaton construction, SAT solver, extraction code, and the semantics of the target language. Inference: a VL product could reuse the decomposition for generating small verified protocol controllers, but synthesis itself is a threat boundary: a solver or extraction bug can select an unintended program unless Verus verifies the extracted artifact. The approach assumes finite syntax bounds, finite automata, deterministic input handling, and a specification expressible in the supported acceptance classes. It does not establish completeness for unbounded program size; unsatisfiability at a bound only rules out that bound.

Earlier work already provides ordinary bounded synthesis of finite-state machines and Madhusudan’s fixed-variable program synthesis; VL should not redo those translations. The paper’s new value is the direct structured-program encoding and its measured engineering tradeoff. Inference: the table’s four benchmark times are consistent with the stated qualitative result, but they are preliminary and do not establish scalability beyond these examples.

techniques for the catalog

• two-way universal run-graph synthesis — encode a program tree, universal automaton run graph, reachability, and bounded Büchi/co-Büchi/Streett annotations as SAT
• two-wayless direct synthesis — simulate deterministic program fragments, compress them with ranked shortcut successors, then verify the compressed transition graph
• annotation acceptance witnesses — express an infinite-path acceptance condition as bounded local comparisons on every reachable edge Checked 2026-10-14 against the paper by a Codex agent: audit record gerstacker2018bounded; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15