Liveness Checking Algorithm in TLC
The algorithm is described in the book: "temporal verification of reactive systems: safety"
High-Level Overview
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:
- Converting temporal formulas to a specific normal form
- Building a behavior graph that combines the state space with a tableau
- Searching for strongly connected components (cycles) in this graph
- 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
Formula Conversion and Preprocessing
Step 1: Processing Liveness Properties
The algorithm starts by parsing the liveness properties defined in the specification and converting them to a workable form:
- Temporal formulas are parsed and converted to
LiveExprNode
objects through theastToLive
method - The formulas are tagged, simplified, and converted to Disjunctive Normal Form (DNF)
- 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
Step 2: Creation of Tableau and Order of Solution
For each temporal formula, the algorithm creates:
- A tableau graph representation
- 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
Behavior Graph Construction
Step 3: Building the Behavior Graph
The algorithm constructs a behavior graph that combines:
- The state space graph from model checking
- 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
Strongly Connected Component Detection
Step 4: Checking for Cycles Using Tarjan's Algorithm
The core of the liveness checking is performed by the LiveWorker
class, which searches for strongly connected components (SCCs) in the behavior graph:
- The algorithm uses an iterative version of Tarjan's algorithm to find SCCs
- It focuses on finding cycles that might violate liveness properties
- 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
Step 5: Checking Components for Violations
For each SCC found, the algorithm checks if it violates the liveness properties by examining:
- AEState conditions: Eventually Always State predicates
- AEAction conditions: Eventually Always Action predicates
- Promises: Special temporal conditions that must be fulfilled
LiveWorker.java:530-546
The core violation check:
LiveWorker.java:736-766
Counterexample Generation
Step 6: Building Error Traces
If a violation is found, the algorithm constructs a counterexample by:
- Creating a prefix path from an initial state to the SCC
- Identifying the cycle within the SCC that demonstrates the violation
- Combining these into a full trace that shows the liveness violation
LiveWorker.java:822-853
LiveWorker.java:887-896
Optimization and Scheduling
The liveness checking is not performed after every state exploration step, as that would be too expensive. Instead, the algorithm:
- Runs liveness checking periodically based on how much the behavior graph has grown
- Uses a threshold to determine when to run the check
- Always performs a final check on the complete graph
LiveCheck.java:171-200
LiveCheck.java:225-242
Parallel Execution
The algorithm can leverage multiple cores by:
- Creating multiple
LiveWorker
threads to check different parts of the behavior graph - Using a queue to distribute the work among the workers
- Synchronizing the results and error reporting
LiveCheck.java:262-276
LiveCheck.java:289-300
Notes
- 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.