Model checking
Does a temporal logic formula hold for a finite state machine?
- If not, find counterexample
Temporal logic
- until, eventually, always, etc.
For many logics, checking can be done in linear time in the size of the space state
- Explicit model checking does this, exploiting symmetries for performance