Slides from Will Marrero's Introduction to Model Checking

How is model checking done?

A simple state machine and specification

State machine augmented with state variables

Specification given by a state machine

An example that does not satisfy its specification