Model Checking — State Space Exploration and Counterexamples

In this tutorial, you'll learn about Model Checking. We cover key concepts, practical examples, and best practices to help you understand and apply this topic effectively.

Model Checking automatically verifies whether a finite-state system satisfies a given temporal logic property by exhaustively exploring all reachable states.

Learning Path

flowchart LR
  A["Temporal Logic"] --> B["Model Checking
State Space Exploration"]
  B --> C["Bounded Model Checking"]
  B --> D["Symbolic Execution"]
  style B fill:#f90,color:#fff,stroke-width:2px

Prerequisites

Temporal logic (LTL/CTL). Basic graph theory and state machines.

What Is Model Checking?

Model Checking takes three inputs: a model of the system (finite-state transition system), a specification (temporal logic formula), and verifies that the model satisfies the specification. If verification fails, it produces a counterexample trace.

Step-by-Step: Building a Kripke Structure

Step 1: Define States and Transitions

A Kripke structure has states labeled with atomic propositions and a transition relation.

class Kripke:
    def __init__(self, states, init, transitions, labeling):
        self.states = states
        self.init = init
        self.transitions = transitions
        self.labeling = labeling  # state -> set of props

    def reachable_states(self):
        visited = set()
        stack = [self.init]
        while stack:
            s = stack.pop()
            if s in visited:
                continue
            visited.add(s)
            for t in self.transitions.get(s, []):
                if t not in visited:
                    stack.append(t)
        return visited

states = {"s1", "s2", "s3"}
transitions = {"s1": ["s2"], "s2": ["s1", "s3"], "s3": ["s3"]}
labeling = {"s1": {"ready"}, "s2": {"busy"}, "s3": {"done"}}
k = Kripke(states, "s1", transitions, labeling)
print(f"Reachable: {k.reachable_states()}")

Expected output:

Reachable: {'s1', 's2', 's3'}

Step 2: Label with Atomic Propositions

Each state gets a set of propositions true in that state. In our example, s1 has ready, s2 has busy, s3 has done.

Step 3: Model Check a Property

Check AG (ready → AF done): from any reachable state, if ready holds, eventually done holds along all paths.

def check_AG_AF(kripke, p, q):
    for s in kripke.reachable_states():
        if p in kripke.labeling[s]:
            if not check_AF(kripke, s, q, set()):
                return False, s
    return True, None

def check_AF(kripke, state, q, visited):
    if q in kripke.labeling[state]:
        return True
    if state in visited:
        return False
    visited.add(state)
    succ = kripke.transitions.get(state, [])
    return all(check_AF(kripke, s, q, visited.copy())
              for s in succ)

result, bad_state = check_AG_AF(k, "ready", "done")
print(f"Property holds: {result}")

Expected output:

Property holds: True

BDD-Based Symbolic Model Checking

Instead of enumerating states explicitly, Binary Decision Diagrams (BDDs) represent sets of states compactly.

class SimpleBDD:
    def __init__(self, var_count):
        self.var_count = var_count

    def encode_state(self, bits):
        return sum(b << i for i, b in enumerate(bits))

states_set = set()
for bits in [(0,0), (0,1), (1,0), (1,1)]:
    states_set.add(SimpleBDD(2).encode_state(bits))

print(f"Encoded states: {states_set}")

Expected output:

Encoded states: {0, 1, 2, 3}

Counterexample Analysis

When Model Checking fails, the counterexample is a path from initial state to a violating state.

def find_counterexample(kripke, bad_states):
    visited = set()
    queue = [(kripke.init, [kripke.init])]
    while queue:
        s, path = queue.pop(0)
        if s in visited:
            continue
        visited.add(s)
        if s in bad_states:
            return path
        for t in kripke.transitions.get(s, []):
            if t not in visited:
                queue.append((t, path + [t]))
    return None

bad = {"s3"}
trace = find_counterexample(k, bad)
print(f"Counterexample trace: {trace}")

Expected output:

Counterexample trace: ['s1', 's2', 's3']

Common Errors

1. State Explosion

Models with 50+ boolean variables produce 2^50 states, far too many for explicit enumeration. Use symbolic methods or abstraction.

2. Incomplete Transition Relation

Missing transitions cause the model checker to assume no progress is possible, which may produce false positives.

3. Wrong Initial State

Verifying from the wrong initial state gives meaningless results. The property may hold elsewhere but fail from the intended start.

4. Ignoring Deadlock States

A state with no outgoing transitions may satisfy properties vacuously but represents a system failure.

5. Over-abstracting the Model

Removing too much detail may hide real bugs. The verified model and the implementation may diverge.

Practice Questions

Q1: What is a Kripke structure?

A graph where nodes represent states labeled with atomic propositions and edges represent transitions.

Q2: What does a counterexample look like in CTL Model Checking?

A finite or infinite path from the initial state showing why the property fails.

Q3: Why are BDDs used in symbolic Model Checking?

BDDs represent sets of states compactly, often exponentially smaller than explicit enumeration.

Q4: What is the difference between explicit and symbolic Model Checking?

Explicit stores states individually; symbolic stores sets of states using formulas or BDDs.

Q5: Can Model Checking handle infinite-state systems?

Not directly. Infinite-state systems require abstraction, bounded Model Checking, or Theorem Proving.

Challenge

Model a simple vending machine that accepts coins and dispenses items. Define 4 states (idle, coin_inserted, item_selected, dispensing). Specify in CTL that every coin insertion eventually leads to dispensing. Implement Model Checking in Python and verify.

FAQ

Built by the developers of Doda Browser, DodaZIP, and Durga Antivirus Pro.