Table of contents for Principles of model checking / Christel Baier Joost-Pieter Katoen ; foreword by Kim Guldstrand Larsen.

Bibliographic record and links to related information available from the Library of Congress catalog.

Note: Contents data are machine generated based on pre-publication provided by the publisher. Contents may have variations from the printed book or be incomplete or contain other coding.


Counter
Contents
Foreword i
Preface iii
Contents viii
1 System Veri_cation 3
1.1 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.2 Characteristics of Model Checking . . . . . . . . . . . . . . . . . 12
1.2.1 The Model Checking Process . . . . . . . . . . . . . . . . 13
1.2.2 Strengths and Weaknesses . . . . . . . . . . . . . . . . . . 16
1.3 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2 Modelling Concurrent Systems 21
2.1 Transition Systems . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.1.1 Executions . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.1.2 Modeling Hard- and Software Systems . . . . . . . . . . . 28
2.2 Parallelism and Communication . . . . . . . . . . . . . . . . . . . 36
2.2.1 Concurrency and Interleaving . . . . . . . . . . . . . . . . 37
ix
x CONTENTS
2.2.2 Communication via Shared Variables . . . . . . . . . . . . 41
2.2.3 Handshaking . . . . . . . . . . . . . . . . . . . . . . . . . 48
2.2.4 Channel Systems . . . . . . . . . . . . . . . . . . . . . . . 53
2.2.5 NanoPromela . . . . . . . . . . . . . . . . . . . . . . . . . 63
2.2.6 Synchronous Parallelism . . . . . . . . . . . . . . . . . . . 74
2.3 The State-Space Explosion Problem . . . . . . . . . . . . . . . . 76
2.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
2.5 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . 80
2.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
3 Linear-Time Properties 87
3.1 Deadlock . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
3.2 Linear Time Behavior . . . . . . . . . . . . . . . . . . . . . . . . 92
3.2.1 Paths and State Graph . . . . . . . . . . . . . . . . . . . 92
3.2.2 Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
3.2.3 Linear-Time Properties . . . . . . . . . . . . . . . . . . . 97
3.2.4 Trace Equivalence and Linear-Time Properties . . . . . . 100
3.3 Safety Properties and Invariants . . . . . . . . . . . . . . . . . . 103
3.3.1 Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
3.3.2 Safety Properties . . . . . . . . . . . . . . . . . . . . . . . 107
3.3.3 Trace Equivalence and Safety Properties . . . . . . . . . . 111
3.4 Liveness Properties . . . . . . . . . . . . . . . . . . . . . . . . . . 116
3.4.1 Liveness Properties . . . . . . . . . . . . . . . . . . . . . . 116
3.4.2 Safety Versus Liveness Properties . . . . . . . . . . . . . . 118
CONTENTS xi
3.5 Fairness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
3.5.1 Fairness Constraints . . . . . . . . . . . . . . . . . . . . . 124
3.5.2 Fairness Strategies . . . . . . . . . . . . . . . . . . . . . . 131
3.5.3 Fairness and Safety . . . . . . . . . . . . . . . . . . . . . . 134
3.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136
3.7 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . 137
3.8 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
4 Regular Properties 145
4.1 Automata on Finite Words . . . . . . . . . . . . . . . . . . . . . 145
4.2 Model Checking Regular Safety Properties . . . . . . . . . . . . . 152
4.2.1 Regular Safety Properties . . . . . . . . . . . . . . . . . . 153
4.2.2 Verifying Regular Safety Properties . . . . . . . . . . . . . 157
4.3 Automata on In_nite Words . . . . . . . . . . . . . . . . . . . . . 163
4.3.1 !-Regular Languages and Properties . . . . . . . . . . . . 164
4.3.2 Nondeterministic Buchi Automata . . . . . . . . . . . . . 167
4.3.3 Deterministic Buchi Automata . . . . . . . . . . . . . . . 180
4.3.4 Generalized Buchi automata . . . . . . . . . . . . . . . . 184
4.4 Model Checking !-Regular Properties . . . . . . . . . . . . . . . 190
4.4.1 Persistence Properties and Product . . . . . . . . . . . . . 191
4.4.2 Nested Depth-First Search . . . . . . . . . . . . . . . . . . 196
4.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208
4.6 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . 209
4.7 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211
xii CONTENTS
5 Linear Temporal Logic 219
5.1 Linear Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . 219
5.1.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221
5.1.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 225
5.1.3 Specifying Properties . . . . . . . . . . . . . . . . . . . . . 228
5.1.4 Equivalence of LTL Formulae . . . . . . . . . . . . . . . . 237
5.1.5 Weak Until, Release and Positive Normal Form . . . . . . 241
5.1.6 Fairness in LTL . . . . . . . . . . . . . . . . . . . . . . . . 246
5.2 Automata-Based LTL Model Checking . . . . . . . . . . . . . . . 258
5.2.1 Complexity of the LTL Model-Checking Problem . . . . . 273
5.2.2 LTL Satis_ability and Validity Checking . . . . . . . . . . 282
5.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 284
5.4 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . 285
5.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 286
6 Computation Tree Logic 295
6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 295
6.2 Computation Tree Logic . . . . . . . . . . . . . . . . . . . . . . . 298
6.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 299
6.2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 301
6.2.3 Equivalence of CTL Formulae . . . . . . . . . . . . . . . . 310
6.2.4 Normal Forms for CTL . . . . . . . . . . . . . . . . . . . 312
6.3 Expressiveness of CTL versus LTL . . . . . . . . . . . . . . . . . 314
6.4 CTL Model Checking . . . . . . . . . . . . . . . . . . . . . . . . 320
CONTENTS xiii
6.4.1 Basic Algorithm . . . . . . . . . . . . . . . . . . . . . . . 321
6.4.2 The Until and Existential Globally Operator . . . . . . . 326
6.4.3 Time and Space Complexity . . . . . . . . . . . . . . . . . 333
6.5 Fairness in CTL . . . . . . . . . . . . . . . . . . . . . . . . . . . 336
6.6 Counterexamples and Witnesses . . . . . . . . . . . . . . . . . . 350
6.6.1 Counterexamples in CTL . . . . . . . . . . . . . . . . . . 352
6.6.2 Counterexamples and Witnesses in CTL with Fairness . . 356
6.7 Symbolic CTL Model Checking . . . . . . . . . . . . . . . . . . . 358
6.7.1 Switching Functions . . . . . . . . . . . . . . . . . . . . . 359
6.7.2 Encoding Transition Systems by Switching Functions . . . 363
6.7.3 Ordered Binary Decision Diagrams . . . . . . . . . . . . . 368
6.8 CTL_ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 396
6.8.1 Logic, Expressiveness and Equivalence . . . . . . . . . . . 397
6.8.2 CTL_ Model Checking . . . . . . . . . . . . . . . . . . . . 401
6.9 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 404
6.10 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . 405
6.11 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 407
7 Equivalences and Abstraction 421
7.1 Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 423
7.1.1 Bisimulation Quotient . . . . . . . . . . . . . . . . . . . . 428
7.1.2 Action-based Bisimulation . . . . . . . . . . . . . . . . . . 436
7.2 Bisimulation and CTL_-equivalence . . . . . . . . . . . . . . . . . 438
7.3 Bisimulation Quotienting Algorithms . . . . . . . . . . . . . . . . 446
xiv CONTENTS
7.3.1 Determining the Initial Partition . . . . . . . . . . . . . . 448
7.3.2 Re_ning Partitions . . . . . . . . . . . . . . . . . . . . . . 450
7.3.3 A First Partition-Re_nement Algorithm . . . . . . . . . . 456
7.3.4 An E_ciency Improvement . . . . . . . . . . . . . . . . . 457
7.3.5 Equivalence Checking of Transition Systems . . . . . . . . 462
7.4 Simulation Relations . . . . . . . . . . . . . . . . . . . . . . . . . 465
7.4.1 Simulation Equivalence . . . . . . . . . . . . . . . . . . . 473
7.4.2 Bisimulation, Simulation and Trace Equivalence . . . . . 478
7.5 Simulation and 8CTL_ Equivalence . . . . . . . . . . . . . . . . . 483
7.6 Simulation Quotienting Algorithms . . . . . . . . . . . . . . . . . 488
7.7 Stutter Linear-Time Relations . . . . . . . . . . . . . . . . . . . . 494
7.7.1 Stutter Trace Equivalence . . . . . . . . . . . . . . . . . . 496
7.7.2 Stutter Trace and LTLn Equivalence . . . . . . . . . . . 499
7.8 Stutter Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . 501
7.8.1 Divergence-Sensitive Stutter Bisimulation . . . . . . . . . 508
7.8.2 Normed Bisimulation . . . . . . . . . . . . . . . . . . . . . 516
7.8.3 Stutter Bisimulation and CTL_n Equivalence . . . . . . . 524
7.8.4 Stutter Bisimulation Quotienting . . . . . . . . . . . . . . 531
7.9 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 542
7.10 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . 543
7.11 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 545
8 Partial Order Reduction 557
8.1 Independence of Actions . . . . . . . . . . . . . . . . . . . . . . . 559
CONTENTS xv
8.2 The Linear-Time Ample Set Approach . . . . . . . . . . . . . . . 567
8.2.1 Ample Set Constraints . . . . . . . . . . . . . . . . . . . . 568
8.2.2 Dynamic Partial Order Reduction . . . . . . . . . . . . . 580
8.2.3 Computing Ample Sets . . . . . . . . . . . . . . . . . . . 585
8.2.4 Static Partial Order Reduction . . . . . . . . . . . . . . . 595
8.3 The Branching-Time Ample Set Approach . . . . . . . . . . . . . 608
8.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 619
8.5 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . 619
8.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 621
9 Timed Automata 629
9.1 Timed Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . 633
9.1.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 640
9.1.2 Time Divergence, Timelock, and Zenoness . . . . . . . . . 645
9.2 Timed Computation Tree Logic . . . . . . . . . . . . . . . . . . . 653
9.3 TCTL Model Checking . . . . . . . . . . . . . . . . . . . . . . . . 659
9.3.1 Eliminating Timing Parameters . . . . . . . . . . . . . . . 660
9.3.2 Region Transition Systems . . . . . . . . . . . . . . . . . 663
9.3.3 The TCTL Model-Checking Algorithm . . . . . . . . . . . 685
9.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 690
9.5 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . 691
9.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 692
10 Probabilistic Systems 697
xvi CONTENTS
10.1 Markov Chains . . . . . . . . . . . . . . . . . . . . . . . . . . . . 699
10.1.1 Reachability Probabilities . . . . . . . . . . . . . . . . . . 710
10.1.2 Qualitative Properties . . . . . . . . . . . . . . . . . . . . 721
10.2 Probabilistic Computation Tree Logic . . . . . . . . . . . . . . . 730
10.2.1 PCTL Model Checking . . . . . . . . . . . . . . . . . . . 735
10.2.2 The Qualitative Fragment of PCTL . . . . . . . . . . . . 737
10.3 Linear Time Properties . . . . . . . . . . . . . . . . . . . . . . . 745
10.4 PCTL_ and Probabilistic Bisimulation . . . . . . . . . . . . . . . 755
10.4.1 PCTL_ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 755
10.4.2 Probabilistic Bisimulation . . . . . . . . . . . . . . . . . . 757
10.5 Markov Chains with Costs . . . . . . . . . . . . . . . . . . . . . . 765
10.5.1 Cost-Bounded Reachability . . . . . . . . . . . . . . . . . 766
10.5.2 Long-Run Properties . . . . . . . . . . . . . . . . . . . . . 775
10.6 Markov Decision Processes . . . . . . . . . . . . . . . . . . . . . . 780
10.6.1 Reachability Probabilities . . . . . . . . . . . . . . . . . . 797
10.6.2 PCTL Model Checking . . . . . . . . . . . . . . . . . . . 811
10.6.3 Limiting Properties . . . . . . . . . . . . . . . . . . . . . 814
10.6.4 Linear Time Properties and PCTL_ . . . . . . . . . . . . 825
10.6.5 Fairness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 828
10.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 839
10.8 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . 840
10.9 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 843
A Preliminaries 853
CONTENTS 1
A.1 Frequently used Symbols and Notations . . . . . . . . . . . . . . 853
A.2 Formal Languages . . . . . . . . . . . . . . . . . . . . . . . . . . 856
A.3 Propositional Logic . . . . . . . . . . . . . . . . . . . . . . . . . . 858
A.4 Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 863
A.5 Computational Complexity . . . . . . . . . . . . . . . . . . . . . 868
References 874
Index 907

Library of Congress Subject Headings for this publication:

Computer systems -- Verification.
Computer software -- Verification.