Notebook 10: The Arbiter Kripke Structure

Click through the four-state arbiter Kripke structure from the lecture notes, watch AG(request → AX busy) hold or break in real time, and replay the exact counterexample from the chapter.

The Arbiter Kripke Structure

This notebook is the interactive twin of the arbiter running example from Chapter 7 (Reactive Systems, SMV, and Explicit Model Checking). The arbiter has two state variables, request and state ∈ {Ready, Busy}, giving four states:

  • RF — Ready, no request
  • RT — Ready, request pending
  • BF — Busy, no request
  • BT — Busy, request (still) pending

We check the property \(\mathbf{AG}(\texttt{request} \to \mathbf{AX}(\texttt{state}=\textsc{Busy}))\): whenever a request is present, the very next state must be Busy.

The buggy model is the one from the lecture notes: the SMV case statement’s catch-all TRUE branch leaves the arbiter free to go anywhere, so it can silently drop a pending request. The fixed model adds one clause — if already Busy with a request pending, stay Busy — which is exactly the fix from the chapter’s exercises.

Widget: click through the states

Click any highlighted (reachable) state to take that transition. The property monitor tracks whether \(\mathbf{AG}(\texttt{request} \to \mathbf{AX}(\texttt{state}=\textsc{Busy}))\) has been violated so far along your run — once violated, it stays violated (violations are safety bugs: no future step can undo them, exactly def:safety from the chapter).

Kripke structure

Property monitor: AG(request → AX busy)

Trace so far

What to try

  1. Reproduce the bug manually. Starting from RF, click RT (a request arrives), then BT (the arbiter correctly goes Busy), then RT again. The monitor should flag a violation on that last click—this is exactly the counterexample \(\textsf{RF} \to \textsf{RT} \to \textsf{BT} \to \textsf{RT}\) from the chapter (ex:arbiter-safety-ce).
  2. Switch to the fixed model and try to reproduce the same violation from BT. You can’t—BT’s only legal successors are BF and BT itself, so a pending request can never be silently dropped.
  3. Try an existential query by hand. Can you reach BF from RF without ever passing through a state with request = TRUE? (Yes—RF → BF directly, in one click, in either model.) That is the same shape of question as \(\mathbf{EF}(\texttt{state}=\textsc{Busy} \land \neg\texttt{request})\) from the chapter’s existential-model-checking example, and here you can find the witness yourself.

[!TIP] Read the full chapter in the PDF

For the formal definitions (Kripke structures, safety vs. liveness, counterexamples, SMV syntax) that this notebook operationalizes, see Chapter 7 of the lecture notes.

Download the Full Lecture Notes (PDF)