Before Agents Act: Assurance-Aware Semantic Scheduling for Evidence Acquisition in Distributed Systems
arXiv:2609.34376v1 [cs.DC] 28 Sep 2026
Jun He OpenKedge.io
Deying Yu OpenKedge.io
Abstract
Cognitive Admission Control (CAC) “What evidence is required?”
Tool-using agents can initiate consequential infrastructure changes, yet evidence required for admission may expire while other checks run or depend on a shared fault domain. We formulate evidence acquisition as joint witness selection and scheduling under quorum, diversity, freshness, deadline, and resource constraints. Assurance-Aware Semantic Scheduling (AAS) combines integer-program selection, dispatch-aware temporal scheduling, bounded diagnostic expansion, and receipt-aware repair. Formal results state the assumptions needed for dispatch-time freshness and finite diagnostic expansion. In three generated infrastructure workloads, AAS produces 1,075/1,200 valid candidates versus 647/1,200 for constraint-aware forward scheduling; stale candidates fall from 440 to 12. Paired sensitivity studies reuse the same instances and operation latency draws across parameter settings. A corrected timeout intervention finds 18/20 admissions with repair or full resynthesis versus 0/20 for a static plan, with lower committed cost when receipts are reused. On 20 constructed cases requiring a certified decomposition cut, refinement recovers an oracle-matching feasible plan every time. These are controlled simulation results; the bounded oracle shares a temporal search component, and transfer to deployed systems remains untested.
1
Maps risk ρ(q, s) to obligations Ω(q, s) Obligations Ω(q, s)
Assurance-Aware Semantic Scheduling (AAS) “How is that evidence acquired in time?” Selects and schedules operations in plan π Witness Manifest Wq & Cert Cq
Transactional Context Tracking & Execution (TCT) “When can the action commit?” Enforces atomic dispatch and single-use admission
Figure 1: The Post-Deterministic Distributed Systems (PDDS) control stack. AAS bridges the architectural gap between declarative admission specification (CAC) and transactional execution (TCT). Given a set of assurance obligations, how should an autonomous system acquire, schedule, refresh, and compose the evidence needed to satisfy them under cost, latency, freshness, dependency, and fault-domain constraints? Consider a concrete operational scenario: an autonomous agent proposes a failover of a primary PostgreSQL cluster. CAC dictates that admission requires: (i) a verified cluster topology snapshot, (ii) an independent confirmation of replication lag ≤ 100 ms, (iii) a cryptographically signed node fencing receipt, (iv) an Epistemic Fault Domain (EFD) diversity cut κE ≥ 2, and (v) evidence freshness ∆t ≤ 5 s. Although the admission requirements are explicit, the execution runtime faces a complex web of operational dilemmas:
Introduction
Agents that operate shared infrastructure may propose database failover, network isolation, access-control changes, or deployment rollouts. Authorization alone does not establish that the current system state supports a proposed action. Cognitive Admission Control (CAC) [1] expresses this additional requirement as risk-conditioned obligations Ω(q, s) = {ω1 , . . . , ωk } for action q in modeled state s. The admission gateway discharges each obligation against typed evidence before allowing dispatch. The gateway defines the evidence required for admission. It does not select verifiers or schedule their execution. The resulting systems question is:
• Operation Selection & Multi-Obligation Coverage: Should the runtime query low-level telemetry, invoke a heavyweight formal verification tool, run an in-memory simulation, or query a redundant model verifier? An attestation from a consensus coordinator might satisfy both topology and fencing obligations simultaneously.
1
• Temporal Freshness Intersection: If fencing verification requires 6 s, while replication lag evidence expires after 5 s, a serial schedule A → B → C will arrive at dispatch with stale replication evidence. The scheduler must coordinate operations such that T their validity intervals overlap at dispatch time: i ValidityInterval(ei ) ̸= ∅.
3. Fault-domain-aware selection. An integer program assigns witnesses to obligations while enforcing modeled EFD cuts and charging shared operations once. A decomposed solver coordinates selection with temporal feasibility; cost optimality requires exact subproblem search and full cost modeling (Section 5). 4. Consequential diagnostics and repair. Risk stratification bounds recursive sub-admission under explicit timeout assumptions. A generation-aware controller replans from the live clock, excludes failed operations, and reuses receipts only while their original observations remain valid (Sections 6 and 7).
• Epistemic Dependencies vs. Cost: An optimizer selecting the cheapest verifiers may select two distinct services that secretly depend on the same faulty upstream telemetry broker, violating κE ≥ 2 and inducing commonmode admission failure. • Consequential Diagnostic Actions: To verify rollback feasibility, the system might need to execute an active database probe or snapshot lock. But that diagnostic probe is itself a mutating, consequential operation that requires its own admission certificate, risking recursive deadlocks.
5. Controlled evaluation. Generated infrastructure workloads and paired sensitivity studies measure admission, freshness, diversity, and cost. Selected-operation timeout trials isolate receipt reuse from resynthesis and a static control; constructed cut-producing cases test both supported refinement certificates against a bounded exact oracle (Section 9).
• Adaptive Replanning Under Shifted Risk: If early evidence reveals that the candidate replica is partially degraded, the risk profile shifts from ρ0 to ρ1 , altering the required obligation set Ω0 → Ω1 and requiring dynamic schedule adaptation.
Section 8 gives the reference controller and algorithms; Section 9 describes the evaluation.
The timing problem matters because agent tool use increasingly crosses an authorization boundary at execution time [2]. Additional reasoning cannot replace a current observation of a partitioned switch, and an early observation can expire before a slow independent check completes. Verificationportfolio work, including VP-CONTROL [3], studies verifier selection, evidence-source diversity, and commit-time guards; AAS adds an explicit schedule for expiring operational evidence and for diagnostics that themselves require admission. Classical task scheduling supplies precedence and capacity constraints, but the admissibility of an evidence plan also depends on witness independence and validity at dispatch. 1.1
2
Background and Motivation
2.1
Cognitive Admission Control (CAC) Recap
Cognitive Admission Control (CAC) [1] defines an admission boundary for agentic systems operating in high-consequence environments. When an agent proposes a mutating action q at modeled state s, the control plane evaluates a multidimensional risk vector: ρ(q, s) = ⟨C, Bblast , I, U, Dexp , P ⟩ ∈ R,
(1)
capturing consequence severity (C), blast radius (Bblast ), irreversibility (I), observational uncertainty (U ), dependency exposure (Dexp ), and adverse plausibility (P ). Based on ρ(q, s), the admission policy Π resolves a set of mandatory assurance obligations:
Contributions
We study Assurance-Aware Semantic Scheduling (AAS) through five contributions:
ΩΠ (q, s) = FΠ (ρ(q, s), q, s) = {ω1 , ω2 , . . . , ωk }.
1. Problem formulation. ASP selects and schedules evidence-producing operations under hard admission, budget, and deadline constraints. It separates prospective feasibility from the gateway’s decision on realized receipts (Section 3).
(2)
Each obligation ω ∈ Ω defines a formal predicate ϕω , acceptable evidence classes Eω , structural quorum constraints, validity duration ∆tω , and epistemic diversity requirements κE (ω) ≥ k. To satisfy an obligation ω, the system must provide a set of cryptographic evidence receipts W ⊆ E. The evaluator computes a deterministic ternary discharge:
2. Temporal scheduling. A dispatch-time freshness criterion and backward scheduler place short-lived observations after slower checks when precedence permits. The guarantee is conditional on modeled latency and clock bounds; runtime receipts are checked again at the gateway (Section 4).
Discharge(ω, E, s, χ) ∈ {S ATISFIED(W ), V IOLATED(W ), U NKNOWN(c)}, (3) 2
where χ denotes the evaluation context. If all required obligations return S ATISFIED, the controller mints a single-use admission certificate Cq containing an immutable proposal digest, the witness manifest Wq = {(ω, Wω )}, state version guards Gq , and an expiry bound texp . The execution gateway validates Cq and performs an atomic compare-and-swap on the certificate nonce before forwarding the action to external infrastructure. 2.2
launches alag Just-in-Time on [6.0, 7.2] s, ensuring all validity intervals overlap at dispatch tdispatch = 7.2 s (Case B). Pathology 2: Common-Mode Epistemic Correlation. Assume ωlag requires an Epistemic Fault Domain cut κE ≥ 2, mandating two structurally independent witnesses. The scheduler can query three verifiers: • Verifier VA : cost $0.01, latency 400 ms, queries Prometheus node-exporter S1 .
Reasoning vs. Evidence Acquisition
• Verifier VB : cost $0.01, latency 450 ms, queries CloudWatch agent S2 .
A critical theoretical finding in CAC is the non-fungibility of cognitive resources and empirical evidence. Let R denote a cognitive resource budget encompassing model reasoning tokens T , context window Cctx , tool invocations Atool , and verification compute Vcpu . The epistemic lifecycle follows a strict two-stage transformation: acquisition
discharge under Π
R −−−−−→ E −−−−−−−−−→ Admission Verdict.
• Verifier VC : cost $0.10, latency 2000 ms, executes a direct Postgres replication query S3 . A cost-minimizing scheduler (such as classic knapsack or greedy cost solvers) selects {VA , VB } for a total cost of $0.02. However, unbeknownst to the scheduler, both S1 and S2 pull their metrics from a shared telemetry proxy that has stalled due to memory pressure. Both verifiers return identical, stale lag reports. Because they share an underlying epistemic fault domain (X (VA ) ∩ X (VB ) ̸= ∅), their structural diversity cut is κE = 1. The admission controller rejects the pair. A semantic scheduler must understand epistemic dependency topology: it must recognize that {VA , VC } ($0.11) is the minimal admissible set, whereas {VA , VB } is an inadmissible waste of resources.
(4)
Allocating additional cognitive compute (e.g., test-time reasoning tokens [4] or self-reflection [5]) can synthesize more sophisticated proof strategies or optimize query parameters. However, compute cannot conjure external truth: no amount of internal reasoning can prove that an external replication stream is unpartitioned without acquiring an authentic, current receipt from an external observation channel. Consequently, cognitive resource planning must not be treated as an isolated prompt-engineering problem. Instead, cognitive compute is simply one resource category within a general systems scheduling problem that allocates both computational reasoning and empirical observation bandwidth. 2.3
Pathology 3: Remediation Deadlock from Consequential Diagnostics. To satisfy an obligation regarding storage rollback feasibility, the scheduler selects a diagnostic operation adiag that executes an ephemeral filesystem freeze and snapshot probe. However, freezing production storage is itself a consequential operation that carries high risk (ρ(adiag , s) ≥ τΠ ). Under CAC, adiag cannot execute without its own admission certificate, which demands evidence of cluster quiescence! If the scheduler spawns recursive diagnostics without well-foundedness constraints, the system enters an infinite admission cycle or deadlocks under shared budget depletion.
Motivating Failures in Naive Schedulers
To demonstrate why existing schedulers fail to satisfy assurance obligations, consider three concrete pathologies: Pathology 1: Dispatch-Time Freshness Decay. Suppose a database failover requires three obligations: ωtopo (cluster topology, valid for 30 s), ωlag (replication lag under 100 ms, valid for 5 s), and ωfence (independent confirmation that the dead primary is isolated, valid for 10 s). Measuring topology takes 1.2 s, measuring lag takes 1.2 s, while executing fencing verification requires 6.0 s. A standard serial workflow engine executes tasks in declared sequence (ωtopo → ωlag → ωfence ), as illustrated in Figure 2(Case A). Under serial dispatch, atopo executes on [0, 1.2] s, alag on [1.2, 2.4] s (yielding receipt elag valid on [2.4, 7.4] s), and afence on [2.4, 8.4] s. By the time fencing verification concludes at t = 8.4 s, the replication lag receipt issued at t = 2.4 s has already expired at t = 7.4 s (7.4 < 8.4). At the execution gateway, the certificate is rejected for stale evidence. In contrast, AAS pre-fetches long-lived topology evidence, executes long-latency fencing on [1.2, 7.2] s, and
3
The Assurance Scheduling Problem
The Assurance Scheduling Problem (ASP) maps declarative CAC obligations to a feasible, cost-aware evidenceacquisition plan. Optimality applies only under the exactsearch and full-model conditions stated in Section 5.3. 3.1
Formal Problem Inputs
An instance of the Assurance Scheduling Problem is defined by the 5-tuple: P = ⟨Ω, A, B, D, T ⟩, 3
(5)
A. Serial forward schedule: lag evidence expires before dispatch atopo 0–1.2
alag 1.2–2.4
afence (fencing verification), 2.4–8.4 s t (s) elag valid: [2.4, 7.4] s efence valid after 8.4 s elag expires at 7.4 s < dispatch at 8.4 s
B. Assurance-aware schedule: all receipts are fresh at dispatch atopo 0–1.2
afence (long check), 1.2–7.2 s alag 6–7.2
t (s) etopo valid efence valid elag valid Common validity: [7.2, 12.2] s
Figure 2: Motivating failure under naive scheduling versus Assurance-Aware Semantic Scheduling. In Case A, serial forward execution causes short-lived evidence (elag , validity 5 s, finished at t = 2.4 s) to expire at t = 7.4 s while long-latency fencing verification (afence , latency 6 s) completes at t = 8.4 s, aborting dispatch. In Case B, AAS pre-fetches long-lived topology evidence, schedules long-latency fencing early, and fires alag Just-in-Time on [6.0, 7.2] s, guaranteeing a valid dispatch freshness intersection [7.2, 12.2] s. • ℓ(a) ∈ R+ is nominal execution latency, and ℓ̂(a) ≥ ℓ(a) is a conservative upper bound accounting for network jitter and tail variance,
where each component is specified as follows: Definition 1 (Assurance Obligations Ω). Ω = {ω1 , . . . , ωk } is the finite set of required obligations emitted by the CAC policy resolver ΩΠ (q, s) = FΠ (ρ(q, s), q, s). Each obligation ω = ⟨ϕω , Eω , ∆tω , κmin E (ω), Qω ⟩ specifies:
• tok(a) ∈ N0 is cognitive token consumption (for LLM verifiers or reasoning-based checkers),
• a semantic predicate ϕω : S ∗ × E∗inst → {true, false},
• Cov(a) ⊆ Ω × E denotes the modeled potential coverage: pairs (ω, ε) indicating that a can produce evidence of class ε ∈ Eω relevant to evaluating obligation ω,
• acceptable evidence classes Eω ⊆ E (e.g., attestation, telemetry receipt, proof trace), • a maximum allowable evidence age ∆tω ∈ R+ ,
• ∆t(a) ∈ R+ is the intrinsic physical lifespan of evidence emitted by a,
• a minimum epistemic diversity cut threshold κmin E (ω) ∈ N≥1 ,
• Pre(a) ⊆ A is the set of operational prerequisites that must successfully terminate before a can execute,
• a quorum rule Qω = ⟨kω , polω ⟩ specifying required witness counts (kω ∈ N≥1 ) and authorization polarities.
• X (a) ⊆ F is the epistemic exposure set, enumerating all underlying shared fault domains (e.g., host kernels, DNS resolvers, metrics daemons, model weights) in the fault domain universe F = {f1 , . . . , fp },
Definition 2 (Assurance Operations A). A = {a1 , . . . , am } represents the catalogue of available evidence-producing operations. Each operation a ∈ A is a typed systems action characterized by: a = ⟨c(a), ℓ(a), ℓ̂(a), tok(a), Cov(a), ∆t(a), Pre(a), X (a), ρ(a)⟩,
• ρ(a) ∈ R is the operational risk vector of a, determining whether a is non-consequential (ρ(a) ≺ τΠ ) or consequential (ρ(a) ⪰ τΠ ).
(6)
When operation a executes, it produces a non-empty set of concrete evidence receipts Emit(a) ⊆ Einst . A single operation a may emit multiple receipts, and a single receipt e ∈ Emit(a) may supply witness evidence supporting multiple obligations ω ∈ Ω. Each receipt e records an observation
where: • c(a) ∈ R≥0 is financial or monetary cost (e.g., API charges, egress fees), 4
timestamp tobs (e) ≤ C(a), where C(a) is the completion timestamp of a.
3.3
Prospective Feasibility vs. Realized CAC Discharge
Pre-execution plan feasibility does not establish actual obligation discharge:
Definition 3 (Resource Budgets B). B = ⟨B$ , Blat , Btok , Brisk , Kmax ⟩ bounds total allowable dollar expenditure, end-to-end wall-clock latency, cognitive reasoning tokens, cumulative operational risk perturbation, and the maximum number of concurrent active operations Kmax ∈ N≥1 ∪ {∞}.
1. Prospective Plan Feasibility (π |=pros P): Evaluated at compile time by AAS. A plan is prospectively feasible if, under modeled capabilities Cov(a), latency bounds ℓ̂(a), and exposure sets X (a), its schedule satisfies precedence, budgets, deadline windows, quorum cardinalities, and epistemic diversity cuts. Actual execution can still exceed the latency bound or fail to emit affirmative evidence.
Definition 4 (Assurance Dependencies D). D = ⟨Dop , Depi ⟩ encodes: • Operational precedence constraints Dop ⊆ A × A, where (ai , aj ) ∈ Dop implies aj cannot start until ai S successfully completes ( a∈A {(u, a) | u ∈ Pre(a)} ⊆ Dop ),
2. Realized Obligation Discharge (Wq |=CAC Ω): Evaluated at runtime by CAC. When operations execute, they emit concrete evidence receipts Estore = S a∈Vπ Emit(a). CAC evaluates the formal predicate Discharge(ω, Estore , s, χ) for each ω ∈ Ω. An operation a with (ω, ε) ∈ Cov(a) may fail, timeout, or return evidence refuting the predicate (V IOLATED). Only when all obligations return S ATISFIED(Wω ) does CAC mint certificate Cq , granting dispatch eligibility.
• Epistemic dependency topology Depi = (A ∪ F, Edep ), defining the bipartite graph linking operations to shared failure domains (Edep = {(a, f ) | a ∈ A, f ∈ X (a)}). Definition 5 (Temporal Constraints T ). T = ⟨t0 , Tdead , δexec , δverify , δmint , δdisp , ϵskew ⟩ specifies the scheduling epoch, proposal deadline, protected execution window, receipt-verification time, certificate-minting time, gateway dispatch delay, and clock uncertainty bound, respectively. All delays are nonnegative. Define the post-completion readiness delay once as δready = δverify + δmint + δdisp .
Definition 6 (Prospectively Admissible Assurance Plan). A plan π = ⟨Vπ , Eπ , σπ , Mπ ⟩ is prospectively admissible for P, written π |=pros P, if and only if it strictly satisfies all of the following hard invariants: 1. Precedence Feasibility:
3.2
Assurance Plan Representation
∀(u, v) ∈ Eπ :
σπ (u) + ℓ̂(u) ≤ σπ (v).
(9)
An assurance plan π is a scheduled directed acyclic graph: π = ⟨Vπ , Eπ , σπ , Mπ ⟩,
2. Deadline and Execution Window Feasibility:
(7)
tdispatch (π) + δexec ≤ Tdead .
where:
3. Resource Budget Invariants: X Costtotal (π) = c(a) ≤ B$ ,
• Vπ ⊆ A is the subset of scheduled operations, • Eπ ⊆ Vπ × Vπ is the set of precedence edges satisfying Dop ∩ (Vπ × Vπ ) ⊆ Eπ ,
(10)
(11)
a∈Vπ
Latency(π) = tdispatch (π) − t0 ≤ Blat , X Tokens(π) = tok(a) ≤ Btok ,
• σπ : Vπ → [t0 , Tdead ] assigns a scheduled start time to each operation,
(12) (13)
a∈Vπ
• Mπ : Ω → 2Vπ assigns candidate witness operations Mπ (ω) ⊆ Vπ to each obligation ω ∈ Ω.
Exposure(π) =
X
∥ρ(a)∥ ≤ Brisk ,
(14)
a∈Vπ
Under conservative latency bounds ℓ̂(a), the modeled completion time of operation a ∈ Vπ is Ĉπ (a) = σπ (a) + ℓ̂(a). The nominal completion time is Cπ (a) = σπ (a) + ℓ(a). The proposed target dispatch time of the primary action q is: tdispatch (π) ≥ max Ĉπ (a) + δready . a∈Vπ
where Vπ includes each operation of any admitted diagnostic sub-plan exactly once. Shared prerequisites are likewise charged once. If a concurrency limit Kmax < ∞ is specified, then for all t ∈ [t0 , Tdead ]:
(8) {a ∈ Vπ | σπ (a) ≤ t < σπ (a) + ℓ̂(a)} ≤ Kmax . (15)
5
4
4. Prospective Witness Quorum Coverage: For each obligation ω ∈ Ω, the assigned operation set Mπ (ω) ⊆ Vπ satisfies:
A distinguishing characteristic separating assurance scheduling from standard DAG scheduling (e.g., job-shop or workflow scheduling) is that outputs expire. In traditional systems, once an intermediate artifact is computed, it remains valid indefinitely unless explicitly evicted. In epistemic systems, an evidence receipt e reflects a dynamic distributed state whose fidelity decays over time.
∀a ∈ Mπ (ω) : ∃ε ∈ Eω s.t. (ω, ε) ∈ Cov(a), (16) and the candidate witness cardinality meets the quorum rule: |Mπ (ω)| ≥ kω . (17) 5. Prospective Dispatch Freshness Overlap: For every obligation ω ∈ Ω and assigned operation a ∈ Mπ (ω), let the effective lifespan be ∆teff (a, ω) = min(∆tω , ∆t(a)). The target dispatch time tdispatch (π) and execution window δexec must be covered by the prospective validity window:
4.1
6. Epistemic Fault Domain Diversity Cut: For every obligation ω ∈ Ω, candidate witnesses Mπ (ω) satisfy: (19)
1. Observation Time tobs (e): The physical moment at which system state is sampled. For an operation scheduled at start time σπ (a) with conservative upper-bound latency ℓ̂(a) and actual latency ℓact (a) ≤ ℓ̂(a), observation occurs at σπ (a) ≤ tobs (e) ≤ Cπ (a). In the conservative worst case for expiration, state is assumed observed at invocation: tobs (e) ≥ σπ (a).
where Γω is the positive kω -of-|W | approval rule and κE (W, Γω ) is the decision-rule-relative cut in Definition 7. 7. Diagnostic Admission Invariance: For every consequential diagnostic operation a ∈ Vπ (where ρ(a) ⪰ τΠ ), Vπ contains an admitted prerequisite sub-plan πa ≺ a prospectively satisfying ΩΠ (a, s).
2. Operation Completion Cπ (a): The timestamp when computation finishes: Cπ (a) = σπ (a) + ℓact (a) ≤ σπ (a) + ℓ̂(a) = Ĉπ (a), where Ĉπ (a) is conservative predicted completion. Post-observation computation duration is ℓpost (a) = Cπ (a) − tobs (e) ≥ 0.
Let Πadm (P) = {π | π |=pros P} denote the set of all prospectively admissible plans. Under our canonical optimization contract (Contract C: Constrained Cost Minimization), the primary objective of AAS is to synthesize an admissible plan π ∗ that minimizes total financial expenditure subject to hard bounds on latency (Blat ), cognitive reasoning tokens (Btok ), operational risk perturbation (Brisk ), and CAC quorums and EFD cuts: π ∗ = arg
min π∈Πadm (P)
= arg
min π∈Πadm (P)
Costtotal (π) X c(a).
Validity Intervals, Latency, and Readiness Lifecycle
When an assurance operation a ∈ A executes, it inspects external system state at an observation timestamp tobs (e) and completes processing at completion timestamp Cπ (a) ≥ tobs (e). Distinguishing tobs (e) from Cπ (a) is vital: a distributed telemetry probe, log aggregator, or formal model checker may sample state at start, yet finish computation seconds or minutes later. To establish sound scheduling, we track the complete evidence and dispatch readiness lifecycle:
tdispatch (π) + δexec ≤ σπ (a) + ∆teff (a, ω) − ϵskew . (18)
κE (Mπ (ω), Γω ) ≥ κmin E (ω),
Temporal Freshness and Validity Intersections
3. Receipt Availability & Verification tavail (e): Emitting, cryptographically signing, transmitting, and verifying the receipt requires non-zero duration δverify ≥ 0. The receipt is available in the receipt store only at tavail (e) ≥ Cπ (a) + δverify . 4. Certificate Minting tmint : CAC evaluates the composite witness manifest Wq and mints admission certificate Cq . Minting requires that all required witness receipts have completed verification:
(20)
a∈Vπ
When multiple candidate plans achieve identical minimum financial expenditure, AAS resolves ties lexicographically by minimizing dispatch latency Latency(π) = tdispatch (π) − t0 and cumulative operational risk Exposure(π) = P a∈Vπ ∥ρ(a)∥. If Πadm (P) = ∅, AAS returns I NFEASIBLE, triggering deterministic safe refusal at the admission boundary.
tmint ≥ max Cπ (a) + δverify + δmint . a∈Vπ
(21)
5. Gateway Dispatch tdispatch : Proposal q and certificate Cq arrive at the execution gateway and complete mediation after network transit delay δdisp : tdispatch ≥ tmint + δdisp ≥ max Cπ (a) + δready , (22) a∈Vπ
6
where δready is the post-completion lead time defined in Section 3.1.
Remark 1 (Temporal Freshness vs. Physical Truth). Temporal freshness and certificate admissibility (Properties 1 and 2) are necessary epistemic proxies, but do not guarantee physical predicate truth (Property 3). If the environment experiences unmodeled out-of-band state mutations (e.g., a physical power cut or external manual override), or if policy freshness ∆tω is set more permissively than the physical state drift rate τdrift (ϕω ), a temporally fresh certificate will attest to a condition that has already ceased to hold physically. AAS and CAC guarantee rigorous epistemic admissibility under the modeled policy; ensuring physical truth requires that policy authors configure ∆tω ≤ τdrift (ϕω ).
6. Protected Execution Window: The action executes during [tdispatch , tdispatch + δexec ]. Clock Uncertainty Model. Each observer node records tobs (e) on its local clock Ci , while gateway dispatch is evaluated against the gateway clock Cgw . We model clock synchronization uncertainty under bounded skew: |Ci (t)−Cgw (t)| ≤ ϵskew for all physical times t. Hence, when an observer records tobs (e), the physical observation time expressed in the gateway’s reference frame satisfies tgw sample ∈ [tobs (e) − ϵskew , tobs (e) + ϵskew ]. In the worst case, physical observation occurred at the lower bound tobs (e) − ϵskew . When two independent observer nodes i and j compare raw timestamps directly without gateway mediation, the relative clock skew is at most |Ci (t) − Cj (t)| ≤ 2ϵskew (reconciling Section 10). Each receipt e ∈ Emit(a) carries an intrinsic validity lifespan ∆t(e). For obligation ω ∈ Ω with policy freshness bound ∆tω , the effective lifespan is ∆teff (e, ω) = min(∆tω , ∆t(e)). If e supports multiple obligations Ωe ⊆ Ω, its effective lifespan across all supported obligations is: ∆teff (e) = min ∆teff (e, ω). ω∈Ωe
Theorem 1 (Completion-Aware Dispatch Freshness Intersection). Fix an executed assurance plan π with completed operations Vπ , actual completions {Cπ (a)}, observation timestamps {tobs (e)}, and composite witness manifest Wall . Let Vreq ⊆ Vπ denote the set of all operations whose completion is mandatory prior to proposal dispatch, including both witness-producing operations Vmanifest = {a ∈ Vπ | ∃e ∈ Wall , e ∈ Emit(a)} and prerequisite operational dependencies AncDop (Vmanifest ). For a fixed completed plan and its receipts, a dispatch timestamp satisfying readiness and freshness throughout the protected execution window exists if and only if:
(23)
max Cπ (a) + δready + δexec + ϵskew
Evaluated at the gateway, receipt e expires at tgw exp (e) = tobs (e) + ∆teff (e) − ϵskew , yielding the conservative validity interval:
a∈Vreq
≤ min (tobs (e) + ∆teff (e)) . e∈Wall
This condition concerns the freshness interval. Full admission additionally requires tdispatch +δexec ≤ Tdead and the latency budget; equivalently, their upper bounds must also exceed the readiness lower bound. Equivalently, the condition holds if and only if for every required operation a ∈ Vreq and every witness receipt ei ∈ Wall :
I(e) = [tobs (e) − ϵskew , tobs (e) + ∆teff (e) − ϵskew ] . (24) Freshness, Admissibility, and Physical Truth. Sound systems engineering requires rigorously distinguishing three distinct properties:
Cπ (a) − tobs (ei ) ≤ ∆teff (ei ) − δready − δexec − ϵskew . (27)
1. Receipt Freshness: Receipt e is fresh at gateway time t if t ∈ I(e), i.e., t ≤ tobs (e) + ∆teff (e) − ϵskew .
Furthermore, for any witness-producing operation a ∈ Vmanifest emitting receipt ej ∈ Wall with observation time tobs (ej ) and post-observation latency ℓpost (a) = Cπ (a) − tobs (ej ) ≥ 0:
2. Certificate Admissibility: Certificate Cq is admissible at dispatch time tdispatch if all state version guards hold (Gq = {νs = νlive }), all obligation quorums and EFD cuts are satisfied, and all constituent witnesses remain continuously valid throughout the protected execution window: \ [tdispatch , tdispatch + δexec ] ⊆ I(e), (25)
tobs (ej ) − tobs (ei ) ≤ ∆teff (ei ) − ℓpost (a) − δready − δexec − ϵskew .
where Wall =
(28)
Non-witness prerequisite operations u ∈ Vreq \ Vmanifest emit no admission receipts and therefore have no tobs terms, but their completions Cπ (u) participate in the readiness bound (27) against all ei ∈ Wall .
e∈Wall
S
(26)
(ω,Wω )∈Wq Wω .
3. Physical Predicate Truth: The underlying physical safeguard ϕω (s(t)) holds continuously in the environment: ∀t ∈ [tdispatch , tdispatch + δexec ], ϕω (s(t)) = true.
Proof. By Equation (22), dispatch cannot occur until all mandatory operations in Vreq have completed and candidate receipts have been verified and minted: tdispatch ≥ maxa∈Vreq Cπ (a) + δready . Simultaneously, condition (25) 7
requires that for every witness receipt e ∈ Wall , the execution window end does not exceed receipt expiration on the gateway clock: tdispatch + δexec ≤ mine∈Wall (tobs (e) + ∆teff (e) − ϵskew ). Thus, admissible dispatch timestamps form the closed interval [tlower , tupper ], where:
yielding an empty validity intersection! ASAP forward execution guarantees dispatch failure whenever short-lived telemetry is gathered prior to long-latency operations. 4.3
tlower = max Cπ (a) + δready ,
To satisfy Theorem 1 without delaying action execution unnecessarily, AAS implements Backward Just-in-Time (JIT) Scheduling.
a∈Vreq
tupper = min (tobs (e) + ∆teff (e) − ϵskew ) − δexec . e∈Wall
This interval is non-empty if and only if tlower ≤ tupper , which rearranges directly to Equation (26). Condition (26) holds if and only if each term in the maximum is bounded by each term in the minimum, directly establishing pairwise equivalence (27) for all a ∈ Vreq and ei ∈ Wall . For witnessproducing operations a ∈ Vmanifest , substituting Cπ (a) = tobs (ej ) + ℓpost (a) yields Equation (28).
Analysis of Target Dispatch Feasibility: Continuous Monotonicity vs. Heuristic Artifacts. A critical theoretical question is whether the set of feasible target dispatch timestamps Tfeas ⊆ [tmin , tmax ] is continuous and monotonic, or whether it can fragment into disconnected sub-intervals. Proposition 1 (Time-Translation Invariance of Continuous ASP Feasibility). For any static ASP instance in continuous time with release epoch t0 , deadline Tdead , execution window δexec , and latency budget Blat , define the maximum legal dispatch horizon:
Example 1 (Counterexample: Failure of Observation-Only Dispatch Bounds). Consider an operation averify that samples database state at tobs (e) = 0, but executes complex consistency checking requiring latency ℓ̂(a) = 10 s, completing at C(a) = 10 s. Let effective evidence lifespan be ∆teff (e) = 8 s, with lead times δready = 0.2 s, execution window δexec = 1.0 s, and ϵskew = 0. If dispatch feasibility were naively bounded by observation time alone (max tobs + δready + δexec ≤ min(tobs + ∆t)), the inequality would evaluate to 0 + 0.2 + 1.0 = 1.2 ≤ 8.0. An observation-only scheduler would falsely declare this schedule feasible, planning dispatch at t = 1.2 s. In physical reality, receipt e does not exist at t = 1.2 s because averify is still running. Earliest legal dispatch cannot occur before tready = 10 + 0.2 = 10.2 s. At t = 10.2 s, the evidence collected at t = 0 has already expired (10.2 + 1.0 = 11.2 > 8.0). Theorem 1 correctly flags this as infeasible because max C(a) + δready + δexec = 11.2 > 8.0. 4.2
Tmax = min(Tdead − δexec , t0 + Blat ).
(30)
If (σπ , tdispatch ) is a prospectively feasible schedule, then for all forward shifts ∆ ∈ [0, Tmax − tdispatch ], the uniform time-translated schedule defined by σπ′ (u) = σπ (u) + ∆ and t′dispatch = tdispatch + ∆ is also prospectively feasible. Consequently, Tfeas is either empty or a single connected interval [t∗min , Tmax ]; it is never a disconnected union of sub-intervals. Proof. Let (σπ , tdispatch ) be feasible. Under translation by ∆ ≥ 0: (i) release constraints hold since σπ′ (u) = σπ (u) + ∆ ≥ t0 + ∆ ≥ t0 ; (ii) precedence constraints σπ′ (u) + ℓ̂(u) ≤ σπ′ (v) hold identically; (iii) dispatch readiness t′dispatch ≥ maxu (σπ′ (u) + ℓ̂(u)) + δready is preserved since ∆ appears on both sides; (iv) receipt freshness at dispatch satisfies t′dispatch + δexec − (σπ′ (u) + ℓ(u)) = tdispatch + δexec − (σπ (u) + ℓ(u)) ≤ ∆teff (u) − ϵskew , since ∆ cancels identically; (v) instantaneous concurrency |{u | σπ′ (u) ≤ t < σπ′ (u) + ℓ̂(u)}| at time t equals concurrency at t − ∆, preserving Kmax ; (vi) the deadline condition t′dispatch + δexec ≤ Tdead holds because t′dispatch ≤ Tmax ≤ Tdead − δexec ; and (vii) the latency budget condition Latency(π ′ ) = t′dispatch − t0 = (tdispatch − t0 ) + ∆ ≤ Blat holds because t′dispatch ≤ Tmax ≤ t0 + Blat .
Why Forward Scheduling Fails
Traditional workflow engines apply earliest-deadline-first (EDF) or as-soon-as-possible (ASAP) forward scheduling: operations dispatch immediately once precedence dependencies are met. Consider three operations from Section 2.3: • atopo : latency 1.2 s, lifespan ∆t = 30 s, • alag : latency 1.2 s, lifespan ∆t = 5 s, • afence : latency 6.0 s, lifespan ∆t = 10 s.
Why, then, do practical temporal schedulers encounter non-monotonic behavior across candidate targets? Nonmonotonicity is strictly an artifact of heuristic placement algorithms, rather than a property of the underlying continuous scheduling problem:
Under forward scheduling starting at t = 0, atopo finishes at t = 1.2 s (valid on [1.2, 31.2] s). Next, alag completes at t = 2.4 s, producing receipt elag whose validity window is [2.4, 7.4] s. Finally, long-latency fencing afence executes from t = 2.4 s to t = 8.4 s. Here: tlower = 8.4 s + δready > 7.4 s = tupper ,
Backward Just-in-Time Scheduling
1. Epoch Clamping: Backward propagation anchors completions to ttarget − δready and pushes starts backwards.
(29) 8
Algorithm 1 Two-Tier Backward Just-in-Time Temporal Scheduler
When ttarget is small, unconstrained starts fall before t0 . Heuristically clamping starts to σπ (u) ≥ t0 alters inter-operation spacing; as ttarget is increased without uniformly translating the earliest operations, the elapsed duration ttarget −σπ (u) grows, causing clamped receipts to expire before dispatch.
Require: Plan DAG (Vπ , Eπ ), manifest assignments Mπ , conservative latencies ℓ̂, lifespans ∆teff , epoch t0 , deadline Tdead , latency budget Blat , concurrency Kmax , guards δexec , δready , ϵguard , ϵskew , grid step τgrid Ensure: Feasible schedule (σπ , tdispatch ), I NFEASIBLE (certified structural failure), or N OT F OUND (heuristic exhaustion) 1: tCP ← ComputeCriticalPath(Vπ , Eπ , ℓ̂ + ϵguard ) 2: tmin ← t0 +tCP +δready ; tmax ← min(Tdead −δexec , t0 +Blat ) 3: if tmin > tmax then 4: return I NFEASIBLE ▷ Structural critical path exceeds deadline or latency budget 5: end if 6: Vmanifest ← {a ∈ Vπ | ∃ω, a ∈ Mπ (ω)} ▷ Tier 1: Fast Parallel Backward-JIT Search 7: for ttarget ← tmin to tmax step τgrid do 8: feasible ← true 9: Initialize Tlatest (u) ← ttarget − δready for all u ∈ Vπ 10: for each u ∈ Vπ in reverse topological order do 11: Tlatest (u) ← min Tlatest (u), min(u,v)∈Eπ σπ (v)
2. Concurrency Collisions (Kmax < ∞): Under finite concurrency, greedy placement heuristics serialize overlapping operations using local priority rules. Shifting ttarget changes which operations collide, producing discrete reorganizations of the schedule where a greedy heuristic may succeed at t1 , fail at t2 > t1 , and succeed again at t3 > t2 . Accordingly, universal binary search over [tmin , tmax ] is unsound for backward heuristics. AAS evaluates candidates across a discrete grid with step τgrid . If grid search exhausts without finding a placement, it returns N OT F OUND; provable I NFEASIBLE is reserved strictly for certified structural violations.
epoch end if if u ∈ Vmanifest then ∆tmin (u) ← minω:u∈Mπ (ω) min(∆tω , ∆t(u)) if ttarget + δexec > σπ (u) + ∆tmin (u) − ϵskew then feasible ← false; break ▷ Witness receipt expires before window ends 20: end if 21: end if 22: end for 23: if feasible then 24: if Kmax = ∞ ∨ maxt |{u ∈ Vπ | σπ (u) ≤ t < σπ (u) + ℓ̂(u)}| ≤ Kmax then 25: return (σπ , ttarget ) ▷ Fast parallel JIT placement succeeds 26: end if 27: end if 28: end for ▷ Tier 2: Authoritative Slack-Aware Temporal Solver 29: if Kmax < ∞ then 30: res ← AUTH T EMPORAL(π, Kmax , tmin , tmax , τgrid ) 31: if res ̸= N OT F OUND then 32: return res ▷ Slack-aware serialization succeeds 33: end if 34: end if 35: return N OT F OUND ▷ Grid search exhausted without valid placement 15: 16: 17: 18: 19:
Backward Propagation with Safety Margins. Given candidate target dispatch ttarget , operations are scheduled in reverse topological order. For each operation u ∈ Vπ , the latest permissible completion time Tlatest (u) is bounded by successors in Eπ and target dispatch: Tlatest (u) ≤
min
σπ (v),
(31)
Tlatest (u) ≤ ttarget − δready ,
(32)
(u,v)∈Eπ
σπ (u) = Tlatest (u) − ℓ̂(u) − ϵguard ,
(33)
where ℓ̂(u) is the conservative upper-bound latency and ϵguard is an operational safety buffer absorbing network round-trip jitter. Two-Tier Architecture, Completeness, and Limits. Tier 1 evaluates candidate target dispatch timestamps over Kgrid = ⌈(tmax − tmin )/τgrid ⌉ discrete breakpoints in reverse topological order, requiring O(Kgrid · (|Vπ | + |Eπ |)) time. When concurrency is constrained (Kmax < ∞) and parallel placement collides, Tier 1 fails conservatively. To prevent heuristic parallel failure from being mistaken for problem infeasibility, Tier 2 activates the Authoritative Temporal Solver (SolveAuthoritativeTemporal). For each candidate ttarget , Tier 2 establishes the admissible release-due interval [s(u), s̄(u)] for each operation u: s(u) = max t0 , ttarget + δexec + ϵskew − ∆tmin (u) , (34) s̄(u) = ttarget − δready − ℓ̂(u) − ϵguard .
σπ (u) ← Tlatest (u) − ℓ̂(u) − ϵguard if σπ (u) < t0 then feasible ← false; break ▷ Insufficient lead time from
12: 13: 14:
If slack-aware serialization finds a valid placement, it returns the sound schedule (σπ , ttarget ). We formally distinguish the levels of completeness and their cut semantics: 1. Soundness: Any schedule returned by Tier 1 or Tier 2 strictly satisfies all precedence, deadline, concurrency (Kmax ), and freshness window constraints. 2. Certified Critical-Path Infeasibility: If the directed critical path of prerequisites exceeds available lead time (tCP + δready > Tdead − t0 − δexec ), the instance is provably infeasible in continuous time, generating a sound structural Benders cut (47).
(35)
3. Finite-Grid Exhaustion vs. Certified Infeasibility: When candidate evaluation over a finite grid τgrid terminates without finding a placement, Algorithm 1 re-
Tier 2 then executes an event-driven forward simulation under Kmax , prioritizing ready operations by minimum slack (s̄(u)). 9
5. Capacity bound: |{u ∈ Vπ | σπ (u) ≤ t < σπ (u) + ℓ̂(u)}| ≤ Kmax for all t.
turns N OT F OUND, not certified I NFEASIBLE. Under continuous time, feasibility is a single connected interval (Proposition 1); failure of finite-grid heuristic placement cannot prove continuous infeasibility. Crucially, no heuristic failure (N OT F OUND) generates a globally valid Benders cut in the Master ILP. Exact certificates of infeasibility under general concurrency bounds require exhaustive Simple Temporal Network permutation enumeration, as implemented by our Exact Oracle (Section 9.5). Non-manifest operations are excluded from freshness checks, preventing artificial restriction of the dispatch window. 4.4
6. Deadline feasibility: tdispatch + δexec ≤ Tdead . Consequently, executing π strictly preserves completionaware dispatch readiness and witness freshness during target execution: tdispatch ≥ max Cπ (a) + δready , a∈Vπ \ [tdispatch , tdispatch + δexec ] ⊆ I(e).
and
e∈Wall
Proof. Let (σπ , tdispatch ) be any schedule returned by Algorithm 1. Both Tier 1 and Tier 2 explicitly gate schedule emission upon satisfying validation conditions (1)–(6). For every operation u ∈ Vπ , actual completion satisfies Cπ (u) = σπ (u) + ℓact (u) ≤ σπ (u) + ℓ̂(u) because execution latency is bounded by ℓ̂(u). By validation condition (3), σπ (u) + ℓ̂(u) ≤ tdispatch − δready , directly implying tdispatch ≥ maxu∈Vπ Cπ (u) + δready . Next, for each admitted witness receipt e ∈ Wall emitted by manifest operation u ∈ Vmanifest , physical observation occurs at or after start: tobs (e) ≥ σπ (u). The gateway receipt validity interval is I(e) = [tobs (e) − ϵskew , tobs (e) + ∆teff (e) − ϵskew ]. By condition (3), tdispatch ≥ σπ (u) + ℓ̂(u) ≥ tobs (e) ≥ tobs (e) − ϵskew since ϵskew ≥ 0. By condition (4), tdispatch + δexec ≤ σπ (u) + ∆tmin (u) − ϵskew ≤ tobs (e) + ∆teff (e) − ϵskew . Therefore, [tdispatch , tdispatch + δexec ] ⊆ I(e) holds for every witness receipt e ∈ Wall , preserving the freshness invariant throughout proposal execution.
Robustness to Tail Latency and Staging Protocol
Real distributed environments exhibit heavy-tailed execution latencies [6]. Let actual latency be a random variable ℓact (a) ∼ Da with conservative quantile bound ℓ̂(a) = inf{ℓ | P(ℓact (a) ≤ ℓ) ≥ 1 − αtail }. If an unpredicted stall occurs in a long-latency operation aslow , pushing completion beyond ℓ̂(aslow ), any short-lived receipts collected earlier may expire before dispatch. To decouple short-lived validity from long-latency variance, AAS employs a Dual-Stage Staging Protocol: 1. Stage 1 (Pre-fetch & Long-Latency Execution): Operations with long validity horizons (∆teff (a) ≫ ℓ̂(a)) and long latencies are dispatched early. Stochastic completion variance is absorbed while short-lived operations remain dormant. 2. Stage 2 (Synchronization Barrier & JIT Burst): As soon as all Stage 1 operations finish and their receipts are verified, the scheduler locks the exact completion timestamp tsync = maxa∈Vstage1 Cπ (a) + δverify . It recomputes target dispatch ttarget = tsync + maxu∈Vjit (ℓ̂(u) + ϵguard ) + δready and fires all short-lived operations in a tightly synchronized parallel burst.
Remark 2 (Stochastic Latency Safety Invariant). If realized latency exceeds ℓ̂(a), the runtime admission boundary preserves fail-closed freshness under the stated clock and receipt assumptions: it rejects a manifest containing any receipt that expires before tdispatch + δexec , triggering replanning (Section 7) or refusal. Tail latency can reduce admission availability. Freshness alone does not establish that the underlying physical predicate remains true.
Theorem 2 (Temporal Freshness Invariant under Bounded Latency). Suppose execution latencies are bounded by ℓact (a) ≤ ℓ̂(a) for all a ∈ Vπ . If Algorithm 1 returns a schedule (σπ , tdispatch ), then (σπ , tdispatch ) satisfies the common post-schedule validation conditions across both Tier 1 and Tier 2:
5
Epistemic-Dependency-Aware Scheduling
CAC specifies when high-consequence operations require independent witnesses. AAS encodes their declared Epistemic Fault Domain (EFD) dependencies as constraints on witness selection.
1. Release validity: σπ (u) ≥ t0 for all u ∈ Vπ . 2. Topological precedence: σπ (u) + ℓ̂(u) ≤ σπ (v) for all (u, v) ∈ Eπ .
5.1
3. Lead-time readiness: tdispatch ≥ σπ (u) + ℓ̂(u) + δready for all u ∈ Vπ .
Epistemic Fault Domains and Structural Cuts
Let F = {f1 , f2 , . . . , fp } denote the set of modeled epistemic fault domains. A fault domain f ∈ F represents an unobserved, shared point of failure—such as an operating system kernel, a hypervisor, a local network switch, a metrics
4. Witness freshness: tdispatch + δexec ≤ σπ (u) + ∆tmin (u) − ϵskew for all manifest operations u ∈ Vmanifest . 10
Proposition 2 (Correlated Selection Under Cost Minimization). Let an obligation ω require k affirmative witnesses. Suppose available verifiers partition into two sets:
scraping daemon, an external SaaS API, or a base foundation model. Each assurance operation a ∈ A has an exposure set X (a) ⊆ F enumerating modeled roots on which its correctness depends. The completed fault basis includes a distinct local root fa ∈ X (a) for each witness operation; shared roots represent correlated dependencies. Its receipts inherit at least this exposure. The gateway unions additional receipt-declared roots with the catalogued set.
• Correlated cluster Vcorr = {v1 , . . . , vm } (m ≥ k) sharing a single common telemetry exporter fproxy ∈ F, with per-operation cost bounded by c(vi ) ≤ cmax . • Independent verifier vindep with disjoint exposure (X (vindep ) ∩ X (vi ) = ∅) but higher financial cost satisfying c(vindep ) > k · cmax . P Any cost-minimizing scheduler that optimizes cost i c(vi ) without enforcing κE (W, Γω ) ≥ 2 will select k verifiers exclusively from Vcorr . The resulting witness set has κE (W, Γω ) = 1 and will be rejected by the admission controller.
Safe Default for Unknown Dependencies. If an assurance operation a has an unmapped or unknown dependency structure (X (a) = ⊥ or unspecified), it must never default to the empty set ∅. Setting X (a) = ∅ would imply that a is completely immune to all known failure domains (∀C ⊆ F, X (a)∩C = ∅), falsely granting the unmapped operation artificial epistemic independence from all other verifiers. Instead, AAS enforces the Conservative Exposure Principle: any operation with unknown shared dependencies is assigned the universal infrastructure exposure set X (a) = Finfra ⊆ F (or F if infrastructure partitions are undefined), in addition to its local root. It cannot establish independence from another witness sharing standard infrastructure.
Proof. Any Pcandidate selection W ⊆ Vcorr of size k incurs total cost v∈W c(v) ≤ k · cmax . Conversely, any candidate selection W ′ ⊂ Vcorr ∪ {vindep } of size k containing vindep must include vindep and k − 1 other verifiers; since ′ costs P are non-negative (c(v) ≥ 0), Cost(W ) = c(vindep ) + v∈W ′ \{vindep } c(v) ≥ c(vindep ) > k · cmax ≥ Cost(W ). Therefore, any cost-minimizing selection strictly chooses k verifiers exclusively from Vcorr . However, {fproxy } ∩ X (vi ) ̸= ∅ for all vi ∈ Vcorr . Thus C = {fproxy } exposes a decisive coalition, so κE (W, Γω ) = 1 < 2, causing deterministic gateway rejection.
Definition 7 (Epistemic Diversity Cut κE ). For candidate witness set W and obligation ω, let Γω be its positive kω of-|W | approval rule. Write Wmin = {Wd ⊆ W : |Wd | = kω } for its minimal decisive coalitions. A root f exposes DW (f ) = {a ∈ W : f ∈ X (a)}. Following decision-rulerelative EFD theory [7], define
5.3
κE (W, Γω ) = min{ |C| : C ⊆ F, ∃Wd ∈ Wmin , [ Wd ⊆ DW (f ) }.
The joint assurance scheduling problem (Equation (20)) requires simultaneously choosing a witness portfolio satisfying quorums, EFD diversity, and resource budgets, while constructing a feasible temporal schedule (σπ , tdispatch ) satisfying precedence Dop and evidence freshness intervals. Because joint mixed-integer non-linear optimization over continuous time and combinatorial fault cuts is computationally intractable in real-time control loops, AAS adopts a Decomposed Optimization Architecture based on LogicBased Benders Decomposition (LBBD):
(36)
f ∈C
Set the cut to zero if |W | < kω . With local roots present, 1 ≤ κE (W, Γω ) ≤ kω once a quorum is assigned. Refuting evidence vetoes admission before this positive approval rule is evaluated; arbitrary nonmonotone rules are outside the implemented model. If κE (W, Γω ) = 1, one root exposes a decisive approval coalition, even if other signatures remain independent. For three independent witnesses the cut is 2 under a 2-of-3 rule and 3 under unanimity. CAC requires κE (W, Γω ) ≥ κmin E (ω). This structural guarantee requires a complete exposure map and a sound causal account of what exposure permits; it does not establish physical predicate truth. 5.2
Optimization Architecture: Decomposed MasterSubproblem Solver
1. Master Selection Problem (0-1 ILP): Solves the combinatorial witness selection and obligation assignment problem, minimizing financial cost subject to quorums, EFD cuts, and hard resource budgets (B$ , Btok , Brisk ). 2. Temporal Scheduling Subproblem (Algorithm 1): Solves the continuous backward JIT scheduling pass over the candidate witness assignments y∗ and operational DAG G[V ∗ ] under precedence Dop and freshness intervals.
The Cost-Minimization Vulnerability
Standard portfolio optimization and LLM routing algorithms [3, 8] rank verifiers primarily by financial cost and marginal accuracy. In distributed systems, this creates a catastrophic vulnerability:
3. Sound Conflict Generation & Refinement: If the subproblem detects temporal infeasibility, it distinguishes 11
The Sound Master Selection ILP. For each operation a ∈ A and obligation ω ∈ Ω, let Eligible(a, ω) ⇐⇒ ∃ε ∈ Eω s.t. (ω, ε) ∈ Cov(a). We formulate the Master ILP under Contract C: X min c(a) · xa (37)
assignment-induced freshness conflicts from structural precedence bottlenecks, generating provably sound Benders cuts. Operation Roles and Distinctions. To guarantee soundness in cut generation, AAS strictly distinguishes five categories of operations:
x,y
subject to
∗
1. Selected Operations (V = {a | xa = 1}): Operations committed for execution, which consume financial cost c(a), tokens tok(a), and risk budget ∥ρ(a)∥.
a∈A
ya,ω ≤ xa
∀a ∈ A, ω ∈ Ω,
(38)
xa ≤ xu
∀a ∈ A, ∀u ∈ Prereq(a),
(39)
ya,ω = 0 ∀a, ω with ¬ Eligible(a, ω), (40) X ya,ω ≥ kω ∀ω ∈ Ω, (41)
2. Witness Assignments (y∗ = {(a, ω) | ya,ω = 1}): Operations whose emitted receipts are actively assigned to discharge obligation ω. Freshness constraints apply only to assigned pairs.
a∈A
X
ya,ω ≤ kω − 1
(42)
a:X (a)∩C̸=∅
∀ω ∈ Ω, ∀C ⊂ F s.t. |C| < κmin E (ω),
3. Manifest Contributors (Vmanifest = {a ∈ V ∗ | ∃ω, ya,ω = 1}): The subset of selected operations that produce receipts for the final admission certificate.
X
c(a) · xa ≤ B$ ,
(43)
tok(a) · xa ≤ Btok ,
(44)
∥ρ(a)∥ · xa ≤ Brisk ,
(45)
X
(46)
a∈A
X Prerequisites (Vprec = 4. Precedence AncDop (Vmanifest ) \ Vmanifest ): Operations selected through prerequisite closure that must complete before a manifest contributor can launch, even if they emit no admission receipts. Thus Vprec ⊆ V ∗ .
a∈A
X a∈A
ya,ω ≤ |Aconflict | − 1
(a,ω)∈Aconflict
5. Nonmanifest Operations (Vnonmanifest = V ∗ \ Vmanifest ): Selected operations whose receipts are unassigned or superseded, including mandatory prerequisites. Their receipt freshness does not constrain dispatch, but their completion and resource use still do.
∀Aconflict ∈ Kassign , X xa ≤ |Vchain | − 1
(47)
a∈Vchain
∀Vchain ∈ Kchain , xa ∈ {0, 1}, ya,ω ∈ {0, 1}
Counterexample: Unsoundness of Operation-Set Conflict Cuts. A naive Benders formulation adds the conflict cut P a∈Vconflict xa ≤ |Vconflict | − 1 whenever portfolio Vconflict fails temporal scheduling. This cut is unsound:
∀a ∈ A, ω ∈ Ω. (48)
The diversity row forbids any fault set smaller than the required cut from exposing kω assigned witnesses. The implementation synthesizes local roots for exact validation. In the master ILP it enumerates shared-root rows: a local root can be replaced by a declared shared root of the same witness without shrinking the exposed set, while local roots alone cannot expose a quorum with fewer than kω failures. Thus the omitted local rows are redundant when the required threshold is at most kω .
Example 2 (Alternative Witness Relief). Suppose Master ILP selects V ∗ = {a1 , a2 } with assignments ya1 ,ω1 = 1 and ya2 ,ω2 = 1. Operation a1 has long latency ℓ̂(a1 ) = 8 s, but obligation ω1 has a short freshness lifespan ∆tω1 = 3 s. The temporal subproblem determines that assigning a1 to ω1 is infeasible ([tmin , tmax ] = ∅). If the scheduler appends an operation-set cut xa1 + xa2 ≤ 1, it permanently forbids selecting both a1 and a2 in any future solution. Now suppose there exists an alternative operation a3 with short latency ℓ̂(a3 ) = 1 s that also covers ω1 , while operation a1 is also eligible to cover a third obligation ω3 with a generous lifespan ∆tω3 = 45 s. Consider the expanded portfolio V ′ = {a1 , a2 , a3 } with reassigned witnesses ya3 ,ω1 = 1, ya2 ,ω2 = 1, and ya1 ,ω3 = 1. This solution is completely feasible and may be cost-optimal! However, the naive cut xa1 + xa2 ≤ 1 incorrectly excludes V ′ , pruning a valid, optimal solution.
Formulation and Cut Semantics. • Exact Financial and Prerequisite Accounting: Constraint (38) links witness assignments to operation selection, while Constraint (39) enforces transitive operational prerequisite closure (xa ≤ xu ). This guarantees that selecting an operation automatically forces the selection of all required predecessor operations, charging each operation c(a) exactly once in objective (37) and budget P (43), regardless of multi-obligation witness coverage ( ω ya,ω ≥ 2). 12
admission, a1 admits its diagnostic sub-plan, yielding total cost Costtotal = $101.00 ≫ $5.00. While shadow reservation ledgers prevent budget overruns, global cost-optimality Costtotal requires pre-flattening diagnostic expansions into A.
• Assignment-Aware No-Good Cuts (Kassign ): When temporal scheduling fails due to evidence expiration or lack of freshness intersection, the authoritative subproblem isolates the certified minimal con∗ flicting assignments Aconflict = {(a, ω) | ya,ω = 1 active in conflict}. Constraint (46) eliminates this specific assignment without forbidding operations in Aconflict from being selected or reassigned to other obligations. When heuristic placement exhausts without certified proof (N OT F OUND), the solver applies a safe P full-candidate combinatorial no-good cut ( a:x∗ =1 (1 − a P xa ) + a:x∗a =0 xa ≥ 1) to avoid over-pruning alternative witness assignments.
Decomposition Interface, Convergence, and Optimality. The master-subproblem solver operates in an iterative loop: 1. Solve Master ILP (37)–(48). If infeasible, terminate with safe refusal (Πadm (P) = ∅). 2. Pass candidate assignments y∗ and operational DAG G[V ∗ ∪ AncDop (V ∗ )] to the Authoritative Temporal Solver (Algorithm 1).
• Precedence-Chain Structural Cuts (Kchain ): When failure is caused by an unavoidable directed precedence chain Vchain ⊆ A in Dop whose cumulative conservative latency exceeds available deadline: X (ℓ̂(u) + ϵguard ) + δready + δexec > Tdead − t0 ,
3. If the temporal solver returns a valid schedule (σπ , tdispatch ), terminate. Plan π is prospectively admissible. 4. If the temporal solver proves I NFEASIBLE:
u∈Vchain
• If the critical path of an induced precedence chain exceeds Tdead − t0 − δexec , append structural cut (47) to Kchain .
(49) latency monotonicity guarantees that any portfolio containing Vchain is temporally infeasible. Only in this structural case is the operation-level cut (47) valid.
• Otherwise, when certified by the exact oracle, isolate minimal conflicting witness assignments Aconflict ⊆ y∗ and append assignment cut (46) to Kassign . If heuristic search exhausts without certified proof (N OT F OUND), append a safe fullcandidate combinatorial no-good cut to avoid unsound pruning of unvisited assignments.
Financial Optimization Scope and Consequential Coordination. The Master ILP P objective (37) minimizes the direct financial cost Cost(π) = a∈A c(a)xa . When all assurance operations in A are non-consequential (ρ(a) ≺ τΠ ), direct cost equals total cost: Costtotal (π) = Cost(π) (Section 3). When consequential operations require diagnostic sub-plans (Section 6), cost optimization has two cases:
Return to Step 1. Theorem 3 (Convergence and Conditional Global Optimality). The decomposed LBBD algorithm terminates in a finite number of iterations. Furthermore, for any fully modeled or flattened problem P, if the master solver executes to completion without timeout (Tctrl = ∞) and the subproblem is evaluated authoritatively via an exact temporal oracle (Section 9.5), the returned plan π ∗ is globally cost-optimal over all prospectively admissible plans: X Cost(π ∗ ) = min c(a). (50)
1. Statically Modeled / Flattened Instances: If candidate diagnostic trees are fully expanded and flattened into the catalog A with their prerequisites, risks, and shared costs accounted for, the Master ILP jointly minimizes Costtotal . 2. Runtime Consequential Coordination: In dynamic systems where diagnostic sub-plans are synthesized recursively at runtime via local risk stratification (Algorithm 3), the static Master ILP optimizes direct operational cost, while recursive admission coordinates subplan synthesis and budget reservation dynamically.
π∈Πadm (P)
a∈Vπ
When evaluated under bounded concurrency Kmax < ∞ with the polynomial-time slack-priority heuristic, or upon solver timeout Tctrl < ∞, the returned plan is approximately optimized and prospectively feasible, with no claim of global optimality. Dynamic consequential sub-plans admitted at runtime are coordinated outside this static optimality guarantee.
We note that direct-cost minimization does not guarantee joint consequential optimality without flattening: Example 3 (Cheap Verifier with Expensive Diagnostics). Suppose obligation ω can be satisfied by either a1 (c(a1 ) = $1.00, but consequential with diagnostic sub-plan πa1 costing c(πa1 ) = $100.00) or a2 (c(a2 ) = $5.00, non-consequential with c(πa2 ) = $0.00). A static optimizer minimizing only direct cost strictly selects a1 ($1.00 vs. $5.00). Upon runtime
Proof. The assignment space {0, 1}|A|×|Ω| and portfolio space 2|A| are finite. Each iteration generates either an assignment cut (46) (or safe full-candidate cut) that prunes at least 13
one integer assignment vector y∗ or a structural cut (47) that prunes at least one operation subset. Both cut families are sound: structural cuts prune operation subsets whose topological critical path latency strictly exceeds the deadline window (tCP + δready > Tdead − t0 − δexec ), while assignment cuts prune certified conflicting witness assignments. When subproblem feasibility is determined via exact temporal search, no prospectively admissible plan π ∈ Πadm (P) is ever falsely pruned. Because P the Master ILP optimizes the exact linear cost objective a c(a)xa over an admissible outer relaxation, the first verified feasible candidate achieves global cost optimality over the flattened instance P. 5.4
if there exists an admissible plan of cost at most K. Full bidirectional reduction and equivalence proofs are given in Appendix A. 5.5
Progress-Based Greedy Fallback Heuristic
When the controller computation budget is constrained (Tctrl < 5 ms), AAS executes an efficient Progress-Based Marginal Score Heuristic: For an active partial plan with selected operations Vπ and assigned witnesses Wω ⊆ Vπ , define the provisional cut κ eE (W, ω) = κE (W, Γmin(kω ,|W |) ) for nonempty W , and zero for empty W . This provisional score rewards distinct roots while a quorum is assembled; admission always checks the fixed rule Γω .
Complexity and EFD Cut Separation
To understand the computational tractability of AAS, we rigorously distinguish four related problem variants:
1. Quorum Progress: ∆Q(a, ω) = 1 if Eligible(a, ω) and |Wω | < kω ; 0 otherwise.
1. Checking Diversity of a Fixed Witness Set: Given W ⊆ A and threshold h, determining whether κE (W, Γω ) ≥ h requires checking that each C ⊆ F with |C| < h exposes fewer than kω assigned witnesses. For fixed h, there are O(|F|h−1 ) candidates and each check costs O(|W |h).
Progress: 2. Diversity max(0, min(e κE (Wω κ eE (Wω , ω)).
∆κ(a, ω) = ∪ {a}, ω), κmin (ω)) − E
/ Vπ , c̃(a) = 3. Marginal Cost: If a ∈ Vπ , c̃(a) = 0; if a ∈ c(a).
2. Separating Violated ILP Diversity Cuts: Given candidate assignments (x, y), finding a violated cut C for Constraint (42) requires evaluating the O(|F|k−1 ) candidate fault sets. For k = 2, |C| = 1, so there are only |F| cuts per obligation, which can be instantiated statically!
4. Temporal Feasibility Guard: 1temp (a) = 1 if adding a to Vπ preserves a feasible JIT completion window within remaining latency and deadline bounds; 0 otherwise. At each iteration, the heuristic selects: P ω∈Ω [∆Q(a, ω) + λκ ∆κ(a, ω)] ∗ a = arg max , c̃(a) + ϵ a:1temp (a)=1 (51) where λκ > 0 weights fault-cut diversity relative to quorum count. The reference heuristic computes the exact provisional cut by enumerating root coalitions up to min(kω , |Wω | + 1); with local roots, its worst-case enumeration is O((|F| + |Wω |)kω ) for bounded quorum size. It may fail after choosing an unfavorable quorum; it is not a completeness guarantee.
3. Unbounded Cut Computation: Finding a minimum root coalition exposing a decisive quorum generalizes set-cover variants and is NP-hard for arbitrary thresholds [9]. Small fixed thresholds (h ∈ {2, 3}) permit polynomial-time checking. 4. The ASP Decision Problem: Selecting a minimumcost witness set satisfying multi-obligation coverage and quorums is NP-hard. Theorem 4 (NP-Hardness of ASP Decision Problem). The decision version of the Assurance Scheduling Problem (ASPDEC)—determining whether there exists a prospectively admissible plan π |=pros P with financial cost Cost(π) ≤ K— is NP-hard, even in the absence of precedence constraints (Dop = ∅) and with unit operation latencies.
Example 4 (Greedy Heuristic Execution Trajectories). To illustrate heuristic behavior under trade-offs: • Quorum vs. EFD Diversity: Suppose obligation ω1 requires quorum kω1 = 2 and diversity κmin = 2. E Let current witness set be W = {a1 } with exposure X (a1 ) = {f1 }. Candidate acheap (c = $0.01) has exposure {f1 }, while candidate aindep (c = $0.03) has exposure {f2 }. Candidate acheap yields ∆Q = 1, but κ eE ({a1 , acheap }, ω1 ) = 1 (since {f1 } hits both), so ∆κ = 0. Its score is 1/(0.01 + ϵ) ≈ 100. Candidate aindep yields ∆Q = 1 and ∆κ = 1. With λκ = 3, its score is (1 + 3)/(0.03 + ϵ) ≈ 133. The heuristic strictly prefers the independent verifier aindep , successfully steering away from the correlated trap.
Proof Sketch. We establish a polynomial-time reduction from M INIMUM W EIGHT S ET C OVER to ASP-DEC. Given universe U = {u1 , . . . , un } and candidate subsets S = {S1 , . . . , Sm } with weights w(Sj ), we map each universe element ui to an obligation ωi ∈ Ω and each subset Sj to an assurance operation aj ∈ A with cost c(aj ) = w(Sj ) and coverage Cov(aj ) = {(ωi , ε) | ui ∈ Sj }. Setting unit quorums, a set cover of weight at most K exists if and only
14
• Diversity vs. Temporal Deadlines: Suppose obligation ω2 requires diversity κmin = 2. Candidate asolver E provides perfect epistemic diversity (∆κ = 1), but is a heavy formal model checker requiring conservative latency ℓ̂(asolver ) = 8 s. If the remaining deadline budget is Tdead − tnow = 5 s, Backward JIT scheduling detects that asolver cannot complete before dispatch. The temporal guard evaluates 1temp (asolver ) = 0, immediately pruning asolver from consideration and preventing a dead-end plan commitment.
6
Target Action q (Primary Failover)
ωlag (Lag)
ωrb (Rollback Feasibility)
atelemetry
asnap (Snapshot Probe) Consequential (ρ(a2 ) ⪰ τΠ )
(Passive scrape)
Recursive CAC
Ω(a2 ) (Quiescence Verification)
Recursive and Consequential Acquisition alock (Flush & Check)
The CAC paper [1] identifies a remediation-liveness problem: a diagnostic action may require another diagnostic action to be admitted first. Budget bounds alone do not ensure progress. We give graph and risk conditions for finite diagnostic expansion and state the additional assumptions needed for operational liveness. 6.1
Figure 3: The Assurance Dependency Graph (ADG). Consequential diagnostic action asnap requires its own admission obligations Ω(asnap ), spawning recursive sub-scheduling. • VA ⊆ A ∪ {q} are action nodes, S • VΩ ⊆ u∈VA Ω(u) are obligation nodes, • Edge (u, ω) ∈ E indicates that action u requires obligation ω,
When Evidence Acquisition is Consequential
Not all evidence acquisition is passive telemetry scraping. In real-world distributed architectures, establishing that a complex predicate holds often requires active systems probing:
• Edge (ω, a) ∈ E indicates that operation a is scheduled to produce a witness discharging ω.
• Storage Rollback Validation: Freezing a database tablespace and mounting a copy-on-write snapshot to verify point-in-time recovery.
Without formal safeguards, recursive acquisition risks two structural pathologies:
• Network Isolation Verification: Injecting synthetic probe traffic or testing border gateway BGP route filtering.
1. Cyclic Admission Deadlock: Operation a1 requires evidence from a2 , while a2 requires evidence from a1 (e.g., verifying replication requires snapshot lock, while snapshot lock requires replication sync).
• Failover Readiness: Initiating an ephemeral dry-run transition on an auxiliary standby replica.
2. Infinite Remediation Regress: Each diagnostic probe requires a further diagnostic probe of equal or greater consequence, depleting budgets without reaching base evidence.
Under CAC, any action whose modeled operational risk equals or exceeds the policy threshold τΠ is classified as consequential:
6.3 ρ(a) ⪰ τΠ =⇒ a is consequential.
(52)
To prevent cyclic dependencies and infinite regress during plan synthesis, AAS enforces a Risk Stratification Discipline.
Because the execution gateway completely mediates all infrastructure interactions, a consequential diagnostic operation a ∈ A cannot bypass the admission boundary. The gateway will reject a unless presented with a valid admission certificate Ca satisfying its own obligations ΩΠ (a, s). 6.2
Structural Acyclicity and Bounded Expansion
Definition 9 (Strict Risk Stratification of Finite Height). Let ≺R be a strict partial order on the risk space R with finite height HR = height(R) < ∞ (i.e., every strictly descending chain has length at most HR ). An admission policy is strictly risk-stratified if, for every consequential action u, any diagnostic action a invoked to discharge ω ∈ Ω(u) satisfies:
The Assurance Dependency Graph (ADG)
This recursive dependency induces a directed bipartite graph of alternating actions and obligations (Figure 3):
ρ(a) ≺R ρ(u).
Definition 8 (Assurance Dependency Graph (ADG)). The Assurance Dependency Graph GADG = (VA ∪ VΩ , E) is a directed bipartite graph where:
Furthermore, non-consequential operations form a base stratum Rbase = {a ∈ A | ρ(a) ≺ τΠ } whose obligations are empty by policy definition: ∀a ∈ Rbase , Ω(a) = ∅. 15
(53)
Proposition 3 (Structural Acyclicity of the ADG). If an admission policy Π is strictly risk-stratified, then the Assurance Dependency Graph GADG is a directed acyclic graph (DAG).
unhandled controller delays, unbounded retries, deadlock on shared physical locks, or event-loop stalls. To establish operational liveness, AAS couples risk stratification with six explicit systems execution bounds:
Proof. Suppose for contradiction that GADG contains a directed cycle: u1 → ω1 → u2 → ω2 → · · · → um → ωm → u1 . By Definition 9, every composite step ui → ωi → ui+1 implies ρ(ui+1 ) ≺R ρ(ui ). By transitivity of the strict partial order, ρ(u1 ) ≺R ρ(u1 ), contradicting irreflexivity. Thus GADG contains no directed cycles.
Theorem 5 (Conditional Operational Diagnostic Liveness). Assume an admission policy is strictly risk-stratified of finite height HR < ∞ with bounded concrete instances Bact < ∞, yielding an expanded ADG of at most MA actions. Diagnostic evidence acquisition is guaranteed to terminate deterministically in finite wall-clock elapsed time—either minting certificate Cq or safely refusing proposal q—provided the distributed runtime satisfies:
Proposition 4 (Bounded Recursive Expansion of Bipartite ADG). Assume admission policy Π is strictly risk-stratified of finite height HR = height(R) < ∞. Let KΩ = maxu∈A∪{q} |Ω(u)| < ∞ be the maximum number of obligations per action, and let each obligation require at most Kinst < ∞ concrete action instances dynamically instantiper ated from capability templates Tcap (Kinst ≤ |Tcap | · Kinst ). Then:
1. Bounded Operation Latency: Every executed operation a ∈ A has an enforced wall-clock timeout ℓ̂(a) ≤ ℓ̂max < ∞. 2. Bounded Cancellation and Cleanup Delay: Transmitting cancellation signals and terminating an in-flight worker thread requires at most δcancel < ∞ time, and controller state cleanup requires at most δcleanup < ∞ time.
1. The maximum action-recursion depth of GADG is strictly bounded by the ordering height: depthA (GADG ) ≤ HR < ∞. 2. The effective action branching factor is finite: Bact ≤ KΩ · Kinst < ∞.
3. Bounded Controller Computation: Every invocation of the plan synthesizer, ILP solver, or replanning monitor terminates within controller computation timeout Tctrl < ∞ (falling back to greedy heuristic or refusal upon timeout).
3. The total number of concrete action nodes VA in the expanded ADG is strictly bounded by the sum: 1 d MA = |VA | ≤ Bact = HR + 1 HR +1 Bact −1 d=0 HR X
if Bact = 0, if Bact = 1,
4. Finite Retry and Generation Limits: The controller max permits at most Nretry < ∞ adaptive repair or retry attempts across the entire lifecycle of proposal q.
if Bact > 1, (54) where MA < ∞ in all cases. The total number of obligation nodes satisfies |VΩ | ≤ KΩ · MA < ∞. Bact −1
5. Deadlock-Free Resource and RPC Execution: Mutating locks or physical hardware mutexes required by concurrent diagnostic operations are acquired in a canonical total order and released within bounded time δrel < ∞ (or executed in copy-on-write sandboxes). All remote RPCs and network verifiers enforce non-blocking socket timeouts ℓ̂max , preventing unbounded waiting on external queues.
Proof. Every directed path of action nodes in bipartite graph GADG corresponds to a strictly descending sequence of risk values ρ(u0 ) ≻R ρ(u1 ) ≻R · · · ≻R ρ(ud ) alternating through obligation nodes ωi ∈ Ω(ui−1 ). Because (R, ≺R ) has finite height HR , any such chain contains at most HR action transitions. Each action node expands into at most KΩ obligation nodes, each of which links to at most Kinst candidate diagnostic actions, establishing branching factor Bact ≤ KΩ · Kinst . Summing action nodes across depths 0 ≤ d ≤ HR yields the geometric sum (54). Leaves terminate in non-consequential base actions Rbase with Ω(a) = ∅, terminating expansion in finite steps. 6.4
6. Non-Blocking Event Loop & Epoch-Relative Deadline Abort: The controller event loop never blocks indefinitely awaiting external messages; if physical wall-clock time reaches proposal deadline Tdead , all active workers are cancelled, state is reconciled, and the workflow deterministically aborts via safe refusal. Under these conditions, the total elapsed wall-clock time Tterm from scheduling epoch t0 until complete system quiescence (all worker threads terminated and resources released)
Operational Diagnostic Liveness
We emphasize an essential systems distinction: structural acyclicity and bounded expansion do not automatically imply operational termination during physical execution. A structurally acyclic plan may still hang at runtime due to 16
Initial CAC Evaluation ρ0 = ρ(q, s0 ) =⇒ Ω0 = FΠ (ρ0 , q, s0 )
is strictly bounded by: Tterm ≤ min (Tdead − t0 ) + δcancel + δcleanup ,
AAS Dynamic Scheduler Synthesize & dispatch plan π0
max (Nretry + 1) · Tctrl max + (Nretry + 1) · MA · (ℓ̂max + δrel ) max + Nretry · (δcancel + δcleanup ) < ∞. (55)
Execute Assurance Op a1 Returns receipt e1 Dynamic Replan: Splice ∆π
State Update & Risk Shift s1 = Update(s0 , e1 ) =⇒ ρ1 = ρ(q, s1 )
Proof. By Proposition 4, the number of actions in any synthesized plan DAG is bounded by MA < ∞. Under condition (5), diagnostic operations cannot deadlock on shared physical mutexes or block indefinitely on remote RPCs. Under condition (1), every launched operation either finishes or times out in at most ℓ̂max . If an operation fails, times out, or refutes a predicate, condition (2) guarantees that cancellation halts all in-flight workers within δcancel and controller cleanup finishes within δcleanup . Under condition (3), each scheduling pass completes in at most Tctrl wall-clock time. Because max condition (4) limits the number of repair attempts to Nretry , max the controller can execute at most Nretry + 1 planning phases max (1 initial synthesis plus at most Nretry repairs) and at most max Nretry cancellation/cleanup cycles before aborting. Finally, condition (6) enforces an absolute hard stop when wall-clock time reaches Tdead , with in-flight worker cancellation and cleanup completing within δcancel + δcleanup after the deadline. Hence, the system cannot livelock, deadlock, or stall indefinitely, guaranteeing deterministic termination within bound (55). 6.5
CAC Obligation Escalation Ω1 = FΠ (ρ1 , q, s1 ) with ∆Ω+ = Ω1 \ Ω0
Figure 4: The closed-loop adaptive assurance cycle. Incoming evidence updates system state s, triggering risk escalation ρ0 → ρ1 and online schedule replanning. 7.1
Consider the execution timeline illustrated in Figure 4: 1. At t0 , the controller observes state snapshot s0 and evaluates baseline risk ρ0 = ρ(q, s0 ). The policy emits obligations Ω0 = FΠ (ρ0 , q, s0 ). 2. The scheduler constructs plan π0 and dispatches an initial operation a1 (e.g., query replica replication stream). 3. Operation a1 completes, returning evidence receipt e1 . The payload of e1 reveals that the secondary replica has accumulated 45 GB of unapplied Write-Ahead Logs (WAL) and disk I/O throughput is severely degraded.
Bounded Diagnostic Capabilities
4. The world state updates to s1 = Update(s0 , e1 ). Under this degraded condition, observational uncertainty and adverse consequence plausibility increase, shifting the risk profile:
In high-throughput environments, deep recursive admission introduces unacceptable latency overhead. AAS supports Bounded Diagnostic Capabilities: pre-authorized, ephemeral execution tokens with strictly constrained blast radiuses (e.g., read-only filesystem snapshots, dedicated diagnostic tenant namespaces, or sandboxed eBPF probes). When an operation executes using a certified diagnostic capability, its effective operational risk is pre-attenuated below the policy threshold: ρeff (a) ≺ τΠ . This places a immediately in the base stratum Rbase , collapsing the ADG depth to 1 and eliminating recursive overhead.
7
Risk Dynamics and Obligation Escalation
ρ1 = ρ(q, s1 )
with
ρ1 ̸⪯ ρ0 .
(56)
5. The admission engine re-evaluates obligations under updated risk ρ1 : Ω1 = FΠ (ρ1 , q, s1 ).
(57)
Because risk increased, Ω1 contains new mandatory obligations: ∆Ω+ = Ω1 \ Ω0 ̸= ∅, (58)
Adaptive Replanning Under Partial Information
such as requiring an attestation of secondary memory headroom or escalating to human dual-control.
Static workflow planners assume that the environment remains stationary while an evidence plan executes. In reality, evidence acquisition is an active discovery process: acquiring evidence updates the controller’s knowledge of the world, which can fundamentally alter both the perceived risk of the action and the obligations required to admit it.
If the scheduler executed π0 blind to environment updates, it would arrive at the gateway with an evidence manifest satisfying Ω0 but lacking ∆Ω+ , resulting in an immediate rejection and wasted work.
17
7.2
Authoritative Runtime State Machine Σ
3. Running: Launched into an asynchronous worker thread; tagged with current generation g; financial cost committed (Bresv → Bcommit ) exactly once.
To ensure sound execution across asynchronous events, AAS defines a single authoritative runtime state Σ: Σ = q, s, ρ, Ω, g, π, Brem , Bcommit , Bresv , Jrun , Vdone , Estore , Wq , tdispatch , Tdead ,
4. Completed: Finished execution within timeout ℓ̂(a); emitted receipts ingested into Estore .
(59)
5. Failed: Threw an unhandled software exception or network connection failure.
where:
6. TimedOut: Wall-clock elapsed time exceeded ℓ̂(a) without completion; worker is sent an abort signal.
• q is the active action proposal, • s is the modeled environment state (with version vector νs ),
7. CancelRequested: Cancellation signal dispatched due to plan replacement or affirmative refutation.
• ρ = ρ(q, s) is current evaluated operational risk,
8. CancelConfirmed: Remote worker confirmed thread termination and resource cleanup.
• Ω = FΠ (ρ, q, s) is the active mandatory obligation set,
9. Superseded: The active plan generation advanced (g ′ > g) before or during execution; the operation’s witness role in Wq is revoked, but its physical state sideeffects are preserved.
• g ∈ N is the monotonically increasing plan generation tag, • π = ⟨Vπ , Eπ , σπ , Mπ ⟩ is the active plan DAG stamped with generation g,
10. Reconciled: Terminal accounting complete; any genuine unspent reservations returned to Brem .
• Brem , Bcommit , Bresv partition total resource budgets, • Jrun is the set of currently executing worker jobs ⟨a, ga , tlaunch , ℓ̂(a)⟩,
Handling Seven Asynchronous Runtime Scenarios. The controller state machine resolves race conditions via strict semantic rules:
• Vdone is the set of terminated operations,
1. Diagnostic Completing Post-Supersession: If an operation launched in generation g completes when the active generation is g ′ > g, its receipts are not automatically assigned to the new manifest Wq . However, any physical telemetry or state mutation in its payload is incorporated into environment state s.
• Estore is the pool of verified evidence receipts, • Wq is the candidate witness manifest, • tdispatch is the prospective gateway dispatch target timestamp, • Tdead is the proposal hard wall-clock deadline. 7.3
2. Multi-Receipt Operations: An operation producing multiple receipts emits them all into Estore , but financial cost c(a) is charged strictly once upon launch into Bcommit .
Ten-State Operation Lifecycle Across Plan Generations
Every scheduled operation a ∈ A transitions through an explicit 10-state lifecycle:
3. Cancellation Racing with Completion: If completion arrives before cancellation confirmation, the operation is marked Completed and receipts are ingested. If cancellation confirms first, the operation enters CancelConfirmed, receipts are discarded, and unspent reservations are refunded.
Reserved −→ Ready −→ Running −→ {Completed, Failed, TimedOut} −→ {CancelReq → CancelConf} −→ {Superseded, Reconciled}
4. Timed-Out Operations Continuing Remotely: An operation marked TimedOut cannot resurrect its witness role if late output arrives; its results are treated as discardable.
(60) 1. Reserved: Budget is set aside (Brem → Bresv ); operational prerequisites are executing.
5. Non-Rollback Mutations: If a consequential diagnostic mutates external state and subsequent admission fails, the state change is retained in s, and compensation actions are scheduled via TCT.
2. Ready: Prerequisites in Dop have terminated; awaiting scheduled start time σπ (a).
18
6. Earlier-Generation Evidence: Receipts acquired in earlier generations remain in Estore and are eligible for reuse if they satisfy version match G(e) = s|G(e) and freshness against the repaired dispatch target.
Obligation Compiler
Parsed Ω
Parse Ω(q, s) & EFD requirements
Plan Synthesizer Joint EFD & Temporal Solver Plan π ∗
Execution Dispatcher Async worker pool & timeouts
Operation Catalogue
7. New Obligations at Minting Boundary: Handled via atomic Compare-And-Swap (CAS) on state version νs ; if state changed while minting, the certificate is discarded and replanning is re-entered.
Receipts
Signatures, latencies, X (a)
Replanning Monitor Valid E
Risk tracking & dynamic repair
Admission Mint Interface Freshness check & manifest Wq
7.4
Atomic Incremental Plan Repair Transaction
Figure 5: The AAS reference scheduler. The synthesizer selects and times evidence operations, the dispatcher handles execution and consequential sub-admission, and the monitor triggers repair after modeled state changes. Optimality requires the exact-search conditions of Theorem 3.
Algorithm 2 formalizes how state Σ transitions upon an asynchronous event without corrupting plan generation invariants or masking real-world state mutations. To maintain physical and algorithmic integrity, AAS strictly distinguishes:
Algorithm 2 specifies a validation guard before generation advancement. The current prototype cancels running jobs and reconciles reservations before solving the replacement problem; a failed repair can therefore leave the prior execution canceled. It enforces budget conservation but does not implement full transactional rollback of external jobs. The prototype removes receipts with invalid versions or insufficient remaining lifetime, represents potentially reusable receipts as zero-cost observation proxies, and checks their original observation timestamps against the proposed dispatch. The joint solver checks diversity with any new witnesses. In the matched 20-trial selected-operation timeout study, receiptaware repair and full resynthesis each admit 18 cases, while the static control admits none; reuse lowers mean committed cost (Section 9.6).
1. Irreversible Physical Effects: Actual mutations in external systems, hardware state, or non-refundable financial/token expenditure. These effects are authoritatively reflected in Σ.s and Σ.Bcommit and are never rolled back merely because replacement plan synthesis fails. 2. Authoritative Environment State (Σ.s): The true, known state of the physical world. 3. Tentative Repair State: Shadow evaluations of risk ρcand and active obligations Ωlive . 4. Candidate Schedule (∆π, t′dispatch ): The prospective replacement sub-plan. cand cand 5. Candidate Reservations (Bresv , Brem ): Tentative resource ledger allocations.
8
Plan repair executes as a structured PREPARE–VALIDATE– COMMIT transaction:
Reference Scheduler Architecture and Algorithms
The AAS reference scheduler separates plan synthesis, evidence execution, admission, and repair into four components.
Semantic Receipt Reuse and Atomicity Guarantees. AAS permits reusing previously acquired receipts in Estore across plan repair if and only if three conditions hold simultaneously:
8.1
Component Architecture
The AAS architecture comprises six decoupled subsystems (Figure 5):
1. Repaired Dispatch Freshness: The receipt’s expiration bound extends beyond the prospective repaired dispatch and execution window (t′dispatch + δexec ≤ tobs (e) + ∆teff (e) − ϵskew ), rather than merely the current timestamp tnow .
1. Obligation Compiler: Ingests Ω(q, s) from the CAC policy resolver, extracts predicate requirements, epistemic diversity thresholds κmin E (ω), and temporal lifespans ∆tω .
2. State Invariance: The underlying state versions guarded by the receipt (G(e)) match live state: G(e) = Σ.s|G(e) .
2. Operation Catalogue & Exposure Index: Indexes registered operations A by covered claims, conservative latencies ℓ̂(a), costs c(a), token consumption tok(a), and exposure sets X (a) ⊆ F.
3. Epistemic Independence: The receipt’s exposure set X (e) satisfies the EFD diversity cuts required by current live obligations Σ.Ω.
3. Plan Synthesizer: Implements the joint optimization engine. It selects an admissible subset of operations
19
Vπ ⊆ A via ILP (Section 5.3) or progress-based greedy fallback (Section 5.5) and synthesizes execution start times σπ via Backward JIT scheduling (Algorithm 1).
These measured times are small relative to simulated operation latencies. The ordinary size sweep contains no refinement cuts; a separate 20-case constructed suite exercises the supported cut certificates but does not bound worst-case online planning time.
4. Execution Dispatcher: Manages an asynchronous worker pool enforcing strict per-operation timeouts ℓ̂(a). Crucially, any consequential diagnostic operation is intercepted and subjected to recursive CAC admission before dispatch.
9
We evaluate the AAS reference implementation with generated infrastructure workloads and small constructed counterexamples. The primary comparison applies six policies in two evaluation modes to the same 1,200 instances, yielding 14,400 policy-mode records. A policy-mode record is not an independent deployment. Targeted paired studies test freshness, fault-domain diversity, repair, and decomposition cuts.
5. Replanning Monitor: Listens to incoming receipts, detects whether new observations alter world state s, recalculates risk ρ(q, s), and triggers incremental plan repair (Algorithm 2) upon risk escalation, timeout, or negative evidence. 6. Admission Mint Interface: Verifies composite witness manifests Wq = {(ω, Wω )} and forwards them to the authoritative CAC engine for formal discharge evaluation and certificate minting. 8.2
9.1
Workloads and Protocol
The generator creates 400 instances each for PostgreSQL standby promotion, Kubernetes node remediation, and cloud IAM/network reconfiguration (seeds 1000–2199). They contain 4–12 obligations, operation costs and precedence edges, evidence lifetimes of 3–30 s, and an exposure map with 24 modeled fault domains. Actual operation latency is sampled from a log-normal distribution centered on nominal latency (σ = 0.35); this is a simulator assumption, not a measured cloud model. Domain faults are injected into 15% of instances. The selected operation catalogue and gateway policy are held fixed across the main policy comparisons. The six primary policies are serial forward acquisition (B1), cheapest-witness greedy selection (B2), constraintaware parallel forward scheduling (B3/B5), full AAS (B4), and constraint-aware selection followed by scheduling without decomposition refinement (B6). B3 and B5 share an implementation and are shown separately only to preserve the original policy nomenclature. B2 is deliberately simple and is not an implementation of prior portfolio methods such as VP-CONTROL [3]. A bounded exact solver (B7) is used only for the oracle study; full resynthesis (B8) is used in the repair study. In Mode A, the admission gateway scores a candidate manifest retrospectively. In Mode B, it enforces the admission boundary and blocks invalid candidates. We distinguish valid admission, gateway rejection, proven safe refusal, and planning indeterminacy. A recorded invalid candidate in Mode A is a simulated proposal, not an unauthorized physical action. Each main-table outcome count uses the full 1,200-instance denominator. Table latency and cost means are conditional on valid admission; rejected attempts and safe refusals are excluded from those means.
Complete Scheduling Loop
Algorithm 3 formalizes the complete end-to-end scheduling and execution loop operating on authoritative state Σ. 8.3
Empirical Evaluation
Computational Complexity and Scalability Profile
While arbitrary epistemic cut minimization is NP-hard (Theorem 4), our generated instances have at most 16 obligations and 48 operations. On the reference benchmark platform (Apple Silicon, 12-core ARM64, 36 GB RAM, macOS/Darwin, Python 3.13, HiGHS branch-and-cut solver): • In the corrected feasible scaling sweep, end-to-end solver time averages 0.58 ms at four operations and 10.66 ms at 48 operations; neither value isolates Master ILP time. • The greedy fallback (Equation (51)) enumerates fault coalitions up to quorum size for its provisional score. It remains polynomial for fixed small quorums but provides no feasibility certificate when it stops without a plan. • Two-tier Backward JIT scheduling is measured as part of the end-to-end solver time above; the sweep does not separately estimate its latency under bounded concurrency. • In the corrected 20-trial selected-operation timeout study, all 20 cases trigger repair. Receipt-aware repair and full resynthesis each admit 18; local-process repair computation averages 2.05 and 2.32 ms, respectively, in the rerun (Section 9.6).
20
Scheduler Policy
Valid Dispatch
Stale Failures
Correlated Failures
Safe Refusal
Admitted Latency (s)
Admitted Cost ($)
Replan (ms)
Serial Forward (ASAP)
29.75% (357/1200) 28.17% (338/1200) 53.92% (647/1200) 89.58% (1075/1200) 53.92% (647/1200) 89.58% (1075/1200)
0.0% (0/1200) 1.58% (19/1200) 36.67% (440/1200) 1.0% (12/1200) 36.67% (440/1200) 1.0% (12/1200)
61.5% (738/1200) 61.5% (738/1200) 0.0% (0/1200) 0.0% (0/1200) 0.0% (0/1200) 0.0% (0/1200)
8.75% (105/1200) 8.75% (105/1200) 9.42% (113/1200) 9.42% (113/1200) 9.42% (113/1200) 9.42% (113/1200)
7.70 (p95: 7.70) 2.40 (p95: 2.40) 4.18 (p95: 6.51) 5.50 (p95: 12.40) 4.18 (p95: 6.51) 5.50 (p95: 12.40)
$0.11
—
$0.11
—
$0.14
—
$0.15
—
$0.14
—
$0.15
—
Greedy Cost Portfolio Static Parallel AAS (Proposed) Constraint-Aware Forward Separate Sched (No Refinement)
Table 1: Mode A on 1,200 generated instances per policy. Outcome counts use all instances; latency and cost means condition on valid admission. The gateway scores candidate manifests retrospectively. Scheduler Policy
Valid Admitted
Stale Refused
Correlated Blocked
Explicit Safe Refusal
Admitted Latency (s)
Admitted Cost ($)
Serial Forward (ASAP)
29.75% (357/1200) 28.17% (338/1200) 53.92% (647/1200) 89.83% (1078/1200) 53.92% (647/1200) 89.58% (1075/1200)
0.0% (0/1200) 1.58% (19/1200) 36.67% (440/1200) 0.75% (9/1200) 36.67% (440/1200) 1.0% (12/1200)
61.5% (738/1200) 61.5% (738/1200) 0.0% (0/1200) 0.0% (0/1200) 0.0% (0/1200) 0.0% (0/1200)
8.75% (105/1200) 8.75% (105/1200) 9.42% (113/1200) 9.42% (113/1200) 9.42% (113/1200) 9.42% (113/1200)
7.70
$0.11
2.40
$0.11
4.18
$0.14
5.50
$0.15
4.18
$0.14
5.50
$0.15
Greedy Cost Portfolio Static Parallel AAS (Proposed) Constraint-Aware Forward Separate Sched (No Refinement)
Table 2: Mode B on 1,200 generated instances per policy. The gateway blocks invalid candidates before physical proposal execution. Latency and cost means condition on valid admission.
9.2
Main Comparison
100
Valid admission (%)
In Mode A, AAS produces 1,075/1,200 valid candidates (89.58%), 12 stale candidates (1.00%), and 113 proven safe refusals (9.42%). Constraint-aware forward scheduling produces 647 valid candidates (53.92%), 440 stale candidates (36.67%), and the same 113 refusals. Thus, on these paired generated instances, backward placement changes 428 outcomes from stale candidate to valid admission. B6 matches B4 on this workload because no refinement cut is generated by its ordinary instances; this comparison alone does not establish a decomposition benefit. Greedy cost selection and serial forward acquisition each produce 738/1,200 correlated-failure classifications (61.50%) under the declared exposure map. No B4 candidate is classified as structurally correlated. In Mode B the gateway admits 1,078 AAS candidates, blocks nine stale candidates, and records 113 safe refusals. Three of the 12 Mode A stale cases are recovered by the controller in Mode B; no physical proposal executes on a blocked candidate. The gateway blocks 738 serial-forward and 757 greedy-cost candidate dis-
80 60 40 20 0
0.6
0.8
1.0
Constraint-aware forward AAS 1.2 1.4
Evidence lifetime scale
Figure 6: RQ1: Valid admission under matched evidencelifetime scales. Each point uses the same 30 PostgreSQL base instances and operation-keyed latency draws for both policies and all three scales. patches. Mean wasted committed cost over all 1,200 proposals is $0.013 for B4 and $0.106 for B2. These are simulator outcomes under the modeled faults and budgets.
21
80 60 40 20 0
1
2
Required diversity κE
3
0.30
0.14 0.12 0.10 0.08 0.06 0.04 0.02 0.00
1
2
Required diversity κE
3
2.0
Mean committed cost ($)
infeasible for 2-of-q
Mean repair computation (ms)
Greedy cost AAS
Mean attempted cost ($)
Valid admission (%)
100
1.5 1.0 0.5 0.0
Receipt reuse
Full resynthesis
0.25 0.20 0.15 0.10 0.05 0.00
Receipt reuse
Full resynthesis
Figure 7: RQ2: Valid admission and unconditional attempted cost on 30 matched base instances under fixed 2-of-q quorums. Threshold 3 is structurally infeasible because κE ≤ 2; its zero attempted cost reflects refusal, not a cost improvement.
Figure 8: RQ4: Matched mean repair computation and committed cost on 20 selected-operation timeout trials. Receipt reuse and resynthesis each admit 18; the static control admits none. Computation times are local-process measurements.
9.3
9.5
RQ1: Paired Freshness Sensitivity
On 20 bounded instances (|Ω| ≤ 4, |A| ≤ 10), AAS and the exact oracle both find feasible plans at the same cost. Mean local solve times in the corrected rerun are 2.15 and 5.44 ms, respectively; this small paired sample does not establish a general speed advantage. The revised solver uses exhaustive temporal-order fallback for portfolios of at most six operations, and the oracle shares that temporal search component. The comparison checks selection and cost on small cases, not independent temporal correctness or general completeness.
We vary only evidence lifetimes (0.6×, 1.0×, 1.5×) on 30 PostgreSQL base instances (seeds 7000–7029). Each operation receives a fixed latency draw keyed by base seed and operation identifier, so the same trace is reused across policies and scales. At 0.6×, AAS admits 14/30 while constraintaware forward scheduling admits 0/30; the other 16 AAS cases are proven infeasible and refused. At nominal lifetime, the counts are 30/30 versus 0/30; at 1.5×, they are 30/30 versus 23/30. The paired admission difference at 1.5× is 7/30 (23.3 percentage points; percentile bootstrap 95% interval 10.0–40.0 points over base instances). The gap narrows as evidence remains valid longer. The separate Kmax = 1 fixture verifies that a two-operation serial schedule is feasible, but does not distinguish policies. 9.4
RQ3: Bounded Joint Optimality
9.6
RQ4: Repair After a Selected-Operation Timeout
The corrected intervention faults an operation selected by the same initial plan in every arm (20 trials, seeds 5000–5019). It compares incremental repair with receipt reuse, the same controller with reuse disabled, full resynthesis, and a static no-repair control. All 20 cases trigger repair in the three enabled arms. Reuse, no-reuse, and resynthesis each admit 18/20; static planning admits 0/20. The two failures in each repair arm occur on different instances, so equal totals do not imply identical recovery. Receipt reuse records 2.85 reused receipts per case and mean committed cost $0.223 versus $0.296 for either no-reuse or resynthesis. The paired cost difference (reuse minus no-reuse) is −$0.073 with a percentile bootstrap 95% interval of approximately [−$0.100, −$0.047] over 20 instances. Mean local repair computation in the corrected rerun is 2.05 versus 2.21 ms for no-reuse and 2.32 ms for resynthesis; these small timing differences are process dependent and do not establish a deployment latency advantage. This study injects operation timeouts, not environmental version changes.
RQ2: Diversity and Cost
We vary required EFD threshold κmin ∈ {1, 2, 3} on the same E 30 base instances (ten per scenario; seeds 8000–8029), fixing 2-of-q quorum rules, operation-keyed latency, and injected domain faults. AAS admits 23 and 25 instances at thresholds 1 and 2; the greedy cost baseline admits 18 and 10. The different admission counts reflect both diversity and realized faults, so the threshold-2 arm is not a monotone availability claim. At threshold 3, all 30 AAS instances are proven infeasible because a completed local fault basis implies κE ≤ kω = 2 for the varied obligations. Greedy cost selection produces no valid admission either. The zero attempted cost of AAS in this arm records safe refusal. Cost comparisons among admitted proposals must therefore use the feasible threshold-1 and threshold-2 arms; unconditional cost is $0.139 and $0.151 per instance, respectively. For the declared exposure map and positive authorization rule, κE (W, Γω ) ≥ h means that fewer than h modeled roots cannot expose a decisive approving coalition. This is a conditional structural guarantee; unmodeled shared dependencies or an incorrect causal account of exposed approvals can defeat it.
9.7
RQ5: Consequential Diagnostics
Twelve deterministic fixtures test prospective recursive admission: ten finite stratified trees are admitted, while a cycle and a non-descending-risk tree are rejected. These fixtures check specific invariants; they do not estimate distributed liveness or resource-leak rates.
22
Solver Wallclock Time (ms)
12 10
AAS Decomposition Solver Scaling with Problem Size
9.9
Mean Solve Time p95 Solve Time
On 30 shared generated instances, full AAS admits 28/30. Greedy selection without EFD constraints admits 10/30 and produces 20 correlated-failure classifications. Forward scheduling admits 19/30 with 11 stale outcomes. The nominal “No Adaptive Repair” general ablation shares the forward policy implementation and therefore cannot isolate repair; the dedicated timeout study above supplies that intervention. Noreuse and no-refinement each admit 28/30, matching full AAS because the general workload activates neither mechanism. The paired repair and cut-producing studies identify their effects under controlled activation. These are mechanism tests on synthetic data, not estimates of production reliability.
8 6 4 2 10
20
30
Number of Operations in Problem (||)
40
50
Figure 9: RQ6: Solver time on seven generated sizes (4–48 operations). This ordinary scaling sweep generates no refinement cuts; the separate constructed suite below exercises both supported cut certificates.
10
93.3%
G: FULL_AAS
33.3%
E: SEPARATE: SCHED: NO_REFINEMENT
93.3%
D: NO_RECEIPT_REUSE
93.3% 63.3%
C: NO_ADAPTIVE: REPAIR
63.3%
B: NO_JIT_SCHEDULING
33.3%
A: NO_EFD: SELECTION 0
20
40
60
Valid Admission Rate (%)
80
100
Figure 10: General ablation outcomes on 30 generated instances per policy. No-reuse and no-refinement coincide with full AAS here because these trials do not trigger repair or refinement. 9.8
Discussion and Limitations
Scope of Empirical Evidence. The three main scenario families still use generated operations, costs, exposure maps, latencies, and faults. Policy and mode records share instances. The new sensitivity studies pair base instances, fault injections, and operation-keyed latency draws, but retain the same generator and small sample sizes. The 20-instance oracle comparison shares a bounded temporal-search component; the 20 cut-producing cases are constructed to activate the supported certificates. The corrected timeout study demonstrates recovery under selected-operation faults, but does not test production state shifts, distributed cancellation, or transactional rollback. Independent workloads and live integrations are required to assess transfer and worst-case solve behavior.
Ablation Study: Contribution of AAS Components F: GREEDY_FORWARD
Ablations and Interpretation
Clock Synchronization and Distributed Skew. Theorem 1 defines evidence validity evaluated at the execution gateway clock Cgw , deducting maximum gateway-observer skew ϵskew (|Ci (t) − Cgw (t)| ≤ ϵskew ). In distributed architectures lacking hardware-synchronized clocks (such as GPS/atomic reference clocks in TrueTime [10]), relative clock drift between two independent observers i and j can reach 2ϵskew . If peer observers compare timestamps directly without mediation through an authoritative gateway, soundness requires deducting 2ϵskew :
RQ6: Solver Scaling and Certified Refinement
On seven feasible generated sizes, each with 2-of-q obligations and separate witness roots, mean solver time rises from 0.58 ms at four operations to 10.66 ms at 48 operations (p95 11.63 ms at the largest size). Every fixture admits a plan; this assertion prevents timing structural refusals. The sweep supports neither an asymptotic claim nor a bound for repeated refinement, and generates zero cuts. We therefore add 20 constructed, seeded small cases: ten violate a witness’s intrinsic lifetime, and ten contain a cheap precedence chain that misses the deadline. In every case the unrefined master selects a temporally infeasible portfolio; one certified cut leads the decomposed solver to a feasible alternative in the second iteration. Both cut types occur ten times, and the refined cost matches the exact oracle in all 20. These cut-producing cases demonstrate the implemented mechanism, not its frequency in deployed workloads.
∆tpeer effective (e) = max (0, ∆t(e) − 2ϵskew ) .
(61)
If clock drift exceeds evidence validity, short-lived telemetry cannot be safely scheduled across disparate clock domains without atomic local re-observation at the gateway. Proactive Pre-fetching vs. Invalidation Risk. Prefetching long-lived evidence (e.g., reading cluster topology 30 s prior to failover) amortizes scheduling latency. However, if concurrent background mutations modify the underlying resource versions, the pre-fetched witness becomes obsolete. The CAC admission gateway enforces state version guards
23
Ablation Variant
Valid (%)
Stale (%)
Corr (%)
Refusal (%)
Lat (s)
Cost ($)
A: no EFD selection
33.33% (10/30) 63.33% (19/30) 63.33% (19/30) 93.33% (28/30) 93.33% (28/30) 33.33% (10/30) 93.33% (28/30)
0.0% (0/30)
66.67% (20/30) 0.0% (0/30)
0.0% (0/30)
2.40
$0.11
0.0% (0/30)
4.19
$0.14
B: no JIT scheduling C: no adaptive repair D: no receipt reuse E: no refinement F: greedy forward G: full AAS
36.67% (11/30) 36.67% (11/30) 6.67% (2/30)
0.0% (0/30)
0.0% (0/30)
4.19
$0.14
0.0% (0/30)
0.0% (0/30)
5.15
$0.15
6.67% (2/30)
0.0% (0/30)
0.0% (0/30)
5.15
$0.15
0.0% (0/30)
66.67% (20/30) 0.0% (0/30)
0.0% (0/30)
7.70
$0.11
0.0% (0/30)
5.15
$0.15
6.67% (2/30)
Table 3: General ablation study on the same 30 generated instances per policy. Latency and cost means condition on valid admission. Gq = {νs = νlive }. If any guarded version changes between pre-fetching and dispatch, the certificate CAS fails, forcing an abort. Thus, aggressive pre-fetching in high-concurrency environments increases the probability of optimistic concurrency aborts.
Verification Portfolios and Model Routing. FrugalGPT [8] and RouteLLM [13] trade inference cost against model capability. VP-CONTROL [3] studies cost-aware verifier portfolios, common-mode evidence failures, and committime guards, including a live HTTP/SQLite study. Its portfolio problem motivates source-aware selection. Our formulation additionally schedules observations with finite validity intervals and treats consequential evidence acquisition as a recursively admitted operation. The evaluations address different workloads and should not be read as a direct performance comparison.
Incomplete Epistemic Dependency Maps. The structural diversity guarantees of Section 5 depend on the fidelity of the exposure map X : A → 2F . If two ostensibly independent services share an undisclosed transitive dependency—such as a common DNS resolver, power bus, or base model—the calculated cut κE (W, Γω ) can overstate diversity. Establishing complete epistemic independence remains an empirical challenge.
Real-Time and Dependency Scheduling. Real-time scheduling [14, 15] and resource-constrained project scheduling [16] address deadlines, precedence, and capacity. Assurance scheduling adds a policy-defined validity interval to each selected witness. A feasible task schedule can therefore yield an inadmissible dispatch if evidence expires before the protected execution window ends.
Human-in-the-Loop Latency Asymmetry. Human approval can dominate automated evidence-acquisition latency. The current simulator does not model an asynchronous human response or re-fire short-lived telemetry after approval. Such a workflow would need an explicit provisional state, a new dispatch-time freshness check, and another admission decision.
11
Fault Tolerance and Epistemic Diversity. N-Version Programming [17] and Byzantine fault-tolerant replication [18] use redundancy against specified failures. EFD theory [7] defines a structural cut relative to the authorization rule and an explicit fault basis. AAS imports that cut into witness selection and admission, then adds temporal freshness and budget constraints. Its guarantee remains relative to the declared exposure map; an undisclosed common dependency can invalidate it.
Related Work
Admission Control and Mediated Agent Execution. Access-control models such as ABAC [11] decide whether a principal may invoke an operation. Proof-Carrying Code [12] made consumer-side proof checks explicit. Recent agent-tool work, including ToolGuardian [2], characterizes tool behavior and applies task-aware runtime authorization. CAC [1] specifies risk-conditioned assurance obligations. AAS addresses the intervening planning problem: which observations to obtain and when to obtain them before mediated execution.
12
Conclusion
AAS formulates evidence acquisition for consequential agent actions as a joint selection and scheduling problem. Its witness assignment enforces declared fault-domain cuts; its tem24
poral scheduler places expiring observations near dispatch; and its controller admits consequential diagnostics and repairs plans after state changes. The formal guarantees depend on modeled dependencies, bounded latencies, and exact search where optimality is claimed. On three generated workload families, AAS raises valid candidate admission from 647/1,200 for constraint-aware forward scheduling to 1,075/1,200 and reduces stale candidates from 440 to 12. Paired sensitivity studies hold the base instance and latency draws fixed while varying freshness and diversity. In 20 constructed cut-producing cases, certified refinement recovers an oracle-matching feasible alternative; in 20 selected-operation timeout trials, receipt-aware repair admits 18 and lowers committed cost relative to resynthesis. The bounded oracle shares temporal search with the solver, and neither constructed cuts nor simulator timeouts establish production reliability. Independent workloads and live gateway integrations remain the next tests. AI-Use Disclosure. OpenAI Codex and Google Antigravity assisted with draft structuring, language and notation editing, implementation debugging, experiment auditing, figure preparation, and reference formatting. The authors are responsible for verifying the code, proofs, sources, and reported results.
[7] Jun He and Deying Yu. The illusion of independent quorums: Epistemic fault domains and correlated cognitive failures in agentic quorums. arXiv preprint arXiv:2609.02925, 2026. [8] Lingjiao Chen, Matei Zaharia, and James Zou. FrugalGPT: How to use large language models while reducing cost and improving performance. arXiv preprint arXiv:2305.05176, 2023. [9] Richard M. Karp. Reducibility among combinatorial problems. In Raymond E. Miller and James W. Thatcher, editors, Complexity of Computer Computations, pages 85–103. Plenum Press, 1972. [10] James C. Corbett, Jeffrey Dean, Michael Epstein, Andrew Fikes, Christopher Frost, J. J. Furman, Sanjay Ghemawat, Andrey Gubarev, Christopher Heiser, Peter Hochschild, Wilson Hsieh, Sebastian Kanthak, Eugene Kogan, Hongyi Li, Alexander Lloyd, Sergey Melnik, David Mwaura, David Nagle, Sean Quinlan, Rajesh Rao, Lindsay Rolig, Yasushi Saito, Michal Szymaniak, Christopher Taylor, Ruth Wang, and Dale Woodford. Spanner: Google’s globally distributed database. ACM Transactions on Computer Systems, 31(3):8:1– 8:22, 2013.
References
[11] Vincent C. Hu, David Ferraiolo, Rick Kuhn, Adam Schnitzer, Kenneth Sandlin, Robert Miller, and Karen Scarfone. Guide to attribute based access control (ABAC) definition and considerations. Technical Report SP 800-162, National Institute of Standards and Technology, 2014.
[1] Jun He and Deying Yu. Cognitive admission control: Risk-conditioned assurance for consequential actions in agentic distributed systems. arXiv preprint arXiv:2609.16313, 2026. [2] Arun Ravindran and Saurabh Deochake. ToolGuardian: Declarative security for AI agent-tool interactions. arXiv preprint arXiv:2607.21835, 2026.
[12] George C. Necula. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 106–119, 1997.
[3] Zihao Zheng, Baichuan Li, Junyi Yao, and Jiayu Long. Engineering reliable commit gates for agentic ai: Costaware verification portfolios under common-mode data failures. arXiv preprint arXiv:2609.10969, 2026.
[13] Isaac Ong, Amjad Almahairi, Vincent Wu, Wei-Lin Chiang, Tianhao Wu, Joseph E. Gonzalez, M Waleed Kadous, and Ion Stoica. RouteLLM: Learning to route LLMs with preference data. arXiv preprint arXiv:2406.18665, 2024.
[4] Charlie Snell, Jaehoon Lee, Kelvin Xu, and Aviral Kumar. Scaling LLM test-time compute optimally can be more effective than scaling model parameters. arXiv preprint arXiv:2408.03314, 2024.
[14] Chung Laung Liu and James W. Layland. Scheduling algorithms for multiprogramming in a hard-real-time environment. Journal of the ACM, 20(1):46–61, 1973.
[5] Noah Shinn, Federico Cassano, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao. Reflexion: Language agents with verbal reinforcement learning. Advances in Neural Information Processing Systems, 36:8634–8652, 2023.
[15] Giorgio C. Buttazzo. Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications. Springer Science & Business Media, 3rd edition, 2011.
[6] Jeffrey Dean and Luiz André Barroso. The tail at scale. Communications of the ACM, 56(2):74–80, 2013.
[16] Ronald L. Graham, Eugene L. Lawler, Jan Karel Lenstra, and Alexander H. G. Rinnooy Kan. Optimization and approximation in deterministic sequencing and scheduling:
25
a survey. Annals of Discrete Mathematics, 5:287–326, 1979.
Simultaneously, the completion of the protected execution window cannot exceed the gateway-evaluated expiration timestamp of any witness receipt:
[17] Algirdas Avižienis. The N-version approach to faulttolerant software. IEEE Transactions on Software Engineering, SE-11(12):1491–1501, 1985.
tdispatch + δexec ≤ min (tobs (e) + ∆teff (e) − ϵskew ) . e∈Wall
(64) Combining (63) and (64), an admissible dispatch timestamp tdispatch exists if and only if the feasible dispatch interval [tlower , tupper ] is non-empty, where:
[18] Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys, 22(4):299–319, 1990.
A
tlower = max Cπ (a) + δready ,
Formal Proofs
a∈Vreq
(65)
tupper = min (tobs (e) + ∆teff (e) − ϵskew ) − δexec . (66) e∈Wall
This appendix provides complete formal proofs for the theoretical statements established in the main manuscript. A.1
The interval [tlower , tupper ] is non-empty if and only if tlower ≤ tupper : max Cπ (a) + δready ≤ min tobs (e) a∈Vreq e∈Wall (67) + ∆teff (e) − ϵskew − δexec .
Proof of Theorem 1 (Dispatch Freshness Intersection)
Theorem 6 (Restatement of Theorem 1). Fix an executed assurance plan π with completed operations Vπ , actual completions {Cπ (a)}, observation timestamps {tobs (e)}, and composite witness manifest Wall . Let Vreq ⊆ Vπ denote mandatory operations prior to dispatch (Vmanifest ∪ AncDop (Vmanifest )), and δready = δverify + δmint + δdisp . A dispatch timestamp satisfying readiness and freshness throughout the protected execution window exists, before imposing the independent deadline and budget guards, if and only if condition (26) holds:
Moving constants δready , δexec , and ϵskew directly establishes Equation (62). To establish equivalence with pairwise condition (27): • ( =⇒ ) Suppose condition (62) holds. For any operation a ∈ Vreq and any witness ei ∈ Wall , we have Cπ (a) ≤ maxu∈Vreq Cπ (u) and mine∈Wall (tobs (e)+∆teff (e)) ≤ tobs (ei ) + ∆teff (ei ). Substituting these bounds gives Cπ (a) + δready + δexec + ϵskew ≤ tobs (ei ) + ∆teff (ei ), yielding Cπ (a) − tobs (ei ) ≤ ∆teff (ei ) − δready − δexec − ϵskew . For a ∈ Vmanifest , substituting Cπ (a) = tobs (ej ) + ℓpost (a) gives Equation (28).
max Cπ (a) + δready + δexec + ϵskew
a∈Vreq
≤ min (tobs (e) + ∆teff (e)) .
(62)
e∈Wall
which is equivalent to pairwise operational skew bound (27) and observation skew bound (28). Non-witness prerequisites u ∈ Vreq \ Vmanifest participate directly in readiness bound (27).
• ( ⇐= ) Conversely, suppose (27) holds for all operations a ∈ Vreq and witnesses ei ∈ Wall . Choosing a∗ = arg maxa∈Vreq Cπ (a) and e∗i = arg mine∈Wall (tobs (e)+∆teff (e)) directly recovers condition (62).
Proof. By Definition 6 and Equation (25), dispatch requires that for every witness receipt e ∈ Wall , the entire protected execution window [tdispatch , tdispatch + δexec ] is contained within the conservative gateway-evaluated validity interval I(e) = [tobs (e) − ϵskew , tobs (e) + ∆teff (e) − ϵskew ]. Furthermore, proposal dispatch cannot legally occur until all mandatory operations in Vreq (both witness producers and precedence prerequisites) have completed execution, receipts have been emitted and verified (δverify ), the admission certificate has been minted by CAC (δmint ), and gateway mediation delay (δdisp ) has elapsed: tdispatch ≥ max Cπ (a) + δready , a∈Vreq
This completes the proof. A.2
Proof of Theorem 4 (NP-Hardness of ASP-DEC)
Theorem 7 (Restatement of Theorem 4). The decision version of the Assurance Scheduling Problem (ASP-DEC) is NP-hard, even when operational precedence is empty (Dop = ∅) and operation latencies are uniform. Proof. We establish NP-hardness by constructing a polynomial-time reduction from the classical NP-complete problem M INIMUM W EIGHT S ET C OVER (WSC) [9] to ASP-DEC.
(63)
where δready = δverify + δmint + δdisp .
26
– Witness mapping: For each ωi ∈ Ω, since S ′ covers U, there exists at least one Sj ∈ S ′ such that ui ∈ Sj . Choose one such aj ∈ Vπ and set Mπ (ωi ) = {aj }.
The WSC Decision Problem. An instance of M INIMUM W EIGHT S ET C OVER is defined by a 4-tuple ⟨U, S, w, K⟩: a finite universe U = {u1 , . . . , un }, a S collection of subsets m S = {S1 , . . . , Sm } with Sj ⊆ U and j=1 Sj = U, a nonnegative cost function w : S → R≥0 , and a target cost threshold K ∈ R≥0 . The problem asks S whether there exists a sub-collection S ′ ⊆ S such that Sj ∈S ′ Sj = U and P Sj ∈S ′ w(Sj ) ≤ K.
We verify prospective admissibility of π: 1. Precedence: Eπ = ∅, trivially satisfied. 2. Latency & Deadlines: All operations start at 0 and have latency ℓ̂ = 1, so Ĉπ (aj ) = 1. With δdisp = 0, target dispatch is tdispatch = 1. Then tdispatch + δexec = 1 + 1 = 2 ≤ 10 = Tdead , satisfying deadline feasibility. Latency is 1 − 0 = 1 ≤ Blat . P 3. Cost Budget: Cost(π) = aj ∈Vπ c(aj ) = P w(S ) ≤ K = B . Token and risk bud′ j $ Sj ∈S gets are identically zero, satisfying all budget invariants.
Polynomial-Time Construction. Given an arbitrary instance ⟨U, S, w, K⟩ of WSC, we construct an instance of ASP-DEC P = ⟨Ω, A, B, D, T ⟩ with cost bound K as follows: 1. Assurance Obligations Ω: For each ui ∈ U, create obligation ωi = ⟨ϕωi , Eωi , ∆tωi , κmin E (ωi ), Qωi ⟩ with eligible evidence Eωi = {εstd }, freshness lifespan ∆tωi = 10, diversity threshold κmin E (ωi ) = 1, and quorum threshold kωi = 1. Thus |Ω| = |U | = n.
4. Quorum Coverage: For each ωi , (ωi , εstd ) ∈ Cov(aj ) because ui ∈ Sj . The quorum requirement is |Mπ (ωi )| = 1 ≥ kωi = 1.
2. Assurance Operations A: For each subset Sj ∈ S, create an operation aj ∈ A with financial cost c(aj ) = w(Sj ), latencies ℓ(aj ) = ℓ̂(aj ) = 1, cognitive tokens tok(aj ) = 0, risk ρ(aj ) = 0 ≺ τΠ (non-consequential), potential coverage Cov(aj ) = {(ωi , εstd ) | ui ∈ Sj }, lifespan ∆t(aj ) = 10, prerequisites Pre(aj ) = ∅, and distinct epistemic exposure X (aj ) = {fj } for distinct fj ∈ F = {f1 , . . . , fm }. Thus |A| = |S| = m.
5. Freshness: Effective lifespan is ∆teff = min(10, 10) = 10. Then tdispatch + δexec = 2 ≤ σπ (aj ) + ∆teff = 0 + 10 = 10. 6. Epistemic Diversity: Each obligation requires κmin E (ωi ) = 1. The singleton witness {aj } is decisive for its 1-of-1 rule and is exposed by {fj }, so κE (Mπ (ωi ), Γωi ) = 1 ≥ κmin E (ωi ).
3. Dependencies D: Set Dop = ∅ and Depi = {(aj , fj ) | 1 ≤ j ≤ m}.
7. Diagnostics: All operations have risk ρ = 0 ≺ τΠ , so no diagnostic sub-plans are required.
4. Budgets B and Temporal Constraints T : Set B$ = K, Blat = 10, Btok = 0, Brisk = 0, and Kmax = ∞. Set t0 = 0, Tdead = 10, δexec = 1, δverify = δmint = δdisp = 0, and ϵskew = 0.
Thus π |=pros P with Cost(π) ≤ K. • ( ⇐= ) Conversely, suppose there exists a prospectively admissible plan π = ⟨Vπ , Eπ , σπ , Mπ ⟩ for P with Cost(π) ≤ K. Define the sub-collection S ′ = {Sj ∈ S | aj ∈ Vπ }. By the resource budget invariant (11): X X w(Sj ) = c(aj ) = Cost(π) ≤ K.
This construction maps universe elements to obligations and subsets to multi-obligation operations in time O(|U| · |S|), which is polynomial in the input size. Equivalence Proof. We Pnow prove that there exists a valid set cover S ′ ⊆ S with Sj ∈S ′ w(Sj ) ≤ K if and only if there exists a prospectively admissible plan π |=pros P with Cost(π) ≤ K:
Sj ∈S ′
aj ∈Vπ
Now consider any arbitrary universe element ui ∈ U. In the constructed ASP instance, ui corresponds to obligation ωi ∈ Ω. By prospective quorum coverage (Definition 6), π must assign candidate witness operations Mπ (ωi ) ⊆ Vπ satisfying:
• P ( =⇒ ) Suppose S ′ ⊆ S is a valid set cover with Sj ∈S ′ w(Sj ) ≤ K. Construct assurance plan π = ⟨Vπ , Eπ , σπ , Mπ ⟩ as follows:
|Mπ (ωi )| ≥ kωi = 1
– Set of operations: Vπ = {aj ∈ A | Sj ∈ S ′ },
and
∀a ∈ Mπ (ωi ), (ωi , εstd ) ∈ Cov(a).
– Precedence edges: Eπ = ∅,
Thus, there exists at least one operation aj ∈ Vπ such that (ωi , εstd ) ∈ Cov(aj ). By our polynomial construction, (ωi , εstd ) ∈ Cov(aj ) holds if and only if ui ∈ Sj .
– Scheduled start times: σπ (aj ) = 0 for all aj ∈ Vπ ,
27
Since aj ∈ Vπ , the corresponding subset Sj belongs to S ′ . Because this holds for every ui ∈ U, we conclude that: [ Sj = U.
total number of integer assignment configurations is at most 2|A|·(|Ω|+1) , which is strictly finite. At each iteration k where candidate solution (x(k) , y(k) ) is rejected by the Authoritative Temporal Solver: (1) If rejection is caused by an unavoidable directed precedence chain whose critical path exceeds available lead P time (tCP + δready > Tdead − t0 − δexec ), structural cut (47) ( a∈Vchain xa ≤ |Vchain | − 1) is added. This strictly forbids Vchain and all supersets from being generated in future iterations, pruning at least one point in {0, 1}|A| . (2) Otherwise, the failure is caused by freshness expiration or concurrency collision among assigned witnesses. When certified by an exact subproblem evaluation, the solver identifies active (k) conflicting assignment pairs AconflictP = {(a, ω) | ya,ω = 1}, and appends assignment cut (46) ( (a,ω)∈Aconflict ya,ω ≤ |Aconflict | − 1). If heuristic evaluation exhausts without certified proof (N OT combinatorial PF OUND), a safe full-candidate P no-good cut ( a:x(k) =1 (1 − xa ) + a:x(k) =0 xa ≥ 1) is a a appended. Each cut strictly eliminates candidate assignment (x(k) , y(k) ) without pruning unvisited alternatives. Because each iteration strictly eliminates at least one previously unvisited integer assignment point and the total number of integer assignments is finite, the LBBD loop must terminate in a finite number of iterations (at most 2|A|·(|Ω|+1) ).
Sj ∈S ′
Hence, S ′ is a valid set cover of U with total weight at most K. Since M INIMUM W EIGHT S ET C OVER is NP-complete, the decision problem ASP-DEC is NP-hard. Complexity Analysis: Multi-Obligation Coverage vs. EFD Cut Verification. We emphasize that Theorem 4 formally establishes that ASP-DEC is NP-hard due to multi-obligation witness coverage via reduction from Minimum Weight Set Cover. Regarding epistemic diversity: (1) Fixed thresholds: To verify κE (W, Γω ) ≥ h, enumerate each fault coalition C ⊆ F with |C| < h and check whether it exposes fewer than kω assigned witnesses. For fixed h, this costs O(|W | h |F|h−1 ). (2) ILP separation: At h = 2, singletonroot cuts can be instantiated statically. At h = 3, root pairs are also polynomial to enumerate. (3) Decision-rule bound: The completed local-root basis implies κE (W, Γω ) ≤ kω once a quorum exists. Hence a threshold above the quorum cardinality is infeasible before scheduling. The NP-hardness reduction uses h = kω = 1 and is unaffected by this correction. A.3
Part 2: Soundness of Cuts and Global Optimality. To establish global cost optimality upon non-timeout termination: 1. Outer Relaxation Property: The initial Master ILP (37)– (48) without conflict cuts enforces all necessary conditions of prospective admissibility: operational prerequisite closure (xa ≤ xu ), multi-obligation quorum coverage, EFD diversity cuts, and resource budgets. Thus, the feasible region of the Master ILP is an outer relaxation of Πadm (P).
Proof of Theorem 3 (Convergence and Conditional Global Optimality)
Theorem 8 (Restatement of Theorem 3). The decomposed Logic-Based Benders Decomposition (LBBD) algorithm terminates in a finite number of iterations. Furthermore, for any fully modeled or flattened problem instance P, if the master solver executes to completion without timeout (Tctrl = ∞) and the subproblem is evaluated authoritatively, the returned plan π ∗ is globally cost-optimal over all prospectively adP missible plans: Cost(π ∗ ) = minπ∈Πadm (P) a∈Vπ c(a). If the solver reaches computation timeout Tctrl < ∞ and returns the best incumbent integer solution, or falls back to the greedy heuristic (Section 5.5), the resulting plan is approximately optimized and prospectively feasible, with no claim of global optimality. Consequential diagnostic sub-plans admitted dynamically at runtime are coordinated outside this static optimality theorem.
2. Soundness of Pruning: A cut is valid if it prunes no prospectively admissible plan π ∈ Πadm (P). Structural cuts are sound because if a subset of operations Vchain has a topological critical path exceeding Tdead − t0 − δready − δexec , latency monotonicity guarantees that no schedule containing Vchain can complete before the hard deadline under conservative latencies. Assignment cuts are sound when subproblem infeasibility is certified authoritatively by an exact temporal oracle (evaluating all discrete topological serializations and continuous dispatch intervals via STN enumeration). Tier 1 and Tier 2 backward heuristics operate on a discrete grid and provide polynomial-time sound schedule admission, but heuristic exhaustion (N OT F OUND) cannot mathematically prove continuous infeasibility; hence, heuristic failures use safe full-candidate combinatorial cuts to avoid unsound over-pruning.
Proof. We divide the proof into two parts: finite termination and global optimality. Part 1: Finite Termination. Let |A| denote candidate assurance operations and |Ω| denote mandatory obligations. The decision space of the Master ILP is bounded by binary assignments x ∈ {0, 1}|A| , y ∈ {0, 1}|A|×|Ω| . The
3. Optimality of the First Feasible Candidate: The Master ILP minimizes the exact non-decreasing linear objective 28
Operation Class
Example Implementation
Mean Cost
Nominal Latency
Lifespan ∆t
Consequential? (ρ ≥ τΠ )
Primary Epistemic Fault Domains (X )
Passive Telemetry
Prometheus scrape / eBPF
$0.0001
40 ms
5s
No
Log Audit
Loki / OpenSearch query
$0.002
250 ms
30 s
No
Hardware Attestation
$0.005
350 ms
300 s
No
Static SMT Proof
TPM quote / AWS Nitro quote Z3 / Dafny verification
$0.02
1.8 s
∞
No
Redundant Model
Independent LLM judge
$0.03
1.2 s
60 s
No
Consensus Query
Raft / Paxos quorum read
$0.001
80 ms
10 s
No
Filesystem Freeze
LVM / ZFS snapshot probe
$0.01
1.5 s
15 s
Yes
Network Probe
Synthetic BGP / ping burst
$0.005
600 ms
8s
Yes
Failover Dry-Run
Staging replica promotion
$0.25
6.5 s
45 s
Yes
Human Sign-off
Slack / PagerDuty sign-off
$5.00
180 s
600 s
No
Local kernel, metrics daemon Log forwarder, search index Hardware root-of-trust, CA Solver binary, CPU architecture Model weights, inference stack Consensus network quorum Storage controller, I/O bus Network fabric, firewall Database engine, replication stream Human operator, IdP token
Table 4: Taxonomy of heterogeneous assurance operations in AAS, detailing financial expense, observation latency, temporal decay, and operational consequence. P function Z(x) = a∈A c(a)xa . When subproblems are evaluated with exact completeness, cuts prune only provably infeasible points, so the sequence of optimal objective values returned by the Master ILP is monotonically non-decreasing: Z(x(1) ) ≤ Z(x(2) ) ≤ · · · ≤ Z(x∗ ). When candidate x∗ is first verified as temporally feasible, it satisfies all constraints of Πadm (P) and its cost is a valid lower bound on all unvisited feasible candidates. P Hence, Cost(π ∗ ) = minπ∈Πadm (P) a c(a), proving conditional global optimality on the modeled instance P.
treats intent predicate ϕω as fixed. In long-running autonomous workflows, operator intent or business context may drift while evidence is gathered. Formulating formal fidelity metrics connecting physical evidence directly to humanreferential intent remains an active research direction. Multi-Tenant Cross-Sovereignty Scheduling. When orchestrating operations across multiple cloud domains, assurance must navigate heterogeneous trust roots, non-comparable clocks, and data-residency boundaries. Extending AAS to federated epistemic markets is a compelling direction for future architectures.
This completes the proof.
B
Catalogue of Assurance Operations
Table 4 provides a representative taxonomy of assurance operations supported in the AAS reference implementation, categorized across operational risk, latency, cost, and typical validity windows.
C
Open Problems and Roadmap
Negative Knowledge Induction (The Hardknock Bridge). When an assurance plan fails to reach admission—or an admitted action triggers an unexpected incident—the execution trace can reveal omitted epistemic dependencies and correlated failures. A remaining research question is how to use such traces to revise future admission obligations Ω without overfitting to individual incidents. Human-Referential Fidelity and Intent Drift. While AAS models physical state freshness and epistemic diversity, it 29
Algorithm 2 Atomic Adaptive Plan Repair Transaction Require: Runtime state Σ, triggering event E, wall-clock time tnow Ensure: Updated state Σ or A BORT 1: ▷ Phase I: Authoritative Physical State Reconciliation 2: if E carries irreversible physical mutations then 3: Σ.s ← ApplyPhysicalEffects(Σ.s, E) ▷ Authoritative physical state updated 4: end if 5: if E is Affirmative Refutation then 6: CancelAll(Σ.Jrun ); refund unspent Bresv → Brem 7: return A BORT(Predicate Refuted) 8: end if 9: ▷ Phase II: PREPARE (Shadow State & Tentative Ledgers) 10: ρcand ← ρ(Σ.q, Σ.s); Ωlive ← FΠ (ρcand , Σ.q, Σ.s) 11: Let ∆Ω+ ← Ωlive \ Σ.Ω and ∆Ω− ← Σ.Ω \ Ωlive cand cand 12: Vcand ← Σ.Vπ ; Brem ← Σ.Brem ; Bresv ← Σ.Bresv 13: for each unlaunched u ∈ Σ.Vπ witnessing only ∆Ω− do cand cand cand 14: Vcand ← Vcand \ {u}; Brem ← Brem + c(u); Bresv ← cand Bresv − c(u) 15: end for 16: Ereusable ← {e ∈ Σ.Estore | G(e) = Σ.s|G(e) ∧ ¬e.refuted} 17: Determine Ωunresolved ⊆ Ωlive lacking quorums/cuts under Ereusable 18: if Ωunresolved = ∅ then 19: t′disp ← max(tnow , Σ.tdispatch ) 20: if t′disp + δexec ≤ mine∈Ereusable (tobs (e) + ∆teff (e) − ϵskew ) ∧ t′disp + δexec ≤ Σ.Tdead then 21: Σ.ρ ← ρcand ; Σ.Ω ← Ωlive ; Σ.Vπ ← Vcand cand cand ; Σ.Bresv ← Bresv ; Σ.tdispatch ← 22: Σ.Brem ← Brem ′ tdisp ; Σ.g ← Σ.g + 1; return Σ 23: else 24: Mark expired obligations in Ωlive as unresolved → Ωunresolved 25: end if 26: end if 27: ▷ Phase III: SYNTHESIZE & VALIDATE (Transaction Guard) 28: (∆π, t′disp ) ← S YNTH P LAN(Ωunresolved , Bcand , Σ.Tdead ) 29: if ∆π = I NFEASIBLE ∨ t′disp + δexec > Σ.Tdead ∨ Cost(∆π) > Bcand then 30: ▷ ABORT: Retain authoritative physical state Σ.s; cancel unlaunched candidate cand cand 31: CancelAll(Σ.Jrun ); Σ.Brem ← Brem + Bresv ; Σ.Bresv ← 0 32: return A BORT(Infeasible within Budget/Deadline) 33: end if 34: ▷ Phase IV: COMMIT (Publish Schedule & Advance Generation) 35: Σ.g ← Σ.g + 1 ▷ Advance plan generation monotonically 36: Σ.ρ ← ρcand ; Σ.Ω ← Ωlive cand cand 37: Σ.Bresv ← Bresv + Cost(∆π); Σ.Brem ← Brem − Cost(∆π) 38: Σ.Vπ ← Vcand ∪ ∆π.Vπ ; Σ.π ← SpliceDAG(Σ.π, ∆π, tnow ) 39: Σ.tdispatch ← t′dispatch ; return Σ
Algorithm 3 Complete AAS Scheduling and Execution Loop Require: Proposal q, initial state s0 , context χ, deadline Tdead , budget B, constraints D, T Ensure: Admission certificate Cq or R EFUSE 1: Initialize Σ.s ← s0 ; Σ.ρ ← ρ(q, s0 ); Σ.Ω ← FΠ (Σ.ρ, q, s0 ); Σ.g ← 0 2: Σ.Bcommit ← 0; Σ.Bresv ← 0; Σ.Brem ← B; Σ.Vdone , Σ.Estore , Σ.Eseen , Σ.Jrun ← ∅ 3: Σ.π ← SynthesizePlan(Σ.Ω, A, Σ.Brem , D, T ) 4: if Σ.π = I NFEASIBLE then return R EFUSE(No plan within budget/deadline) 5: end if 6: Σ.Bresv ← Cost(Σ.π); Σ.Brem ← Σ.Brem − Cost(Σ.π); Σ.tdispatch ← TargetDispatch(Σ.π) 7: while tnow < Tdead do 8: for each ready operation a ∈ Σ.Vπ with σπ (a) ≤ tnow in state Ready do 9: if ρ(a) ⪰ τΠ then ▷ Consequential sub-admission 10: Ca ← RecursiveCAC(a, Σ.s, Σ.Brem ) 11: if Ca = R EFUSE then 12: CancelAll(Σ.Jrun ); return R EFUSE(Sub-admission failed) 13: end if 14: end if 15: Transition a → Running; move c(a) from Σ.Bresv → Σ.Bcommit ▷ Charged once at launch 16: Launch a into Σ.Jrun tagged with generation Σ.g and timeout ℓ̂(a) 17: end for 18: Await next asynchronous event E or timeout until earliest scheduled launch 19: if Wall-clock timeout with tnow ≥ Tdead then 20: CancelAll(Σ.Jrun ); refund unspent Bresv → Brem ; return R EFUSE(Deadline exceeded) 21: end if 22: if E.id ∈ Σ.Eseen then 23: continue ▷ Discard duplicate event idempotently 24: end if 25: Σ.Eseen ← Σ.Eseen ∪ {E.id} 26: if E is an operation termination event (job a) then 27: Σ.Jrun ← Σ.Jrun \ {E.job}; Σ.Vdone ← Σ.Vdone ∪ {a} 28: if E carries stale generation gE < Σ.g then 29: Transition a → Superseded; reconcile physical effects via AdaptiveRepair(Σ, E, tnow ) 30: continue 31: end if 32: Transition a → Completed (or Failed/TimedOut); refund unused reservations 33: end if 34: if E is Affirmative Refutation then 35: CancelAll(Σ.Jrun ); return R EFUSE(Predicate refuted) 36: else if E returns valid receipt e from operation a then 37: Ingest e into Σ.Estore only if a was verified (including Ca if consequential) 38: end if 39: if E alters state s or is operation fault/timeout then 40: Σ ← AdaptiveRepair(Σ, E, tnow ) 41: if Σ = A BORT then return R EFUSE(Repair failed) ▷ Retain physical state Σ.s; refuse safely 42: end if 43: end if 44: Σ.Wq ← ExtractWitnesses(Σ.Ω, Σ.Estore ) 45: if Σ.Wq satisfies quorums and EFD cuts for all Σ.Ω then 46: if Readiness (22) and execution-window freshness (25) hold for Σ.Wq at tnow then 47: ssnap ← Σ.s; verdict ← CAC . Discharge(Σ.Ω, Σ.Wq , ssnap , χ) 48: if verdict = S ATISFIED then 49: Cq ← CAC . MintCert(q, ssnap , Σ.Wq ) 50: if Σ.s.ν ̸= ssnap .ν then ▷ CAS check: concurrent state invalidation 51: Discard Cq ; Σ ← AdaptiveRepair(Σ, VersionConflict, tnow ) 52: else 53: return Cq ▷ Authoritative admission succeeded 54: end if 55: end if 56: end if 57: end if 58: end while 59: CancelAll(Σ.Jrun ); refund unspent Bresv → Brem ; return R EFUSE(Deadline exceeded)
30