Verification of finite state systems with temporal logic model checking
Loading...
Authors
Schlingloff, B
Issue Date
1997
Type
Article
Language
en
Keywords
Computer aided verification , Finite state systems , Temporal logic , Model checking , Modal logic , Expressivity , Expressiveness , w-languages , Buchi-Automata , Completeness , Decision procedures , Tableaus , Specification , Binary decision diagrams (BDDs) , Partial order methods , Stubborn sets
Alternative Title
Abstract
These tutorial notes contain an introduction to the logical theory and computational aspects of computer aided verification of finite state reactive systems with linear and branching temporal logic model checking. As a general recipe, computer science applications and algorithms are derived from logical notions and proofs. First, the expressivity of various temporal logics is compared to first and second order logic, and to w-automata and formal languages. Then, temporal safety and liveness properties are reviewed. From the completeness proof for natural and tree models, local and global decision procedures are developed. These in turn give rise to the corresponding model checking procedures. Various modelling techniques for reactive systems are presented. Finally, symbolic techniques for global model checking with binary decision diagrams, and partial order techniques for local model checking with stubborn sets are discussed.
Description
Citation
Schlingloff B (1997) Verification of finite state systems with temporal logic model checking. South African Computer Journal, Number 19, 1997
Publisher
South African Computer Society (SAICSIT)
License
Journal
Volume
Issue
PubMed ID
DOI
ISSN
2313-7835