PaperlayerView exact revision on arXiv

Source-linked AI summary

Computing GR(1) Assume-Guarantee Contracts

Yigit Narter, Emily Zhao, Inigo Incer

arXiv:2610.37534v1cs.LOcs.SYeess.SY

TL;DR

Computing composition and quotient for temporal assume–guarantee contracts requires eliminating variables, but exact elimination can leave the GR(1) representation. The paper develops sound, GR(1)-preserving CAVE procedures and applies them to contract operations; comparisons show complementary scaling against exact automata-based elimination.

  • Problem

    Temporal assumptions and guarantees make explicit composition and quotient difficult to compute because eliminating interface variables can leave GR(1) or require costly automata complementation.

    Source: §1 · p. 2

  • Method

    The paper develops sound context-aided variable-elimination procedures for GR(1)-modulo formulas, with subproblem-wise optimality guarantees within an admissible class, and implements them in Pacti.

    Source: §1 · p. 2, §4 · p. 9, Relaxation · p. 13

  • Results

    Spot is faster on small instances, but its time rises from 0.003 s with one target liveness conjunct to over 300 s with six, while CAVE takes 0.05–0.36 s for one to eight.

    Source: Empirical comparisons · p. 14

  • Takeaways & Limitations

    The procedures compute GR(1) contract operations in Pacti, and the AEB study derives system-level contracts and exposes compatibility conditions among component specifications.

    Source: §1 · p. 2, §5.1 · pp. 17–18

    Finite invariant windows can miss GR(1)-expressible consequences that depend on earlier invariant information, so the admissible elimination construction need not be exact.

    Source: §4.1 · p. 11, §4.3 · p. 16

Abstract

from arXiv · show

Assume-guarantee contracts provide a set of algebraic operations that enable the efficient compositional design and analysis of complex engineering systems. The explicit computation of these operations at component interfaces is currently supported only for some logics lacking a notion of time. This paper develops theory and algorithms to compute these operations when the contracts are expressed in the GR(1) modulo theory. The key challenge is the computation of two quantifier elimination problems for temporal formulas. We develop context-aided variable elimination procedures on GR(1)-modulo formulas, establish their soundness, characterize subproblem-wise optimal solutions within an admissible class of formulas, and use the procedures to compute contract operations, including composition and quotient. We implement the resulting framework in Pacti, automating compositional reasoning over GR(1) contracts. Finally, we demonstrate the framework on an automated emergency-braking case study, where we compute system-level contracts and expose compatibility conditions arising from the interaction of component specifications. Experiments on synthetic families show that the cost is governed by the number of eliminated variables and liveness conjuncts, and a comparison with exact automata-based elimination shows complementary scaling.

1 Introduction

Assume–guarantee contracts support compositional system design, but computing temporal contract operations over component interfaces requires eliminating variables. This paper develops sound GR(1)-modulo elimination procedures and implements contract operations in Pacti.

1 Introduction

  • Assume–guarantee contracts formalize component assumptions and guarantees and provide algebraic operations for system-level design and analysis.The paper motivates this compositional approach against a gap between software development and verification across operating conditions.Source: §1 · pp. 1–2
  • Temporal contract composition and quotient require eliminating interface variables, a computation not previously known for contracts with temporal assumptions and guarantees.Exact automata-based elimination can require costly complementation, and its result may not be expressible in LTL.Source: §1 · p. 2
  • The paper develops sound context-aided elimination procedures that preserve GR(1) form and are subproblem-wise optimal within an admissible formula class.The procedures support composition and quotient and are implemented in Pacti.Source: §1 · p. 2
  • CAVE constructs a GR(1) result when contract operations produce formulas outside the GR(1) representation, using refinement or relaxation-based abstraction.The framework is demonstrated on automated emergency braking, deriving system-level contracts and compatibility conditions.Source: §1 · p. 2, Figure 1 · p. 3

2 Preliminaries

The preliminaries establish how temporal specifications and assume–guarantee contracts are represented, then introduce context-aided variable elimination as the computation underlying contract operations. An automated emergency-braking example supplies the components and interfaces used throughout the paper.

2.1 Linear Temporal Logic

  • LTL formulas describe properties of infinite traces; next and until provide temporal operators, while always and eventually are derived operators.Under a background theory, atomic predicates may range over typed variables evaluated along the trace.Source: §2.1 · p. 3

