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.