Title. The talk is about machine-checkable liveness proofs.
Four latches start at zero, selecting the initial graph state.
The selected inputs pick an outgoing edge of the current state.
The latch values update and the highlighted current state moves at the same time.
After four input choices, the reached state violates P, so the highlighted path is a bad trace.
The second state-space view comes out of the first as a clean copy.
A liveness counterexample is another trace that ends in a cycle with a violating transition.
A complex model checker returns traces for unsafe answers or a witness circuit for safe answers.
The independent checker validates the model and witness circuit.
These are the certification papers behind the safety column.
Liveness has several successful algorithms and transformations.
The contribution is one proof format that spans safety and liveness.
W has the same behavior as M
W is obviously safe and obviously live.
The eight SAT obligations appear together within their three checking blocks.
The certificate checker emits a fixed set of formulas, and those formulas go to the SAT solver.
Simulation obligations beside a concrete model trace.
Reset constructs the first witness state.
Transition extends the witness trace in lockstep.
Assume every witness state is safe.
Safety transfers that marking back to the model.
Assume the witness proves progress on the suffix.
Liveness transfers those marked progress transitions to the model.
Base proves the reset witness state safe.
Induction propagates safety along the witness trace.
Assume the same violating edge appears twice in the trace.
Decrease gives the first backward Q edge.
Closure carries the backward Q edge to the repeated state.
repeated edges are live
The safety algorithms are already established; now introduce the four liveness approaches.
The running example has two transitions that violate Q.
Each violating edge marks its source state.
At k=0, both marked states are still bad.
Increasing k once makes the first state safe.
The final counter values match the current k-Liveness witness.
The witness turns the bound into monotone Q' edges.
k-Liveness: model checking runtime.
k-Liveness: model checking plus certificate checking.
The counter states and their binary latch values line up.
First query the most significant bit.
Start with the compact b0 implication check.
Only after the check is complete do we dim the b1-changing edge.
Mark an arbitrary finite prefix of the infinite trace.
Shift the infinite suffix left; its continuing tail makes it look unchanged.
The same filtering step dims the b0-changing edges.
Construct the witness relation: every binary state points to every lower state and to itself.
The paper's comparator definition uses dec for a lower stabilizer value and eq for equally stable states.
k-Liveness+stabilizing: model checking plus certificate checking.
Start from the same four-state running example as k-Liveness.
The additional edge from the last state to the first closes a cycle that is not live.
The run first crosses the violating edge from state 0 to state 1.
State 1 is stored and the copy latches hold it fixed.
The added edge returns the run to state 0 while state 1 stays stored.
At state 0, the bad edge leads back to stored state 1, exposing the not-live cycle as a safety violation.
The running example places (0,1) under state 0 and the three pairs ending in state 3 under state 3.
Those listed pairs are exactly the red forbidden transitions.
All remaining state pairs are green, so the L2S witness proves Q on them.
L2S: model checking plus certificate checking.
Start rLive from the same four-state running example.
Create an enlarged search node around state 0 and its outgoing edge.
The squiggly connector represents a path to the enlarged state-2 transition.
The search from state 2 ends in failure.
The first closed region contains state 3.
Backtrack from the enlarged state-2 transition to state 0.
A different search direction from state 0 also fails.
The next region contains the enlarged state-2 transition and state 1.
A third search from the enlarged state-0 transition ends in failure.
The third highlighted region contains states 0 and 2, but no other states.
Keep only the lowest invariant number for each state.
Draw a green witness edge exactly when the invariant number can increase or stay equal.
rLive: model checking plus certificate checking.
rLive-others: model checking runtime.
rLive-others: model checking plus certificate checking.
rLive points staged on the y-axis.
rLive points move to their related-work checking times.
rLive speedup diagonal.
k-Liveness comparison.
stabilizing+k-Liveness comparison.
The eight obligations establish safety and liveness with low overhead. The paper and code are at froleyks.de.
References used in the talk.
The current certificate checker assumes one liveness signal.
Future work extends the format to a set of liveness signals, where one signal must eventually remain true.
Simulation now preserves every liveness signal separately.
Decrease and closure use the disjunction of all signals.