# 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.

A seminal paper is An Automata-Theoretic Approach to Automatic Program Verification. The idea is to use a Büchi automaton, which is just a normal finite state automaton with a notion of acceptance that works on infinite words. The key result is that you can turn an LTL formula into a Büchi automaton that accepts exactly the computations that satisfy the LTL formula. A model checker takes your specification and produces a Büchi automaton, then it takes the LTL constraint, negates it, and produces a Büchi automaton for it. Finally, it intersects the two Büchi automata and endeavors to show that the resulting automaton accepts nothing, i.e. describes the empty language. It does this by conceptually (and to a large extent actually) enumerating all the states. In practice, the state space is way too large to be completely enumerated and this is why model checkers are not theorem provers.

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$.

It's the "this particular trace" that is problematic. For safety properties, it is enough to visit each state. How you get to a state for the most part doesn't matter. You'll want to keep track of which states have been visited to avoid (potentially infinite) repeated work, but it doesn't matter which trace visited a state. For liveness properties, it is not enough to know that some trace has visited a state. You need to know if this trace has visited that state. The upshot is that checking a safety property just requires enumerating the reachable states, while checking a liveness property requires cycle detection. Of course, there are linear-time algorithms for calculating strongly connected components. Due to the sheer number of states, transcribing textbook algorithms is often not adequate. You can see an indication of some of the issues here. As far as I can tell from the source code and that page, TLC does just do Tarjan's algorithm, but this interacts poorly with distribution (i.e. liveness checking is not supported in the distributed mode) and with symmetry reduction techniques to reduce the state space. It is also just inherently slower than checking safety properties.