18 hours ago
- The author introduces temporal operators A (always) and E (eventually) from linear temporal logic to express system properties, covering safety and liveness.
- A third class of properties, P (possibility), asks whether something can happen in a model, even if not guaranteed; this includes reachability properties.
- Combining operators yields expressions like A(P(x)) (always possible) and A(x => P(y)) (from any state where x is true, y is possible), which cannot be expressed with A and E alone.
- The main use of P is as a sense-check for specifications: verifying that a state like 'Retry' is actually reachable, to avoid trivial satisfaction of liveness properties.
- Tools like Alloy and TLA+ do not natively support P; simple reachability can be mimicked by checking counterexamples to A(!x), but combined operators like A(P(x)) are harder to verify.
- The author notes a chicken-and-egg problem: since tools cannot verify possibility properties, practitioners are not used to noticing them in system designs.