Liveness Checking Algorithm in TLC

The algorithm is described in the book: "temporal verification of reactive systems: safety"

The liveness checking algorithm in TLA+ verifies temporal properties in specifications - properties that describe how a system should behave over time. Unlike safety properties (which check that bad things never happen), liveness properties assert that something good eventually happens.

The algorithm works by:

1. Converting temporal formulas to a specific normal form
2. Building a behavior graph that combines the state space with a tableau
3. Searching for strongly connected components (cycles) in this graph
4. Checking if any cycle violates the liveness properties

If a violation is found, the algorithm constructs a counterexample to show the problematic behavior. LiveWorker.java:33-41

The algorithm starts by parsing the liveness properties defined in the specification and converting them to a workable form:

1. Temporal formulas are parsed and converted to LiveExprNode objects through the astToLive method
2. The formulas are tagged, simplified, and converted to Disjunctive Normal Form (DNF)
3. The DNF is then classified into different types of expressions:
   • AEAction: Eventually Always Actions ( []<>A )
   • EAAction: Always Eventually Actions ( <>[]A )
   • AEState: Eventually Always States ( []<>S )
   • tfs: Temporal formulas with no actions

Liveness.java:498-533

For each temporal formula, the algorithm creates:

1. A tableau graph representation
2. An "Order of Solution" that contains the tableaux and checks to perform

The Order of Solution organizes how the algorithm will verify the different components of liveness properties.

Liveness.java:682-777

The algorithm constructs a behavior graph that combines:

1. The state space graph from model checking
2. The tableau representation of the liveness properties

This combined graph is stored using a disk-based representation (DiskGraph or TableauDiskGraph).

LiveCheck.java:522-615

When the behavior graph has tableaux, a more complex graph construction is used: LiveCheck.java:617-709

The core of the liveness checking is performed by the LiveWorker class, which searches for strongly connected components (SCCs) in the behavior graph:

1. The algorithm uses an iterative version of Tarjan's algorithm to find SCCs
2. It focuses on finding cycles that might violate liveness properties
3. For each SCC found, it immediately checks if it violates the liveness properties

LiveWorker.java:117-147

The main SCC search algorithm: LiveWorker.java:229-319

For each SCC found, the algorithm checks if it violates the liveness properties by examining:

1. AEState conditions: Eventually Always State predicates
2. AEAction conditions: Eventually Always Action predicates
3. Promises: Special temporal conditions that must be fulfilled

LiveWorker.java:530-546

The core violation check: LiveWorker.java:736-766

If a violation is found, the algorithm constructs a counterexample by:

1. Creating a prefix path from an initial state to the SCC
2. Identifying the cycle within the SCC that demonstrates the violation
3. Combining these into a full trace that shows the liveness violation

LiveWorker.java:822-853 LiveWorker.java:887-896

The liveness checking is not performed after every state exploration step, as that would be too expensive. Instead, the algorithm:

1. Runs liveness checking periodically based on how much the behavior graph has grown
2. Uses a threshold to determine when to run the check
3. Always performs a final check on the complete graph

LiveCheck.java:171-200 LiveCheck.java:225-242

The algorithm can leverage multiple cores by:

1. Creating multiple LiveWorker threads to check different parts of the behavior graph
2. Using a queue to distribute the work among the workers
3. Synchronizing the results and error reporting

LiveCheck.java:262-276 LiveCheck.java:289-300

• Liveness checking in TLA+ is based on the theory of temporal logic described in Manna & Pnueli's work, but with adaptations to handle TLA's action formulas.
• The algorithm uses an on-disk representation of the behavior graph to handle large state spaces.
• Compared to safety checking, liveness checking is more computationally expensive, which is why it runs periodically rather than after every state generation.
• The tableau construction is a key theoretical component that allows the algorithm to check arbitrary temporal formulas.
• Tarjan's algorithm for finding strongly connected components is at the core of the liveness checking mechanism.
• The content of this page was generated by deepwiki.com.