supervisory-control.md

Supervisory control: the mathematics under Pitot and Boatstack

This document is the canonical statement of the control theory the system implements. It is host-agnostic and domain-agnostic: coding agents today, any gated agent workflow tomorrow. New capabilities extend the system by classifying new events into the partitions below. The theorems then apply unchanged.

Framework: supervisory control of discrete-event systems (Ramadge & Wonham, 1987). Standard reference: Cassandras & Lafortune, Introduction to Discrete Event Systems.

1. Objects

Plant. The agent plus its host environment is the plant G, a generator of event strings over a finite alphabet Σ. L(G) ⊆ Σ* is every session the plant can physically produce. L_m(G) ⊆ L(G) is the marked language: strings that represent completed deliveries (shipped, with receipts).

Alphabet. Σ is Pitot's canonical event schema. Every event in the system is a letter of this alphabet. Examples: action.requested(shell), file.touched, question.raised, answer.given, approval.granted(h), evidence.recorded(AC), claim.asserted(done), pr.mutation, boundary.fault(reason).

Control partition. Σ = Σ_c ∪ Σ_u.

• Σ_c (controllable): events the host presents synchronously for permission and that can therefore be disabled — shell execution, PR mutation, publication, sends, and claim assertions gated by hooks. The bridge is the physical channel that carries enable/disable for these events.
• Σ_u (uncontrollable): everything else the agent does — reasoning, edits, tool outputs, any event without a hook. These can at most be observed.

Observation partition. Σ = Σ_o ∪ Σ_uo, with the natural projection P : Σ* → Σ_o* that erases unobservable events from a history.

• Σ_o: events Pitot's adapters decode into canonical form.
• Σ_uo: everything the sensing channel does not capture.
• A boundary.fault is not plant behavior; it is degradation of the observation channel itself, and is reported as such.

Supervisor. Boatstack is the supervisor S: a map from observed histories to control patterns, S : P(L(G)) → Γ, where Γ = { γ ⊆ Σ : Σ_u ⊆ γ }. The constraint Σ_u ⊆ γ is structural: the supervisor may only withhold permission for controllable events. It can never force the plant to act and never disable an uncontrollable event. This is the formal statement of "governs claims of approval, completion, review, and shipping — not implementation technique." Boatstack's plan locks, approval receipts, evidence ledgers, and gap ledgers are the state realization of S.

For controllable side effects, an operation receipt refines that state realization. Without it, histories not_started, executing, succeeded_unobserved, and failed can have the same projection even though they require different control decisions. Boatstack therefore records PREPARED -> AUTHORIZED -> EXECUTING -> SUCCEEDED and projects uncertain completion to RECONCILE_REQUIRED. A retry is enabled only after an observation distinguishes success from absence.

Subprocess supervision preserves the transport alphabet before making that observation: stdout carries typed machine results, stderr carries bounded diagnostic text, and the exit status selects success or failure. Collapsing those channels would allow a warning to masquerade as a path, ref, URL, or workflow event, so conformance tests prohibit combined output in production controllers.

Specification. K ⊆ L(G) is the legal language: the delivery spec expressed as constraints on event order. Examples:

• every ship is preceded by approval.granted(h) where h equals the fingerprint of the plan in force at ship;
• every claim.asserted(done, AC) is preceded by evidence.recorded(AC);
• no pr.mutation outside an approved, unexpired plan lock.

2. Conditions and theorems

Controllability. K is controllable w.r.t. L(G) and Σ_u iff

pr(K) · Σ_u ∩ L(G) ⊆ pr(K)

(pr is prefix closure.) In words: no uncontrollable event can ever carry the system out of the legal set, because the supervisor could not have stopped it. Design rule: specifications may only constrain controllable events. A spec that tries to constrain technique (uncontrollable events) is uncontrollable and cannot be enforced; it must be weakened to its supremal controllable sublanguage.

Observability. K is observable w.r.t. L(G), P, Σ_c iff any two histories with the same projection demand the same enable/disable decisions: for s, s' ∈ pr(K) with P(s) = P(s') and σ ∈ Σ_c, if sσ ∈ pr(K) and s'σ ∈ L(G) then s'σ ∈ pr(K). Design rule: the sensor alphabet must be rich enough to make the spec observable, and the spec must not depend on distinctions the sensor cannot make. Pitot and Boatstack are co-designed against this condition.