2.2 The GR(1) Fragment

  • GR(1) organizes environment and system requirements into initial, invariant, and liveness clauses, whose cores use typed predicates and finitely many next operators.Bounded-next terms can be mapped to indexed variables, reducing each core to a finite propositional or SMT formula.Source: §2.2 · pp. 3–4

2.3 Assume–Guarantee Contracts

  • Contracts pair assumptions with guarantees, and composition and quotient are among the algebraic operations that relate component contracts to system-level contracts.Computing these operations requires eliminating irrelevant variables in context; refinement and relaxation CAVE formulate the two required quantifier-elimination problems.Source: §2.3 · pp. 4–5

2.4 GR(1) Specifications as Contracts

  • GR(1) specifications can be translated directly into contracts by collecting assumptions and guarantees into initial, invariant, and liveness parts.The paper’s objective is to derive bounded-next GR(1) CAVE procedures that instantiate contract-operation algorithms.Source: §2.4 · p. 5

2.5 Running Example: Automated Emergency-Braking

  • The running AEB model combines a safety supervisor, vehicle response, and predicted-clearance component to derive component and environment requirements for obstacle clearance.Composition eliminates internal variables u, MOV, DCL, and STP; composing with the clearance component also eliminates v, leaving z visible. The vehicle tracks commands within ±ϵ, and the target contract specifies a one-step safety bound and recurring clear-mode progress.Source: §2.5 · pp. 5–7

3 Related Work

Prior temporal-logic work addresses quantified formulas and contract verification, refinement, or synthesis, but does not compute temporal contract operations by eliminating irrelevant variables. The paper distinguishes its GR(1)-preserving CAVE approach from these lines of work.

Quantification in Temporal Logic

  • Automata-based temporal quantification can eliminate existential propositions, while universal quantification requires Büchi-automaton complementation; CAVE instead returns quantifier-free GR(1) results.The comparison with Spot reports complementary scaling, and CAVE returns a GR(1) formula while exact elimination returns a Büchi automaton.Source: §3 · pp. 7–8

Contract Theories and Tools for Temporal Logic

  • Temporal contract tools verify or tune designer-supplied refinements, or state operations syntactically, but are described as not eliminating irrelevant variables to compute temporal composition or quotient.Pacti computes contract operations for propositional and linear-arithmetic specifications.Source: §3 · p. 8

GR(1) Specifications: Decomposition, Hiding, and Synthesis

  • GR(1) work on hiding variables decomposes system specifications into component contracts, whereas this paper starts with given component contracts and eliminates variables through composition and quotient.Strong-merge work does not require CAVE; other cited temporal-logic contract methods target verification or controller synthesis rather than computing these operations.Source: §3 · pp. 8–9

4 GR(1) Context-Aided Variable Elimination

The section develops context-aided variable elimination (CAVE) procedures that reduce bounded-next GR(1) elimination subproblems to finite SMT formulas while retaining GR(1) structure. The procedures are sound and optimal within their admissible finite-subproblem class, whose restrictions can exclude some consequences of unrestricted temporal elimination.

4.1 Bounded-Next CAVE

  • CAVE flattens bounded-next cores over finite windows, preserving their semantics and reducing each elimination subproblem to finite propositional or SMT quantifier elimination.It quantifies over indexed copies of eliminated variables while using shifted invariant context that holds at the positions addressed.Source: §4.1 · p. 10
  • The admissible class excludes dependencies across obligations and unbounded-depth consistency, so finite-window solutions can miss GR(1)-expressible consequences requiring earlier invariant information.For example, unrestricted elimination can yield an exact refinement while the admissible invariant subproblem yields ⊥; unrestricted exact invariant relaxation may require increasingly deep consistency conditions.Source: §4.1 · p. 11, §4.3 · p. 16

Refinement.

  • Refinement solves initial, invariant, and liveness subproblems separately, selecting among a synthetic branch and context-liveness support branches for each liveness target.Candidates are individually sound; branch selection affects result strength, and no optimality is claimed across branches with different temporal operators.Source: Refinement · pp. 11–12

Relaxation.

  • Relaxation derives consequences from context and target liveness cores, then removes equivalent or redundant recurrent requirements while preserving their conjunction exactly.Its complete result is strongest within the decomposed finite-subproblem class, though invariant elimination need not be exact under unrestricted infinite-trace elimination.Source: Relaxation · p. 13

