The Intersection Algebra of Safety, Cosafety, Liveness, and Coliveness over Linear Temporal Logic

Runtime verification of linear-temporal-logic (LTL) properties needs a precise classification of which omega-regular properties can be monitored, in what verdict alphabet, and with what residual evidence on the unverified portion. Alpern and Schneider partitioned properties into safety and liveness; Kupferman and Vardi added cosafety; coliveness completes the symmetric structure. We integrate these four families into a single intersection algebra over omega-regular properties, develop its operational counterpart as a verdict-alphabet ladder spanning binary, ternary, four-valued, and quantitative monitor systems, and connect the two layers through a universal-attribution theorem. On the classification side, the four families generate a sixteen-cell exclusive partition of the omega-regular properties under combined topological and prefix-quantifier membership. The partition is equivalent, modulo two degenerate singletons, to the nine-cell verdict-axis partition of Peled and Havelund. We give independent topological and prefix-quantifier derivations of the empty cells, a De Morgan duality structure on the partition induced by the LTL temporal dualities, and a literature-anchored worked-example catalog with provenance per cell. On the operational side, a verdict-alphabet ladder spans verdict cardinalities one, two, three, four, and infinity (with the trivial baseline at one, the qualitative rungs at two, three, and four, and the quantitative limit at infinity). Definitive verdicts on every trace characterise the clopen cell, and on every violation or every satisfaction the safety or cosafety properties, which the three-valued rung covers in a single monitor; there definitive verdicts saturate: the four-valued and quantitative rungs add revocable and quantitative information but resolve no further cell, and monitorability in the sense of Pnueli and Zaks is not a function of the cell. A universal-attribution theorem shows that every non-trivial verdict monitor canonically yields, for each verdict, a persistence pullback property on its input, the pre-image of a Liveness-and-Coliveness property of its verdict trace; this pullback is itself Liveness-and-Coliveness exactly when, after every input prefix, the verdict trace can still both settle on that verdict and fail to settle on it. The framework supplies a precise vocabulary for the calibration analysis of monitor-based epistemic guarantees on omega-regular properties. --- Version note (v3; changes from v2, 10.5281/zenodo.21099448). This version contains (1) a citation-integrity review: attributions were made faithful to the cited sources, bibliography entries corrected, and one contribution claim restated as a restatement of an observation of Peled and Havelund; and (2) a consolidated formal erratum of the monitorability overlay. The v2 overlay read Pnueli-Zaks monitorability off the 16-cell membership and conflated verdict completeness with verdict reachability; a new Lemma 5.9 separates the three notions. Replaced, weakened or restricted results: Proposition 10.10 (three-valued monitor, now characterised by completeness and reachability), Proposition 10.15 (the four-valued rung resolves no further cell), Proposition 10.17 (robustness adds no definitive verdict), Remark 11.2 (the monitorable sets are those whose boundary has empty interior), Remark 9.11, Proposition 7.5 (effective verdict cardinality values), Definition 10.5 and Proposition 10.6 (binary monitors now required to commit), Theorem 10.20 (hypotheses restated), Theorem 8.2 (1),(3),(4), Remark 5.8 (2)-(3), the Manna-Pnueli placement of the quaestio cell in Section 8, and dependent statements, tables and captions. The v2 abstract's claim that each rung resolves a strictly larger family of cells is withdrawn: definitive verdicts saturate at the three-valued rung. The four-class taxonomy, the intersection algebra and the 16-cell partition are unchanged, and every v2 result keeps its number (one lemma added).