docs/FOUR-STATES.md

Why four states, and why this order

Semantic grounding for the completion signal.

---

The claim, stated carefully

We did not invent a four-valued answer. We arrived at one, and then found that runtime verification had derived the same shape thirty years earlier for the same reason. This document says exactly how far that correspondence goes — and where it stops — because overclaiming here would be worse than not citing it at all.

What we claim: our precedence order is the settled-verdict order, and our refusal to let UNRESOLVED count as a pass is the same refusal LTL₃ makes.

What we do not claim: that this is an LTL monitor, or an implementation of RV-LTL. It is not. We have not built a Moore machine over an ω-language.

---

LTL₃ and the refusal to guess

Bauer, Leucker and Schallhart's LTL₃ evaluates a linear-temporal-logic formula over a finite prefix of an infinite word — that is, over what has happened so far, when the future has not arrived yet. It is three-valued:

LTL₃	meaning
⊤	every possible continuation satisfies the formula — the verdict is settled
⊥	no possible continuation satisfies it — settled the other way
?	both a satisfying and a violating continuation exist — inconclusive

The third value exists because collapsing it into either of the other two would be a lie. A monitor that reports ⊤ when some continuation still violates the property has claimed knowledge it does not have.

That is our first invariant, exactly: UNRESOLVED is never a pass. We reached it from operations — a gate that treats "we did not measure it" as "it is fine" will eventually approve something it should not have. LTL₃ reaches it from semantics. The agreement is worth noting precisely because the two routes are independent.

Bauer, Leucker & Schallhart, Runtime Verification for LTL and TLTL, ACM TOSEM 20(4), 2011. https://cs.uwaterloo.ca/~bbonakda/teaching/CS745/papers/RV.pdf

RV-LTL and the four-valued refinement

RV-LTL refines the inconclusive verdict into two, giving four values: satisfied, violated, presumably satisfied, presumably violated — where the "presumably" pair covers prefixes whose ω-verdict is not yet settled but whose finite-word semantics leans one way.

Bauer, Leucker & Schallhart, Comparing LTL Semantics for Runtime Verification, Journal of Logic and Computation 20(3):651–674, 2010. https://academic.oup.com/logcom/article-abstract/20/3/651/1016387

The correspondence is structural, not an isomorphism. RV-LTL's axis is certain vs presumptive; ours is complete vs obstructed. The honest mapping:

ours	nearest RV-LTL / LTL₃ notion	settled?
BLOCKED	⊥ — no continuation satisfies it	yes
COMPLETE	⊤ — every continuation satisfies it	yes
PARTIAL	presumably satisfied, under recorded waivers	no
UNRESOLVED	? — inconclusive	no

Why BLOCKED dominates

Our precedence is BLOCKED > UNRESOLVED > PARTIAL > COMPLETE.

Read through the lens above, this is not a preference. Settled verdicts dominate unsettled ones, and among settled verdicts the negative one dominates because a violated non-negotiable admits no continuation that satisfies the rulebook. There is no waiver path in the engine — not as policy, but as an absence of code.

An unsettled verdict can still become either. That is why UNRESOLVED outranks PARTIAL: a waived, recorded, human-owned shortfall is a decision someone made, whereas an unevaluated rule is a decision nobody has made yet. Acting on the second is acting without an owner.

This is a checkable statement rather than a rhetorical one, and it is checked: engine.properties.test.js asserts across thousands of generated rulebooks that any UNEVALUATED rule forces UNRESOLVED or BLOCKED, and that a COMPLETE signal implies every rule was actually evaluated.

Monitorability, and when BLOCKED is terminal

A property is monitorable from a given prefix when some extension still settles it. Once no extension can, the verdict is final and further observation is wasted effort.

Our recourse.js computes exactly this distinction operationally: if a non-negotiable rule is violated, no acquisition of evidence changes the outcome, and the gate reports terminal rather than offering a list of measurements. Telling an operator to collect more data when nothing can help is worse than telling them nothing.

Aceto, Achilleos, Francalanza, Ingólfsdóttir & Lehtinen, An Operational Guide to Monitorability, 2019. https://arxiv.org/pdf/1902.00435

The second invariant has a name too

You cannot waive what you never measured.

In eliminative argumentation this is the discipline of defeaters: confidence in a claim rises only as identified defeaters are eliminated by evidence, never by assertion. A waiver eliminates a defeater that was actually raised; it cannot eliminate one that was never enumerated.

Goodenough, Weinstock & Klein, Eliminative Argumentation: A Basis for Arguing Confidence in System Properties, CMU/SEI-2015-TR-005 (public domain). https://resources.sei.cmu.edu/library/asset-view.cfm?assetid=47781

The same idea has a visual convention in GSN, where an undeveloped goal is drawn as a diamond — a claim with no supporting argument yet — and an undeveloped and uninstantiated goal adds a circle, meaning nobody has even said what would satisfy it. Our UNRESOLVED state is the first; a rule with no declared resolvedBy is the second, and auditEvidenceCoverage() reports those as a rulebook defect.

GSN Community Standard v3, SCSC-141C (2021), CC-BY 4.0. https://scsc.uk/gsn

We describe this as a GSN-inspired status vocabulary, not as GSN conformance. GSN is a notation for human safety arguments; we borrow its distinction, not its semantics.

Prior art we are not claiming parity with

• XACML 3.0 decision values are Permit / Deny / Indeterminate / NotApplicable, and its deny-overrides combining algorithm with extended Indeterminate is close to our precedence. Our four states are deliberately isomorphic in shape — inventing decision semantics from scratch is how you get them wrong. What XACML has no analogue for is measurement freshness, which is where our second invariant lives.
• AWS Config ships COMPLIANT / NON_COMPLIANT / NOT_APPLICABLE / INSUFFICIENT_DATA.
• Kubernetes conditions are True / False / Unknown, and the API convention states that the absence of a condition must be read as Unknown.
• GitHub Checks separates status from conclusion, and has a neutral conclusion for a check that ran and declines to judge.
• OPA/Rego distinguishes undefined from false; the idiom default allow := false exists precisely because undefined is not false.

Every one of these is a mature system that independently concluded that "we do not know" needs its own value. That convergence is the argument.

---

The short version, for a reviewer in a hurry

Three of our four states are backed by something outside our own judgement, and two of those are statements about what we cannot do:

• BLOCKED is terminal when a non-negotiable is violated — proved operationally by recourse.js finding no correction set, and structurally by there being no waiver branch in the engine.
• UNRESOLVED is provable in two distinct forms — not yet (with the sample count that would fix it, from the Beta coverage law) and not ever (per-object conditional coverage is impossible distribution-free at finite width, Barber et al. 2021).
• COMPLETE implies every rule was evaluated — asserted as a property over thousands of generated rulebooks, not over the handful we thought of.