Logical Analysis of Hybrid Systems (eBook)

The author is an assistant professor in the Computer Science Department at Carnegie Mellon University. He has an M.Sc. in computer science from the University of Karlsruhe, Germany and a Ph.D. in computer science from the University of Oldenburg, Germany. Among other awards he won best paper awards at the Tableaux 2007 and FM 2009 conferences, he was among Popular Science Magazine's annual "Brilliant 10" in 2009, he received the ACM Doctoral Dissertation Honorable Mention Award in 2009, he was among the IEEE Intelligent Systems' biennial "AI's 10 to Watch" in 2011, and he received an NSF Career award in 2011. His research interests include the logical foundations of cyberphysical systems, theorem proving and model checking. 

Foreword 4
Preface 5
Contents 12
List of Figures 18
List of Tables 23
List of Theorems 24
Chapter 1 Introduction 26
1.1 Technical Context 29
1.1.1 Hybrid Systems 29
1.1.2 Model Checking 37
1.1.3 Deductive Verification 39
1.1.4 Compositional Verification 41
1.1.5 Lifting Quantifier Elimination 44
1.1.6 Differential Induction and Differential Strengthening 45
1.2 Related Work 46
1.3 Contributions 50
1.4 Structure of This Book 50
Part I Logics and Proof Calculi for Hybrid Systems 55
Chapter 2 Differential Dynamic Logic dL 57
2.1 Introduction 58
2.1.1 Structure of This Chapter 59
2.2 Syntax of Differential Dynamic Logic 59
2.2.1 Terms 61
2.2.2 Hybrid Programs 65
2.2.3 Formulas of Differential Dynamic Logic 71
2.3 Semantics of Differential Dynamic Logic 73
2.3.1 Valuation of Terms 74
2.3.2 Valuation of Formulas 75
2.3.3 Transition Semantics of Hybrid Programs 78
2.4 Collision Avoidance in Train Control 85
2.5 Free-Variable Proof Calculus for Differential Dynamic Logic 88
2.5.1 Substitution 89
2.5.2 Rules of the Calculus for Differential Dynamic Logic 100
2.5.3 Deduction Modulo with Invertible Quantifiers and Real Quantifier Elimination 112
2.5.3.1 Lifting Quantifier Elimination by Invertible Quantifier Rules 112
2.5.3.2 Admissibility in Invertible Quantifier Rules 115
2.5.3.3 Quantifier Elimination and Modalities 117
2.5.3.4 Global Invertible Quantifier Rules 117
2.5.4 Verification Example 118
2.6 Soundness 121
2.7 Completeness 125
2.7.1 Incompleteness 126
2.7.2 Relative Completeness 127
2.7.3 Characterising Real G¨odel Encodings 129
2.7.4 Expressibility and Rendition of Hybrid Program Semantics 130
2.7.5 Relative Completeness of First-Order Assertions 133
2.7.6 Relative Completeness of the Differential Logic Calculus 137
2.8 Relatively Semidecidable Fragments 138
2.9 Train Control Verification 142
2.9.1 Finding Inductive Candidates 142
2.9.2 Inductive Verification 143
2.9.3 Parameter Constraint Discovery 144
2.10 Summary 146
Chapter 3 Differential-Algebraic Dynamic Logic DAL 147
3.1 Introduction 148
3.1.1 Related Work 152
3.1.2 Structure of This Chapter 154
3.2 Syntax of Differential-Algebraic Logic 154
3.2.1 Terms 156
3.2.2 Differential-Algebraic Programs 156
3.2.3 Formulas of Differential-Algebraic Logic 163
3.3 Semantics of Differential-Algebraic Logic 165
3.3.1 Transition Semantics of Differential-Algebraic Programs 165
3.3.2 Valuation of Formulas 169
3.3.3 Time Anomalies 169
3.3.4 Conservative Extension 171
3.4 Collision Avoidance in Air Traffic Control 172
3.4.1 Flight Dynamics 172
3.4.2 Differential Axiomatisation 173
3.4.3 Aircraft Collision Avoidance Manoeuvres 174
3.4.4 Tangential Roundabout Manoeuvre 175
3.5 Proof Calculus for Differential-Algebraic Logic 176
3.5.1 Motivation 177
3.5.2 Derivations and Differentiation 178
3.5.3 Differential Reduction and Differential Elimination 184
3.5.4 Rules of the Calculus for Differential-Algebraic Logic 186
3.5.5 Deduction Modulo by Side Deduction 192
3.5.6 Differential Induction with Differential Invariants 194
3.5.7 Differential Induction with Differential Variants 205
3.6 Soundness 209
3.7 Restricting Differential Invariants 212
3.8 Differential Monotonicity Relaxations 213
3.9 Relative Completeness 217
3.10 Deductive Strength of Differential Induction 218
3.11 Air Traffic Control Verification 221
3.11.1 Characterisation of Safe Roundabout Dynamics 221
3.11.2 Tangential Entry Procedures 224
3.11.3 Discussion 225
3.12 Summary 225
Chapter 4 Differential Temporal Dynamic Logic dTL 227
4.1 Introduction 228
4.1.1 Related Work 229
4.1.2 Structure of This Chapter 230
4.2 Syntax of Temporal Dynamic Logic for Hybrid Systems 230
4.2.1 Hybrid Programs 231
4.2.2 State and Trace Formulas 231
4.3 Semantics of Temporal Dynamic Logic for Hybrid Systems 234
4.3.1 Trace Semantics of Hybrid Programs 234
4.3.2 Valuation of State and Trace Formulas 237
4.3.3 Conservative Temporal Extension 239
4.4 Safety Invariants in Train Control 240
4.5 Proof Calculus for Temporal Invariants 241
4.5.1 Proof Rules 242
4.5.2 Verification Example 245
4.6 Soundness 245
4.7 Completeness 247
4.7.1 Incompleteness 247
4.7.2 Relative Completeness 248
4.7.3 Expressibility and Rendition of Hybrid Trace Semantics 249
4.7.4 Modular Relative Completeness Proof for the Differential Temporal Dynamic Logic Calculus 250
4.8 Verification of Train Control Safety Invariants 251
4.9 Liveness by Quantifier Alternation 252
4.10 Summary 254
Part II Automated Theorem Proving for Hybrid Systems 255
Chapter 5 Deduction Modulo Real Algebra and Computer Algebra 257
5.1 Introduction 258
5.1.1 Related Work 258
5.1.2 Structure of This Chapter 259
5.2 Tableau Procedures Modulo 259
5.3 Nondeterminisms in Tableau Modulo 262
5.3.1 Nondeterminisms in Branch Selection 262
5.3.2 Nondeterminisms in Formula Selection 263
5.3.3 Nondeterminisms in Mode Selection 264
5.4 Iterative Background Closure 267
5.5 Iterative Inflation 270
5.6 Experimental Results 272
5.7 Summary 275
Chapter 6 Computing Differential Invariants as Fixed Points 277
6.1 Introduction 278
6.1.1 Related Work 279
6.1.2 Structure of This Chapter 280
6.2 Inductive Verification by Combining Local Fixed Points 280
6.2.1 Verification by Symbolic Decomposition 281
6.2.2 Discrete and Differential Induction, Differential Invariants 282
6.2.3 Flight Dynamics in Air Traffic Control 284
6.2.4 Local Fixed-Point Computation for Differential Invariants 286
6.2.5 Dependency-Directed Induction Candidates 287
6.2.6 Global Fixed-Point Computation for Loop Invariants 289
6.2.7 Interplay of Local and Global Fixed-Point Loops 292
6.3 Soundness 293
6.4 Optimisations 295
6.4.1 Sound Interleaving with Numerical Simulation 295
6.4.2 Optimisations for the Verification Algorithm 296
6.5 Experimental Results 296
6.6 Summary 297
Part III Case Studies and Applications in Hybrid Systems Verification 299
Chapter 7 European Train Control System 301
7.1 Introduction 302
7.1.1 Related Work 304
7.1.2 Structure of This Chapter 305
7.2 Parametric European Train Control System 305
7.2.1 Overview of the ETCS Cooperation Protocol 305
7.2.2 Formal Model of Fully Parametric ETCS 308
7.3 Parametric Verification of Train Control 310
7.3.1 Controllability Discovery in Parametric ETCS 311
7.3.2 Iterative Control Refinement of ETCS Parameters 312
7.3.3 Safety Verification of Refined ETCS 315
7.3.4 Liveness Verification of Refined ETCS 317
7.4 Disturbance and the European Train Control System 319
7.4.1 Controllability in ETCS with Disturbances 320
7.4.2 Iterative Control Refinement of Parameters with Disturbances 322
7.4.3 Safety Verification of ETCS with Disturbances 322
7.5 Experimental Results 323
7.6 Summary 325
Chapter 8 Air Traffic Collision Avoidance 326
8.1 Introduction 327
8.1.1 Related Work 330
8.1.2 Structure of This Chapter 331
8.2 Curved Flight in Roundabout Manoeuvres 332
8.2.1 Flight Dynamics 332
8.2.2 Roundabout Manoeuvre Overview 333
8.2.3 Compositional Verification Plan 334
8.2.4 Tangential Roundabout Manoeuvre Cycles (AC1) 335
8.2.5 Bounded Control Choices (AC2) 338
8.2.6 Flyable Entry Procedures (AC3) 338
8.2.7 Bounded Entry Duration (AC4) 341
8.2.8 Safe Entry Separation (AC5) 342
8.3 Synchronisation of Roundabout Manoeuvres 345
8.3.1 Successful Negotiation (AC6) 345
8.3.2 Safe Exit Separation (AC7) 349
8.4 Compositional Verification 351
8.5 Flyable Tangential Roundabout Manoeuvre 352
8.6 Experimental Results 354
8.7 Summary 356
Chapter 9 Conclusion 358
Part IV Appendix 362
Appendix A First-Order Logic and Theorem Proving 364
A.1 Overview 364
A.2 Syntax of First-Order Logic 369
A.2.1 Terms 369
A.2.2 First-Order Formulas 370
A.3 Semantics of First-Order Logic 371
A.3.1 Valuation of Terms 372
A.3.2 Valuation of First-Order Formulas 372
A.4 A Sequent Proof Calculus for First-Order Logic 373
A.4.1 Proof Rules for First-Order Logic 374
A.4.2 Proof Example: Ground Proving Versus Free-Variable Proving 377
A.5 Soundness 379
A.6 Completeness 379
A.7 Computability Theory and Decidability 380
Appendix B Differential Equations 381
B.1 Ordinary Differential Equations 381
B.2 Existence Theorems 385
B.3 Existence and Uniqueness Theorems 386
B.4 Linear Differential Equations with Constant Coefficients 387
Appendix C Hybrid Automata 390
C.1 Syntax and Traces of Hybrid Automata 390
C.2 Embedding Hybrid Automata into Hybrid Programs 392
Appendix D KeYmaera Implementation 397
D.1 KeYmaera: A Hybrid Theorem Prover for Hybrid Systems 397
D.1.1 Structure of This Appendix 399
D.2 Computational Back-ends for Real Arithmetic 400
D.2.1 Real-Closed Fields 401
D.2.2 Semialgebraic Geometry and Cylindrical Algebraic Decomposition 403
D.2.3 Nullstellensatz and Gr¨obner Bases 406
D.2.4 Real Nullstellensatz 412
D.2.5 Positivstellensatz and Semidefinite Programming 414
D.3 Discussion 416
D.4 Performance Measurements 419
References 421
Index 434
Operators and Proof Rules 442