Complexity

  • CAVE’s symbolic cost depends on eliminated-variable count, window depth, liveness cores, and the modulo theory; tested Boolean cases scaled more steeply than linear-real-arithmetic cases.For Boolean substitution with DB = 1, refinement rose from 0.06 s at two eliminated variables to 27 s at six, while linear real arithmetic stayed below 0.8 s through eight.Source: Complexity · p. 14

Empirical comparisons

  • Spot is faster on small instances and seven eliminated variables, while CAVE handles one to eight liveness conjuncts in 0.05–0.36 s versus Spot exceeding 300 s at six.On seven variables, Spot takes 7.8 s and CAVE 137 s; CAVE is sound but not necessarily equivalent, unlike the exact automaton.Source: Empirical comparisons · p. 14

4.3 Soundness and Optimality

  • Flattening and quantifier elimination give sound GR(1) refinement and relaxation results, with weakest refinements and strongest relaxations for each admissible finite subproblem.The complete relaxation is also strongest within the decomposed finite-subproblem class; refinement branch choices do not imply complete-refinement optimality.Source: §4.3 · pp. 14–15

5 GR(1) Contract Operations in Pacti

Pacti uses the GR(1)-specific CAVE procedures as variable-elimination primitives for contract operations, while retaining its existing contract algebra. In the emergency-braking case study, computed composition and quotient contracts expose component compatibility conditions, and the refinement checker verifies the composed contract against the target.

5 GR(1) Contract Operations in Pacti

  • Pacti instantiates its unchanged contract algebra with GR(1)-specific CAVE primitives; composition is a sound relaxation, quotient a sound refinement, and merging is exact after lifting to a compatible union interface.Operations invoke CAVE when irrelevant variables must be eliminated and retain generated GR(1) contracts for subsequent operations.Source: §5 · p. 16

5.1 Running Example: Composition and Quotient

  • The computed composition exposes the compatibility condition clear ⇒ d ≥20, and the quotient adds supervisor command-safety and recurrent-progress requirements for clear conditions.The computed relaxed composition gives mode-wise clearance bounds, while Pacti verifies that the existing supervisor meets the computed quotient requirements.Source: §5.1 · pp. 17–18
  • The refinement checker establishes that the composed supervisor and vehicle satisfy the target’s safety bound and recurrent progress, using invariant-assisted recurrence at horizon h = 0.Computing the composed contract and quotient takes a median of 0.93 s over 10 runs, including 0.48 s in CAVE.Source: §5.1 · p. 18

6 Conclusion and Future Work

The paper presents a bounded-next GR(1) contract framework with sound CAVE procedures and finite symbolic support for contract operations. An emergency-braking study and synthetic experiments illustrate its use and computational scaling; future work targets broader verification and evaluation.

6 Conclusion and Future Work

  • The framework implements composition, quotient, merging, and refinement analysis in Pacti, with the emergency-braking study deriving system-level requirements and compatibility conditions.The study illustrates how component specifications interact at the system level.Source: §6 · p. 18
  • Experiments indicate that cost grows steeply with the number of eliminated variables but only linearly with the number of liveness conjuncts.Source: §6 · p. 18
  • Future work includes more complete temporal refinement verification, less conservative CAVE branch selection, extensions beyond bounded-next GR(1), and evaluation on larger compositional systems.Source: §6 · p. 18
  • The implementation, examples, tests, scripts, and raw experimental measurements are planned for release in an archived artifact with a persistent identifier upon acceptance.The artifact link is withheld during double-blind review.Source: §6 · p. 19

Appendices

The appendix gives the Pacti implementation’s GR(1) contract-operation algorithms, built on structured CAVE procedures for eliminating irrelevant variables while retaining bounded-next GR(1) form.

A GR(1) Contract-Operation Algorithms

  • The algorithms operate on GR(1) contracts whose interfaces distinguish inputs and outputs and whose assumptions and guarantees are represented in separate Init, Inv, and Liv buckets.Source: A GR(1) Contract-Operation Algorithms · p. 23

A.1 CAVE primitives

  • Refinement CAVE returns a variable-free strengthening of the exact universal elimination, while relaxation CAVE returns a variable-free weakening of the exact existential elimination.Source: §A.1 · p. 23
  • The procedures need implication soundness rather than equality with quantified formulas, and project initial, invariant, and liveness obligations separately under finite shifted invariant contexts.Source: §A.1 · p. 23