Existence. A supervisor achieving exactly K exists iff K is controllable and observable (with the usual closure conditions). If K is not controllable, the supremal controllable sublanguage

supC(K) = ∪ { K' ⊆ K : K' controllable }

exists and is unique (controllability is closed under arbitrary union). The least-restrictive supervisor implements supC(K): it disables the minimum necessary. This is the formal version of minimum-interference gating.

Nonblocking. S is nonblocking iff

L(S/G) = pr( L_m(S/G) )

— from every reachable state, some path to a marked (delivered) state remains open. The supervisor must never wedge delivery permanently. Repair flows exist to preserve this property: a blocked state is always blocked toward a defined recovery path, never absorbing.

Fail-closed as a corollary. Under observation loss (boundary.fault, undecodable payloads), P is no longer trustworthy, so membership of the current history in pr(K) cannot be certified. The only control pattern that guarantees the spec is

γ = Σ_u

— disable every controllable event until the measurement chain is healthy again. Fail-closed is not a policy preference; it is the unique safe pattern under lost observability. Recovery is bounded and diagnosable (diagnose-hook), and boundary faults are classified distinctly from plant misbehavior so downstream repair targets the channel, not the work.

3. Privacy as projection coarsening

Hash-only export replaces event content with sha256(content). Formally this is a coarsening of the projection P → P': fewer histories are distinguishable. The observability condition then gives an exact test for how much privacy the system tolerates:

Coarsen P until two histories that require different control decisions become indistinguishable. At that point the spec is unenforceable at that privacy level.

Privacy and enforceability are a measurable trade along the same operator. A spec whose decisions depend only on event types, hashes, and prior receipts remains observable under hash-only projection; a spec whose decisions depend on content does not. Every export policy should be checked against this condition.

4. Component boundaries (who owns which symbol)

Symbol	Meaning	Owner
Σ, schema	Event alphabet	Pitot
Σ_c / Σ_u	Control partition (what hooks gate)	Pitot declares, per host adapter
Σ_o / Σ_uo, P	Observation partition and projection (incl. privacy coarsening)	Pitot
Enable/disable transport for Σ_c	Bridge (carries a consumer-supplied decision; contains no policy engine)	Pitot
S (state: locks, receipts, ledgers)	Supervisor	Boatstack
K	Specification (delivery spec)	Boatstack
supC(K), nonblocking, repair	Supervisor synthesis properties	Boatstack
boundary.fault classification	Health of the measurement chain	Pitot reports, Boatstack responds

Pitot is neither the supervisor nor the specification: it defines the alphabet, the projection, and the transport. Boatstack is not the sensor: it consumes canonical events like any other subscriber and supplies decisions through the bridge like any registered controller.

5. Pre-activation authority latch

For managed planning, successful auto-plan adds a controllable phase boundary before the active-delivery supervisor exists. Let q be the repository-derived phase:

• no saved managed plan: product mutation remains outside this supervisor;
• draft, approved, or policy-ready: mutation events are disabled while read and exact planning/activation transitions remain enabled;
• locked active delivery: the existing delivery supervisor owns mutation;
• ambiguous, stale, or invalid: fail closed into one recovery event.

The baseline-diff fingerprint is the observation that distinguishes pre-existing operator edits from post-plan implementation. Approval and activation both re-observe it. This makes mutation denial controllable without discarding user work and makes drift observable without treating conversation or async task completion as authority.

6. Extension rule

To add a new host, a new event, or a new domain (communications, filings, payments):

1. Add the event(s) to Σ via the canonical schema.
2. Classify each into Σ_c or Σ_u (is there a synchronous permission point?).
3. Classify each into Σ_o or Σ_uo (can the adapter decode it?).
4. Extend K only with constraints on Σ_c events (controllability), using only distinctions P preserves (observability).
5. Verify nonblocking: every new blocked state has a defined path to a marked state.

No other change is required. The theorems carry the rest.

References

• P. J. Ramadge and W. M. Wonham, "Supervisory control of a class of discrete event processes," SIAM Journal on Control and Optimization, 25(1), 1987.
• W. M. Wonham and P. J. Ramadge, "On the supremal controllable sublanguage of a given language," SIAM Journal on Control and Optimization, 25(3), 1987.
• C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, Springer.