Research: evaluate BAIT Büchi inclusion and antichain fixpoints for temporal ownership protocols (bounded spike) #446

Classification

• Type: bounded research / external prior-art evaluation
• Priority: P3 / backlog; not a production implementation request
• Area: OwnIR, state/obligation protocols, fixpoint algorithms, temporal verification
• External project: phreppo/bait (Büchi Automata Inclusion Tester)
• Paper: Doveri et al., Inclusion Testing of Büchi Automata Based on Well-Quasiorders, CONCUR 2021
• Related Own.NET work: P1: Add Obligation Protocols for project-specific barrier-sensitive rules #272 (intraprocedural obligations), P2: Extend MOS/effect summaries to protocol and barrier effects #274 (protocol/effect summaries), State protocols: affine tokens — an unspent (terminal) state token must not be OWN001 #392 (affine state tokens), State protocols: diagnostics on protocol tokens use IDisposable wording ("used after it is disposed") #393 (state-token diagnostics), feat(progress): Own.Progress — detect consume-or-exit loop stalls (PRG001) #275 (loop progress), Research: evaluate Tabby-style stateful path pruning for bounded ownership diagnostics #424 (stateful path pruning)

Research question

Is there a concrete, currently unsupported Own.NET temporal/protocol property whose verification would materially benefit from Büchi-language inclusion or its antichain/fixpoint machinery, compared with the existing CFG/dataflow/MOS approach or a simpler finite-state monitor?

BAIT checks L(A) ⊆ L(B) for languages of infinite words recognized by Büchi automata. It is not a C# analyzer, Roslyn frontend, or ownership checker. Its Java CLI accepts two automata in .ba format and returns inclusion/non-inclusion plus statistics.

An attractive example such as Acquire → Dispose → Use is a finite safety violation and does not justify Büchi machinery. The same is true of ordinary barrier obligations from #272 and use-after-transition from #392. A benefit must be demonstrated using an actual requirement, not an invented infinite-trace problem.

Verified implementation details to investigate

• BAInc.java computes X/Y fixpoints with a changed-state frontier and checks inclusion.
• Antichain.java removes subsumed elements under a partial order; this technique might be independently useful for Own.NET state explosion.
• Runner.java returns a boolean and stats; it does not provide a source-level witness/counterexample for a failed inclusion.
• The reference implementation is a small Java/Gradle research artifact (release v0.1 in 2021, latest repository commit inspected: 2023-09-07), not an integration-ready .NET library. README's Java 8+ claim also needs checking against Path.of / var usages in source.

Bounded investigation

Gate 1: select a real property or stop

1. Inventory existing capabilities/limits in P1: Add Obligation Protocols for project-specific barrier-sensitive rules #272, P2: Extend MOS/effect summaries to protocol and barrier effects #274, feat(progress): Own.Progress — detect consume-or-exit loop stalls (PRG001) #275, State protocols: affine tokens — an unspent (terminal) state token must not be OWN001 #392 and the current OwnIR/MOS analyzer path.
2. Pin one real, source-grounded property that concerns potentially unbounded executions, and state explicitly whether it is:
   • finite-trace safety, expressible with current dataflow/FSM;
   • Büchi-recognizable infinite-trace safety or liveness;
   • outside a finite-state model without additional abstractions.
3. For any claimed liveness/progress property, enumerate fairness, scheduling, environment, nondeterminism, loop abstraction, and termination assumptions. Never infer liveness from an incomplete CFG/model.
4. If no legitimate ω-behavior property beats a conventional finite-state/dataflow solution, record NO-GO for Büchi inclusion. Optionally continue only with the independently justified antichain experiment below.

Gate 2: minimal offline model comparison (only if Gate 1 passes)

• Hand-author two very small .ba automata: abstracted implementation behavior and allowed protocol behavior. Document event alphabet, accepting states, and how finite C# traces are treated in the infinite-word model.
• Pin BAIT source commit and runtime; reproduce at least one inclusion PASS and one FAIL; test a near-neighbor that a simplistic model would mishandle.
• Compare against a basic finite-state monitor / existing Own.NET facts, using the same modeled property and assumptions. Establish what additional class of bugs (if any) the Büchi approach detects.
• Measure model size, execution time, memory if practical, and report whether failure can be explained by a meaningful source-level path. BAIT's boolean FALSE alone is not a diagnostic witness.
• Keep all modeling/prototyping offline; do not modify production OwnIR schema, Python/Rust parity logic, CLI, or analyzer diagnostics for the experiment.

Optional separate branch: antichain / frontier reuse

If the temporal-use-case gate fails but an existing Own.NET fixpoint/path-state bottleneck is evidenced, test antichain subsumption + changed-state frontiers as an algorithmic technique against a pinned baseline.

Require a sound subsumption relation for resource identity, may/must/unknown, aliasing, calls, and barriers. Compare peak state count, runtime, and confirmed diagnostics retained on adversarial examples. Never suppress an existing true positive merely because a state appears dominated under an unsound ordering. Do not overlap with #424 without identifying a distinct measurable improvement.

Acceptance / kill criteria

• Short source-backed technical note on BAIT's algorithm, interface, assumptions, maturity, and limits.
• One specific Own.NET property with baseline and competing finite-state/dataflow formulation, or justified NO-GO.
• If a candidate survives: reproducible tiny .ba fixtures; expected inclusion/non-inclusion; near-neighbor controls; measurements and limitations.
• Separate evidence, if any, for antichain/frontier optimization; no speculative speedup claims.
• Explicit final verdict: GO (with quantified advantage), NO-GO, or DEFER (missing precondition).
• No production code/diagnostic changes, no language/schema expansion, no mandatory user-authored automata in this issue.

Non-goals

• Replacing Own.NET's CFG/ownership engine with Büchi automata.
• Claiming infinite-trace soundness from bounded traces.
• Building a general LTL model checker or a Java bridge.
• Treating obligations, use-after-dispose or state-token misuse as novel Büchi use cases when current finite-state/dataflow analysis already covers them.