Model checking is an automated technique such that given a finite state model of a system and a formal property (expressed in temporal logic), then it systematically checks whether the property is true of false in a given state in the model.
- 1.E.M. Clarke, E.A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, in Logic of Programs: Work-Shop, Yorktown Heights, NY, May 1981, vol. 131 of LNCS (Springer, 1981)Google Scholar
- 2.C. Baier, J. Pieter Katoen, Principles of Model Checking (MIT Press, Cambridge, 2008)Google Scholar