# Model checking

Explore the states actually reachable from an initial condition, and evaluate safety on that closure.

## Definitions

- **Reachability**: The least set containing all initial states and closed under transitions.
- **Safety invariant**: A predicate true at every reachable state.
- **Unreachable state**: A declared state that no allowed execution from an initial state reaches.

## Acceptance procedure

1. Initialize the frontier with every initial state.
2. Follow all transitions, deduplicating visited states.
3. Compare the supplied reachable-state certificate with the computed closure.
4. Check whether every reachable state lies in the declared safe set.

## Complexity

Breadth-first exploration is O(V+E) for an explicit finite graph; implicit system state spaces can grow exponentially.

## Common failure

Ignoring an enabled transition can make an unsafe system appear safe.

## Extensions

Add counterexample paths, temporal properties, and fairness-aware liveness checks.

## Instances

- KL-FCS-008: A reachable-state safety invariant — Safety invariant holds: yes
- KL-FCS-020: A reachable unsafe state — Safety invariant holds: no
- KL-FCS-021: Branching safety closure — Safety invariant holds: yes

## References

- https://www.prismmodelchecker.org/doc/whatsinprism.php