Model Checking

  • Calin BeltaEmail author
  • Boyan Yordanov
  • Ebru Aydin Gol
Part of the Studies in Systems, Decision and Control book series (SSDC, volume 89)


In this chapter, we introduce model checking, which is the most basic analysis problem in formal verification. As the focus of the book is on LTL, we restrict our attention to LTL specifications. Since we focus on analysis, we consider transition systems with no inputs. Informally, the LTL model checking problem consists of determining whether the language originating at a state of a finite transition system satisfies an LTL formula over its set of observations. The algorithms presented in this chapter will be extended in subsequent chapters to solve more difficult problems, such as finding the largest satisfying region for finite transition systems and infinite transition systems embedding discrete-time dynamical systems.

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Mechanical Engineering, Electrical and Computer Engineering, and Systems EngineeringBoston UniversityBostonUSA
  2. 2.Biological Computation GroupMicrosoft Research LtdCambridgeUK
  3. 3.Department of Computer EngineeringMiddle East Technical UniversityCankayaTurkey

Personalised recommendations