The origin of the term "model checking" and the idea itself is succinctly described in the Q&A with Clarke, Emerson, and Sifakis in the July 2008 CACM. If a program can be specified in temporal logic, then it can be realized as a finite state program --- a program with just a finite number of different configurations. This suggested the idea of model checking --- to check whether a finite state graph is a model of a temporal logic specifications. This Q&A was based on a preliminary interview with a journalist, followed by many rounds of polishing and revising by the three Turing Award winners and the editor until we were all satisfied. In other words, model checking derives from the Finite Model Property used in my program synthesis work. A more detailed explanation is given in [Emerson, "The Beginning of Model Checking", 25MC].