We survey principles of model checking techniques for the automatic analysis of reactive systems. The use of model checking is exemplified by an analysis of the Needham-Schroeder public key protocol. We then formally define transition systems, temporal logic, ω-automata, and their relationship. Basic model checking algorithms for linear- and branching-time temporal logics are defined, followed by an introduction to symbolic model checking and partial-order reduction techniques. The paper ends with a list of references to some more advanced topics.
CITATION STYLE
Merz, S. (2001). Model Checking: A Tutorial Overview (pp. 3–38). https://doi.org/10.1007/3-540-45510-8_1
Mendeley helps you to discover research relevant for your work.