Temporal Logic and State Systems

Front Cover
Springer Science & Business Media, Mar 27, 2008 - Computers - 436 pages

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.

 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Basic Concepts and Notions of Logics
1
12 Classical FirstOrder Logic
7
13 Theories and Models
11
14 Extensions of Logics
15
Bibliographical Notes
17
Basic Propositional Linear Temporal Logic
18
22 Temporal Logical Laws
26
23 Axiomatization
33
Verification of State Systems
213
72 Invariance Properties
220
73 Precedence Properties
226
74 Eventuality Properties
229
75 A Selfstabilizing Network
239
76 The Alternative Bit Protocol
248
Bibliographical Notes
255
Verification of Concurrent Programs
257

24 Completeness
40
25 Decidability
50
26 Initial Validity Semantics
58
Bibliographical Notes
63
Extensions of LTL
65
32 Fixpoint Operators
73
33 Propositional Quantification
83
34 Past Operators
88
35 Syntactic Anchoring
92
36 Combinations of Extensions
95
Bibliographical Notes
98
Expressiveness of Propositional Linear Temporal Logics
101
42 Temporal Logic and Classical FirstOrder Logic
110
43 Nondeterministic ωAutomata
118
44 LTL and Büchi Automata
130
45 Weak Alternating Automata
144
Bibliographical Notes
151
FirstOrder Linear Temporal Logic
153
52 A Formal System
160
53 Incompleteness
162
54 Primed Individual Constants
168
55 WellFounded Relations
173
56 Flexible Quantification
176
Bibliographical Notes
179
State Systems
180
62 State Transition Systems
187
63 Rooted Transition Systems
195
64 Labeled Transition Systems
198
65 Fairness
207
Bibliographical Notes
212
82 SharedVariables Programs
261
83 Program Properties
269
84 A Mutual Exclusion Program
281
85 Message Passing Programs
288
86 A ProducerConsumer Program
296
Bibliographical Notes
302
Structured Specification
303
92 Basic TLA
308
93 Generalized TLA
314
94 System Verification with GTLA
323
95 Hiding of Internal System Variables
327
96 Composition of System Components
332
Bibliographical Notes
337
Other Temporal Logics
339
102 Interval Temporal Logics
347
103 Branching Time Temporal Logics
352
104 The Logics CTL and CTL
359
105 Temporal Logics for True Concurrency Modeling
368
Bibliographical Notes
373
System Verification by Model Checking
374
112 LTL Model Checking
381
113 CTL Model Checking
386
114 Fairness Constraints
394
115 Symbolic CTL Model Checking
397
116 Further Model Checking Techniques
405
Bibliographical Notes
411
List of Temporal Logical Laws
413
References
421
Index
429
Copyright

Other editions - View all

Common terms and phrases

Popular passages

Page 423 - Self-Stabilizing Systems in Spite of Distributed Control," Communications of the ACM 17, 1974, pp.
Page 423 - Concurrency Verification: Introduction to Compositional and Noncompositional Methods, Cambridge University Press, Cambridge.
Page 423 - Emerson, EA, Sistla, AP: Symmetry and Model Checking, Formal Methods in System Design, 9, 1995, 105-131.

Bibliographic information