Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
There will be several versions of product automata throughout the book, e.g., controlled Büchi product automaton, controlled Rabin product automaton, controlled finite state product automaton. We will have formal definitions for all these product automata. However, whenever possible, we will call them simply product automata in the text, as their meaning will be clear from the context.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Belta, C., Yordanov, B., Aydin Gol, E. (2017). Model Checking. In: Formal Methods for Discrete-Time Dynamical Systems. Studies in Systems, Decision and Control, vol 89. Springer, Cham. https://doi.org/10.1007/978-3-319-50763-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-50763-7_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-50762-0
Online ISBN: 978-3-319-50763-7
eBook Packages: EngineeringEngineering (R0)