A.2 GR(1) Refinement

The appendix specifies structured algorithms for GR(1) refinement verification, composition, quotient, and merging, and establishes the soundness and scope of their results.

A.2 GR(1) Refinement

  • The structured refinement verifier checks initial, invariant, and liveness obligations using finite shifted-invariant certificates; a successful check certifies refinement, but failure is inconclusive.The search bound hmax limits certificates considered, not the semantic horizon; some valid implications have no certificate of this finite-shift form.Source: §A.2 · p. 25
  • A complete refinement verifier would need temporal reasoning for unbounded invariant propagation and general interactions between invariant and recurrence obligations.Source: §A.2 · p. 25

A.3 GR(1) Composition

  • The composition algorithm returns a sound GR(1) relaxation of exact composition, while its composability condition rules out bidirectional cycles that feed assumption-constrained inputs.Separate structured eliminations may discard correlations that unrestricted temporal quantifier elimination would retain.Source: §A.3 · pp. 27–28

A.4 GR(1) Quotient

  • The computed quotient refines the exact quotient and is therefore a sound missing-component specification; failure to establish an assumption implication selects a more conservative fallback.Source: §A.4 · p. 29

A.5 GR(1) Merging

  • After lifting contracts to a compatible union interface, merging is exact and requires no variable elimination; it retains liveness cores as separate recurrence obligations.Source: §A.5 · p. 30

B Setting for Proofs

The proof setting quantifies over temporal valuations of typed variables, then uses temporal facts about liveness and quantifier behavior to support the arguments.

B Setting for Proofs

  • A trace assigns each typed variable a value at every time, and quantification over a variable ranges over all of its temporal valuations.Source: B Setting for Proofs · p. 30

C.1 Temporal Facts

  • The temporal facts show that invariant implication propagates liveness, existential quantification commutes one way with always, and a stronger liveness obligation makes an implied weaker one redundant.Source: §C.1 · p. 31

C.2 Bounded-Next Elimination

Bounded-next elimination reduces temporal obligations to finite windows, where invariant guards and liveness support establish the lifted GR(1) results. Exact finite quantifier elimination gives weakest refinement and strongest relaxation conditions for each subproblem.

C.2 Bounded-Next Elimination

  • A globally valid invariant implies every finite sequence of its next-shifted copies.This is the shifted-consequence property used to form finite-window obligations.Source: §C.2 · p. 31
  • An invariant holding at every time supplies all shifted invariant instances needed to guard a finite window of depth DB.Each shifted core has next-depth no greater than DB, so it can be evaluated within that window.Source: §C.2 · p. 31
  • Fixed-support liveness requires the target and support recurrence to hold at the same time; their separate recurrences do not suffice.Alternating a and ¬a can satisfy both recurrences while the target ⊥ never recurs.Source: §C.2 · p. 32
  • Bounded-next existential relaxation projects a finite window, whose witnesses establish that the resulting liveness condition recurs.For any starting time, a recurring target supplies a later witness position; the shifted invariant guards the window there.Source: §C.2 · p. 32
  • Universal elimination yields the weakest variable-free condition sufficient for a finite obligation, while existential elimination yields its strongest variable-free consequence.These optimality claims concern propositional or SMT formulas over finite windows.Source: §C.2 · pp. 32–33

D.1 Soundness of Context-Aided Variable Elimination by Refinement

The refinement and relaxation CAVE procedures are sound: each produces a GR(1) result that satisfies the corresponding implication after eliminating irrelevant variables. Their proofs rely on finite-window obligations, invariant guards, and branch-wise liveness reasoning.

D.1 Soundness of Context-Aided Variable Elimination by Refinement

  • For fixed-support refinement, the support recurrence supplies a position where the projected implication yields the recurring target.Separate recurrences of the support and candidate are insufficient because they may hold at disjoint positions.Source: §D.1 · pp. 33–34
  • Refinement CAVE returns a variable-free GR(1) formula whose conjunction with the context implies the target.The proof establishes initial and invariant obligations by finite-window reasoning and handles each liveness branch with a sound candidate.Source: §D.1 · pp. 33–34

