# How does TLC check liveness properties?

The paper "Model Checking TLA+ Specifications" published in 1999 explained how TLC (Temporal Logic Checker) checks safety properties written in TLA+ developed by Lamport. At that time, TLC did not yet check liveness properties.

Today, TLC is able to check liveness properties. I want to know:

• What liveness properties is TLC able to check?
• How does TLC check liveness properties?

Any references?

Presumably it can check any "liveness" property that that can be formulated in LTL. A "liveness" property is typically described as a property stating that "something good eventually happens". This is usually contrasted to a "safety" property which states that "nothing bad ever happens". See e.g. Slide 20 of this SPIN tutorial. Basically, a basic safety property will look like $\square P$ which states that it is always the case that $P$ holds, e.g. the temperature is always below boiling. A basic liveness property might look like $\lozenge Q$ which states that $Q$ eventually happens, e.g. eventually the HALT state is reached.
So what's the issue with "liveness" properties that would cause them not to be included from the beginning? To check (the failure of) $\square P$ in a model checker is straightforward. You simply check $P$ for each state. If $P$ ever fails to hold, then you've found a counter-example to $\square P$. On the other hand, checking $\lozenge Q$ requires producing a trace that will never hit a state satisfying $Q$. There are two ways this could happen. First, we could reach a final state without ever going through a state satisfying $Q$. This is straightforward to check. Second, we could enter an infinite loop without ever reaching a state satisfying $Q$. To check this, we need to check if we reach a state that this particular trace has been to before without ever passing through a state satisfying $Q$.