Notebook 6: Reachability Fixpoint & Decision Problems

Interactive notebook on computing reachable states via a least-fixpoint algorithm and exploring decision problems for finite automata. From the Verification and Validation Techniques course at UniUD.

Reachability Fixpoint & Decision Problems

This notebook walks through the reachability fixpoint algorithm for deciding language emptiness, and then shows how universality, inclusion, and equivalence all reduce to emptiness checks.

Running example – DFA that accepts words containing “aaa”:

  • States: \(q_0, q_1, q_2, q_3\)
  • \(\delta(q_0,a)=q_1,\; \delta(q_0,b)=q_0,\; \delta(q_1,a)=q_2,\; \delta(q_1,b)=q_0,\; \delta(q_2,a)=q_3,\; \delta(q_2,b)=q_0,\; \delta(q_3,a)=q_3,\; \delta(q_3,b)=q_3\)
  • \(F = \{q_3\}\)

Widget 1: Reachability Fixpoint Iteration

Click Step → to advance the fixpoint computation one iteration at a time.

Iteration 0 / 5

DFA — "contains aaa"

a a a b b b a,b q₀ q₁ q₂ q₃

Iteration Table

i Rᵢ Post(Rᵢ) New

Widget 2: Decision Problem Reductions

All standard decision problems for regular languages reduce to emptiness. Click the tabs below to see each reduction in action.

Step 0 / 4

Complement DFA — swap accepting states

a a a b b b a,b q₀ q₁ q₂ q₃

Reduction summary

Step 0 / 4

Setup

Reduction summary

Step 0 / 4

Two inclusion checks

Reduction summary

What To Notice

  1. The fixpoint converges in at most |Q| iterations. Here we have 4 states, and the fixpoint is reached in exactly 4 steps (iterations 0 through 3 discover one new state each; iteration 4 confirms the fixpoint). In general \(R_i \subseteq R_{i+1} \subseteq Q\), so the chain stabilises after at most \(|Q|\) steps.

  2. The iteration discovers states in BFS order from \(q_0\). \(R_0 = \{q_0\}\), then \(q_1\) appears at distance 1, \(q_2\) at distance 2, \(q_3\) at distance 3 – exactly the breadth-first layers of the transition graph. The iteration counter \(i\) at which a state first appears equals its shortest-path distance from \(q_0\), which is why the shortest witness for non-emptiness has length 3.

  3. All decision problems reduce to emptiness via closure constructions. Universality uses complementation, inclusion uses product with complement, equivalence uses two inclusion checks. The only “engine” is \(L(\mathcal{A}) \stackrel{?}{=} \varnothing\), which is reachability.

  4. Emptiness itself is just graph reachability. The fixpoint iteration \(R_{i+1} = R_i \cup \mathrm{Post}(R_i)\) is a standard BFS on the state graph. This is the fundamental algorithm underlying model checking: verify a property by exploring the reachable state space and checking whether any “bad” (or “accepting”) state is reachable.