D.2 Soundness of Context-Aided Variable Elimination by Relaxation

  • The relaxation proof establishes only the one-sided finite-window direction from a single valuation satisfying □F to □∃p.F.It does not assert the converse equivalence.Source: §D.2 · p. 34
  • SelectLiveness preserves the conjunction when it removes tautologies, equivalent duplicates, or cores implied by retained cores.Its implication test is incomplete for temporal redundancy, but this affects simplification only, not the returned conjunction's equivalence.Source: §D.2 · pp. 34–35
  • Relaxation CAVE returns a variable-free GR(1) consequence of the existentially projected context-and-target conjunction.The proof establishes initial, invariant, and liveness implications using finite-window witnesses and liveness reduction.Source: §D.2 · pp. 34–35

E Optimality Proofs

The optimality results are restricted to admissible finite-subproblem classes, not unrestricted temporal quantifier elimination. Relaxation has a complete decomposed-class guarantee, whereas refinement optimality is only subproblem-wise.

E Optimality Proofs

  • Refinement cores are weakest within each fixed finite subproblem or certificate branch, but no complete-refinement optimality is established.Different liveness branches can be incomparable, so independent branch selection need not produce an undominated conjunction.Source: E Optimality Proofs · pp. 35–36
  • Finite core implication does not compute exact temporal dominance between different liveness branches.Bounded-next windows can overlap across successive positions.Source: E Optimality Proofs · p. 36
  • Each finite relaxation subproblem yields its strongest variable-free consequence, including its invariant and pre-reduction liveness cores.This is an optimality claim within the admissible branch classes, not unrestricted temporal elimination.Source: E Optimality Proofs · pp. 35–36
  • Relaxation returns the strongest admissible complete consequence within the decomposed finite-subproblem class.The class excludes joint consequences that depend on relationships between distinct subproblems.Source: E Optimality Proofs · p. 36

F Computational Evaluation

The evaluation measures CAVE on synthetic and AEB benchmarks, using warm-call medians and bounded runs. Across tested families, cost is driven by eliminated indexed variables and grows linearly with liveness conjuncts; results are implementation measurements, not general asymptotic bounds.

F Computational Evaluation

  • The appendix organizes E1–E8 and E6b around cost, finite-horizon comparison, soundness and exactness, composition chains, automata comparison, implementation choices, and AEB operations.The measurements apply to the tested implementation and ranges.Source: F Computational Evaluation · pp. 36–37
  • CAVE cost is governed by eliminated indexed variables and grows steeply on Boolean families, while linear-real runs stay below 0.8 s over the tested range.Cost grows linearly with liveness conjuncts; synthetic families isolate cost drivers rather than represent GR(1) specifications generally.Source: F Computational Evaluation · p. 37

F.1 Terminology and Measured Quantities

  • The evaluation tracks eliminated variables, window depth, liveness-core counts, quantified dimension, and QE runtime share as measured quantities.Each irrelevant variable expands to DB + 1 indexed variables across the finite window.Source: §F.1 · pp. 37–38

F.2 Measurement Protocol

  • Reported runtimes are medians of successful warm calls, with timeouts treated as censored observations rather than included in medians.Workers have hard limits; E4 has no repetitions and no timing.Source: §F.2 · pp. 38–39

F.3 Benchmark Families

  • The benchmark families vary one parameter at a time, with other parameters fixed; the depth sweeps measure syntactic window depth rather than changed logical content.Shifted invariant copies beyond the first are implied under □, and no preprocessing step removes them.Source: §F.3 · pp. 39–40

F.4 Scaling with the Problem Parameters (E1 and E2)

Across the experiments, CAVE’s cost varied with quantified dimension, liveness cores, and composition size; an unrolled baseline was faster only at short horizons. Random-instance tests observed no unsound results, but their small synthetic scope limits what they establish about practice.

F.4 Scaling with the Problem Parameters (E1 and E2)

  • In the substitution family, refinement runtime rose from 0.026 s at np = 1 to 26.9 s at np = 6, while all ten np = 8 repetitions timed out.Boolean-family runtime also grew steeply with depth; in the Boolean-bound family, refinement timed out at (np, D) = (4, 3) and (6, 2).Source: §F.4 · p. 40, Table 3 · p. 41, Table 4 · p. 41
  • For substitution-family refinement, QE’s time share rose from 0.19 at np = 1 to 0.78 at np = 6; linear-real cases stayed below 0.708 s with no timeouts.The authors attribute steep Boolean-family growth to QE case-splitting, not temporal construction, and make no claim about an exponential base.Source: §F.4 · pp. 40, 42, Figure 5 · p. 43
  • Runtime grew approximately linearly with the number of liveness cores; refinement took 9.2–9.8 ms per candidate in the substitution family.Relaxation time increased by 0.021 s per added liveness core.Source: §F.4 · p. 42

