Modal and Temporal Properties of Processes

Front Cover
Springer Science & Business Media, Jul 6, 2001 - Technology & Engineering - 191 pages
In recent years, model checking has become an essential technique for the formal verification of systems. With a clarity of presentation and its many illuminating examples, this book makes this technical material easy to grasp. It is perfectly suited for an advanced undergraduate or graduate class in formal verification and will serve as a valuable resource to practitioners of formal methods.
 

What people are saying - Write a review

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

Contents

Processes
1
12 Concurrent interaction
8
13 Observable transitions
17
14 Renaming and linking
21
15 More combinations of processes
25
16 Sets of processes
28
Modalities and Capabilities
31
21 HennessyMilner logic I
32
46 Duality
100
Modal MuCalculus
103
51 Modal logic with fixed points
104
52 Macros and normal formulas
107
53 Observable modal logic with fixed points
110
54 Preservation of bisimulation equivalence
112
55 Approximants
115
56 Embedded approximants
121

22 HennessyMilner logic II
36
23 Algebraic structure and modal properties
39
24 Observable modal logic
42
25 Observable necessity and divergence
47
Bisimulations
51
32 Interactive games
56
33 Bisimulation relations
64
34 Modal properties and equivalences
69
35 Observable bisimulations
72
36 Equivalence checking
77
Temporal Properties
83
42 Processes and their runs
85
43 The temporal logic CTL
89
44 Modal formulas with variables
91
45 Modal equations and fixed points
95
57 Expressing properties
128
Verifying Temporal Properties
133
62 Property checking games
135
63 Correctness of games
144
64 CTL games
147
65 Parity games
151
66 Deciding parity games
156
Exposing Structure
163
71 Infinite state systems
164
72 Generalising satisfaction
165
73 Tableaux I
168
74 Tableaux II
173
References
183
Index
187
Copyright

Other editions - View all

Common terms and phrases