Puzzles for learning real-time model checking

摘要

This paper describes the utility of using puzzles to teach formal methods and real-time model checking. Puzzles allow us to teach model checking via finite games. The limitations of model checkers and the challenge of limiting the size of the state space are evident as students try to solve problems of varying size and difficulty. Students gain valuable practical experience in constructing models for puzzles before moving on to industry-sized problems.