F.5 Comparison with Finite-Horizon Unrolling (E3)

  • The interface-matched unrolled baseline was faster than CAVE through T = 2, slower from T = 3, and timed out at T = 6.CAVE took 0.308 s with simplification and 0.124 s without it, independently of T; unrolled results cover only the first T steps and omit liveness.Source: §F.5 · pp. 43–44, Table 5 · p. 44, Figure 6 · p. 44

F.6 Soundness and Precision on Random Instances (E4)

  • No unsound result appeared in 16,000 classifications (Wilson upper bound 0.05% per direction); refinement was exact on 69.4% of instances and relaxation on 90.6%.Refinement exactness was 96.9% for nonblocking contexts versus 26.1% for blocking contexts; these random small instances do not represent engineering specifications.Source: §F.6 · p. 45, Table 6 · p. 47
  • The random-instance precision percentages indicate where conservatism arises, not how often it occurs in practice.The study examined random small instances and bounded lasso words.Source: §F.6 · pp. 45, 47

F.7 Chains of Compositions (E5)

  • Balanced composition of eight stages took 1.79 s, 35% less than the 2.77 s left fold, but produced 106 rather than 96 DAG nodes.The left-fold step cost grew with the accumulated contract; CAVE accounted for 53–57% of time and QE for 5.0–7.8%.Source: §F.7 · pp. 47–48, Table 7 · p. 48, Figure 8 · p. 48

F.8 Comparison with Exact Automata-Based Elimination (E6 and E6b)

CAVE and exact Spot elimination have complementary scaling: Spot excels with few liveness conjuncts or many irrelevant variables, while CAVE performs better when complementation becomes costly. The section also reports implementation trade-offs, AEB runtimes, and evaluation boundaries.

F.8 Comparison with Exact Automata-Based Elimination (E6 and E6b)

  • Spot is 4.4–16.8 times faster on the small E6 instances, while CAVE is sound but not exact on all 15 checked instances.The highest-Spot-cost instances could not be checked, and the authors did not determine whether exact results can be expressed as GR(1) formulas.Source: Table 8 · p. 49, §F.8 · pp. 49, 52, Table 11 · p. 53
  • At five liveness conjuncts CAVE is 269 times faster than Spot, while Spot is faster at three; Spot times out at six.Complementation grows sharply with added liveness conjuncts; CAVE takes 0.046–0.358 s across one to eight liveness cores.Source: Table 9 · p. 51, §F.8 · p. 51
  • For irrelevant variables, Spot takes 7.8 s at np = 7 versus CAVE's 137 s; with increasing depth, CAVE grows to 11.8 s while Spot takes 0.002–0.009 s.At np = 6, CAVE takes 20.3 s versus Spot's 0.90 s; the depth sweep leaves the automaton unchanged at eight states.Source: §F.8 · pp. 51–52, Table 10 · p. 52

F.9 Implementation Ablations (E7)

  • Ablations show no uniformly fastest QE tactic; disabling simplification makes AEB 2.5 times faster but produces 17 cores instead of five.Synthetic-only candidates take 0.173 s on AEB and return four cores instead of five; on the Boolean-bound instance, support candidates do not contribute.Source: §F.9 · p. 53, Table 12 · p. 54

F.10 AEB Performance (E8)

  • The AEB composition and quotient take 0.718 s and 0.208 s, respectively, totaling 0.927 s; CAVE accounts for 52% of that total.QE takes 0.254 s, or 27% of the total and 52% of CAVE time; the computation uses 11 CAVE calls and 23 QE applications.Source: §F.10 · pp. 54–55, Table 13 · p. 55

F.11 Limitations of the Evaluation

  • Evaluation runtimes are bounded by a single machine, Python implementation, and Z3 and Spot versions; synthetic families isolate cost drivers, and timeouts are censored.The automata comparison uses one Spot pipeline and a stress family designed after the initial comparison; about half of E8 time is outside CAVE.Source: §F.11 · p. 55
Loading 2610.37534v1…