Lately I've been trying to learn how TLC does liveness checking by reading sections of the textbooks Principles of Model Checking (Baier, Katoen, 2008) and Temporal Verification of Reactive Systems (Manna, Pnueli, 1995). The literature is all about checking LTL (Linear Temporal Logic) formulas generally, and while TLA+ isn't exactly the same as LTL it's at least a linear temporal logic (as opposed to branching temporal logic) so the concepts are broadly transmissible. The main difference I've found is that TLA+ requires all formulas to be stuttering-insensitive.
Before learning how LTL liveness properties are checked I've been going through the introductory safety property chapters to build familiarity with LTL vocabulary. In TLA+ we have two types of safety properties, basic invariants which are checked in each state and action-level properties [][A]_v which check that every step taken satisfies some formula A over primed & unprimed variables. LTL tries to address a much broader class of safety properties, and of interest here are regular safety properties. Regular as in "regular language", "regular _expression_", etc., not as in "ordinary". Basically it means the set of properties that can be checked by sending a state trace into a finite automaton; if the trace ends in the automaton's accept state, the trace is a counterexample to the property.
At first glance TLA+ doesn't seem to directly support regular safety properties, beyond the standard tactic of moving various "hasVisited" type flags into the user variable space so the safety property can be written as a standard invariant over those variables. But it strikes me that this bears some resemblance to refinement! In LTL there's a labeling operator, where system states are projected onto subsets of atomic propositions that are fed into the finite automaton, which looks quite a bit like transforming variables in the INSTANCE AbstractSpec WITH val <- op(x) syntax usually used with refinement. And the state graph of the abstract spec is sort of like a finite automaton, although there isn't an accept state that would falsify a trace.
In fact, I have found myself thinking of refinement as a "whole system safety property", which doesn't really make sense since refinement is fundamentally a liveness property, but from this perspective maybe it does. Refinement lets you express "safety" properties like "your system will go through this series of states in this order" which standard invariants can't really capture. So this might explain why I find refinement more intuitive than encoding properties in temporal logic expressions in TLA+.
Of course, the technical difference between safety and liveness properties is that safety properties can be falsified by finite traces, while liveness properties can only be falsified by infinite traces (in practice, a finite series of states ending in an infinite loop). So on those grounds I don't know if it makes sense to talk about refinement as a safety property.
Anyway this was kind of meandering but it's been rolling around my head so I thought I would type it up.
Andrew Helwer