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); each rung resolves a strictly larger family of cells. A universal-attribution theorem shows that every non-trivial verdict monitor canonically yields Liveness-and-Coliveness pullback properties on its input, regardless of which cell its target property occupies. The framework supplies a precise vocabulary for the calibration analysis of monitor-based epistemic guarantees on omega-regular properties.