Temporal logic and state systems

Temporal logic has developed over the last 30 years into a powerful formal setting for the specification and verification of state-based systems. Based on university lectures given by the authors, this book is a comprehensive, concise, uniform, up-to-date presentation of the theory and applications of linear and branching time temporal logic; TLA (Temporal Logic of Actions); automata theoretical connections; model checking; and related theories.

All theoretical details and numerous application examples are elaborated carefully and with full formal rigor, and the book will serve as a basic source and reference for lecturers, graduate students and researchers.

Preface	p. V
1 Basic Concepts and Notions of Logics	p. 1
1.1 Logical Languages, Semantics, and Formal Systems	p. 1
1.2 Classical First-Order Logic	p. 7
1.3 Theories and Models	p. 11
1.4 Extensions of Logics	p. 15
Bibliographical Notes	p. 17
2 Basic Propositional Linear Temporal Logic	p. 19
2.1 The Basic Language and Its Normal Semantics	p. 19
2.2 Temporal Logical Laws	p. 26
2.3 Axiomatization	p. 33
2.4 Completeness	p. 40
2.5 Decidability	p. 50
2.6 Initial Validity Semantics	p. 58
Bibliographical Notes	p. 63
3 Extensions of LTL	p. 65
3.1 Binary Temporal Operators	p. 65
3.2 Fixpoint Operators	p. 73
3.3 Propositional Quantification	p. 83
3.4 Past Operators	p. 88
3.5 Syntactic Anchoring	p. 92
3.6 Combinations of Extensions	p. 95
Bibliographical Notes	p. 98
4 Expressiveness of Propositional Linear Temporal Logics	p. 101
4.1 LTL and Its Extensions	p. 101
4.2 Temporal Logic and Classical First-Order Logic	p. 110
4.3 Non-deterministic w-Automata	p. 118
4.4 LTL and Buchi Automata	p. 130
4.5 Weak Alternating Automata	p. 144
Bibliographical Notes	p. 151
5 First-Order Linear Temporal Logic	p. 153
5.1 Basic Language and Semantics	p. 153
5.2 A Formal System	p. 160
5.3 Incompleteness	p. 162
5.4 Primed Individual Constants	p. 168
5.5 Well-Founded Relations	p. 173
5.6 Flexible Quantification	p. 176
Bibliographical Notes	p. 179
6 State Systems	p. 181
6.1 Temporal Theories and Models	p. 181
6.2 State Transition Systems	p. 187
6.3 Rooted Transition Systems	p. 195
6.4 Labeled Transition Systems	p. 198
6.5 Fairness	p. 207
Bibliographical Notes	p. 212
7 Verification of State Systems	p. 213
7.1 System Properties	p. 213
7.2 Invariance Properties	p. 220
7.3 Precedence Properties	p. 226
7.4 Eventuality Properties	p. 229
7.5 A Self-stabilizing Network	p. 239
7.6 The Alternating Bit Protocol	p. 248
Bibliographical Notes	p. 255
8 Verification of Concurrent Programs	p. 257
8.1 Programs as State Transition Systems	p. 257
8.2 Shared-Variables Programs	p. 261
8.3 Program Properties	p. 269
8.4 A Mutual Exclusion Program	p. 281
8.5 Message Passing Programs	p. 288
8.6 A Producer-Consumer Program	p. 296
Bibliographical Notes	p. 302
9 Structured Specification	p. 303
9.1 Refinement and Stuttering Invariance	p. 303
9.2 Basic TLA	p. 308
9.3 Generalized TLA	p. 314
9.4 System Verification with GTLA	p. 323
9.5 Hiding of Internal System Variables	p. 327
9.6 Composition of System Components	p. 332
Bibliographical Notes	p. 337
10 Other Temporal Logics	p. 339
10.1 Further Modifications of Linear Temporal Logic	p. 339
10.2 Interval Temporal Logics	p. 347
10.3 Branching Time Temporal Logics	p. 352
10.4 The Logics CTL and CTL*	p. 359
10.5 Temporal Logics for True Concurrency Modeling	p. 368
Bibliographical Notes	p. 373
11 System Verification by Model Checking	p. 375
11.1 Finite State Systems	p. 375
11.2 LTL Model Checking	p. 381
11.3 CTL Model Checking	p. 386
11.4 Fairness Constraints	p. 394
11.5 Symbolic CTL Model Checking	p. 397
11.6 Further Model Checking Techniques	p. 405
Bibliographical Notes	p. 411
List of Temporal Logical Laws	p. 413
References	p. 421
Index	p. 429

Available:*

On Order

Summary

Summary

Table of Contents