Model-Checking überprüft zeitliche Eigenschaften sequentieller Schaltungen. Das Anwendungsgebiet von Model-Checking-Verfahren ist vielfältig und reicht von der Software-Verifikation und der Verifikation von Übertragungs- Protokollen bis hin zur Überprüfung von digitalen Systemen. Entsprechend vielseitig sind auch die verwendeten Ansätze und Algorithmen. Die Grundlagen für das Model-Checking kommen aus der Informatik, wo die Verfahren zur Verifikation von Software genutzt werden. Die hier vorgestellten Algorithmen beziehen sich jedoch ausschließlich auf die Verifikation digitaler Systeme.
Beim Model-Checking werden einzelne Eigenschaften eines Systems untersucht. Dies setzt voraus, dass solche Eigenschaften in einer formalen Sprache beschrieben werden können. Je nach Art der Eigenschaft werden verschiedene Anforderungen an eine solche Sprache und damit auch an die Überprüfungsalgorithmen gestellt.