Platzer Logical Analysis of Hybrid Systems

Proving Theorems for Complex Dynamics
1. Auflage 2010
ISBN: 978-3-642-14509-4
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 426 Seiten

Hybrid systems are models for complex physical systems and have become a widely used concept for understanding their behavior. Many applications are safety-critical, including car, railway, and air traffic control, robotics, physical-chemical process control, and biomedical devices. Hybrid systems analysis studies how we can build computerized controllers for physical systems which are guaranteed to meet their design goals. The author gives a unique, logic-based perspective on hybrid systems analysis. It is the first book that leverages the power of logic for hybrid systems. The author develops a coherent logical approach for systematic hybrid systems analysis, covering its theory, practice, and applications. It is further shown how the developed verification techniques can be used to study air traffic and railway control systems. This book is intended for researchers, postgraduates, and professionals who are interested in hybrid systems analysis, cyberphysical or embedded systems design, logic and theorem proving, or transportation and automation.

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. 

Autoren/Hrsg.

Platzer, André

Inhaltsverzeichnis

1;Foreword;4
2;Preface;5
3;Contents;12
4;List of Figures;18
5;List of Tables;23
6;List of Theorems;24
7;Chapter 1 Introduction;26
7.1;1.1 Technical Context;29
7.1.1;1.1.1 Hybrid Systems;29
7.1.2;1.1.2 Model Checking;37
7.1.3;1.1.3 Deductive Verification;39
7.1.4;1.1.4 Compositional Verification;41
7.1.5;1.1.5 Lifting Quantifier Elimination;44
7.1.6;1.1.6 Differential Induction and Differential Strengthening;45
7.2;1.2 Related Work;46
7.3;1.3 Contributions;50
7.4;1.4 Structure of This Book;50
8;Part I Logics and Proof Calculi for Hybrid Systems;55
8.1;Chapter 2 Differential Dynamic Logic dL;57
8.1.1;2.1 Introduction;58
8.1.1.1;2.1.1 Structure of This Chapter;59
8.1.2;2.2 Syntax of Differential Dynamic Logic;59
8.1.2.1;2.2.1 Terms;61
8.1.2.2;2.2.2 Hybrid Programs;65
8.1.2.3;2.2.3 Formulas of Differential Dynamic Logic;71
8.1.3;2.3 Semantics of Differential Dynamic Logic;73
8.1.3.1;2.3.1 Valuation of Terms;74
8.1.3.2;2.3.2 Valuation of Formulas;75
8.1.3.3;2.3.3 Transition Semantics of Hybrid Programs;78
8.1.4;2.4 Collision Avoidance in Train Control;85
8.1.5;2.5 Free-Variable Proof Calculus for Differential Dynamic Logic;88
8.1.5.1;2.5.1 Substitution;89
8.1.5.2;2.5.2 Rules of the Calculus for Differential Dynamic Logic;100
8.1.5.3;2.5.3 Deduction Modulo with Invertible Quantifiers and Real Quantifier Elimination;112
8.1.5.3.1;2.5.3.1 Lifting Quantifier Elimination by Invertible Quantifier Rules;112
8.1.5.3.2;2.5.3.2 Admissibility in Invertible Quantifier Rules;115
8.1.5.3.3;2.5.3.3 Quantifier Elimination and Modalities;117
8.1.5.3.4;2.5.3.4 Global Invertible Quantifier Rules;117
8.1.5.4;2.5.4 Verification Example;118
8.1.6;2.6 Soundness;121
8.1.7;2.7 Completeness;125
8.1.7.1;2.7.1 Incompleteness;126
8.1.7.2;2.7.2 Relative Completeness;127
8.1.7.3;2.7.3 Characterising Real G¨odel Encodings;129
8.1.7.4;2.7.4 Expressibility and Rendition of Hybrid Program Semantics;130
8.1.7.5;2.7.5 Relative Completeness of First-Order Assertions;133
8.1.7.6;2.7.6 Relative Completeness of the Differential Logic Calculus;137
8.1.8;2.8 Relatively Semidecidable Fragments;138
8.1.9;2.9 Train Control Verification;142
8.1.9.1;2.9.1 Finding Inductive Candidates;142
8.1.9.2;2.9.2 Inductive Verification;143
8.1.9.3;2.9.3 Parameter Constraint Discovery;144
8.1.10;2.10 Summary;146
8.2;Chapter 3 Differential-Algebraic Dynamic Logic DAL;147
8.2.1;3.1 Introduction;148
8.2.1.1;3.1.1 Related Work;152
8.2.1.2;3.1.2 Structure of This Chapter;154
8.2.2;3.2 Syntax of Differential-Algebraic Logic;154
8.2.2.1;3.2.1 Terms;156
8.2.2.2;3.2.2 Differential-Algebraic Programs;156
8.2.2.3;3.2.3 Formulas of Differential-Algebraic Logic;163
8.2.3;3.3 Semantics of Differential-Algebraic Logic;165
8.2.3.1;3.3.1 Transition Semantics of Differential-Algebraic Programs;165
8.2.3.2;3.3.2 Valuation of Formulas;169
8.2.3.3;3.3.3 Time Anomalies;169
8.2.3.4;3.3.4 Conservative Extension;171
8.2.4;3.4 Collision Avoidance in Air Traffic Control;172
8.2.4.1;3.4.1 Flight Dynamics;172
8.2.4.2;3.4.2 Differential Axiomatisation;173
8.2.4.3;3.4.3 Aircraft Collision Avoidance Manoeuvres;174
8.2.4.4;3.4.4 Tangential Roundabout Manoeuvre;175
8.2.5;3.5 Proof Calculus for Differential-Algebraic Logic;176
8.2.5.1;3.5.1 Motivation;177
8.2.5.2;3.5.2 Derivations and Differentiation;178
8.2.5.3;3.5.3 Differential Reduction and Differential Elimination;184
8.2.5.4;3.5.4 Rules of the Calculus for Differential-Algebraic Logic;186
8.2.5.5;3.5.5 Deduction Modulo by Side Deduction;192
8.2.5.6;3.5.6 Differential Induction with Differential Invariants;194
8.2.5.7;3.5.7 Differential Induction with Differential Variants;205
8.2.6;3.6 Soundness;209
8.2.7;3.7 Restricting Differential Invariants;212
8.2.8;3.8 Differential Monotonicity Relaxations;213
8.2.9;3.9 Relative Completeness;217
8.2.10;3.10 Deductive Strength of Differential Induction;218
8.2.11;3.11 Air Traffic Control Verification;221
8.2.11.1;3.11.1 Characterisation of Safe Roundabout Dynamics;221
8.2.11.2;3.11.2 Tangential Entry Procedures;224
8.2.11.3;3.11.3 Discussion;225
8.2.12;3.12 Summary;225
8.3;Chapter 4 Differential Temporal Dynamic Logic dTL;227
8.3.1;4.1 Introduction;228
8.3.1.1;4.1.1 Related Work;229
8.3.1.2;4.1.2 Structure of This Chapter;230
8.3.2;4.2 Syntax of Temporal Dynamic Logic for Hybrid Systems;230
8.3.2.1;4.2.1 Hybrid Programs;231
8.3.2.2;4.2.2 State and Trace Formulas;231
8.3.3;4.3 Semantics of Temporal Dynamic Logic for Hybrid Systems;234
8.3.3.1;4.3.1 Trace Semantics of Hybrid Programs;234
8.3.3.2;4.3.2 Valuation of State and Trace Formulas;237
8.3.3.3;4.3.3 Conservative Temporal Extension;239
8.3.4;4.4 Safety Invariants in Train Control;240
8.3.5;4.5 Proof Calculus for Temporal Invariants;241
8.3.5.1;4.5.1 Proof Rules;242
8.3.5.2;4.5.2 Verification Example;245
8.3.6;4.6 Soundness;245
8.3.7;4.7 Completeness;247
8.3.7.1;4.7.1 Incompleteness;247
8.3.7.2;4.7.2 Relative Completeness;248
8.3.7.3;4.7.3 Expressibility and Rendition of Hybrid Trace Semantics;249
8.3.7.4;4.7.4 Modular Relative Completeness Proof for the Differential Temporal Dynamic Logic Calculus;250
8.3.8;4.8 Verification of Train Control Safety Invariants;251
8.3.9;4.9 Liveness by Quantifier Alternation;252
8.3.10;4.10 Summary;254
9;Part II Automated Theorem Proving for Hybrid Systems;255
9.1;Chapter 5 Deduction Modulo Real Algebra and Computer Algebra;257
9.1.1;5.1 Introduction;258
9.1.1.1;5.1.1 Related Work;258
9.1.1.2;5.1.2 Structure of This Chapter;259
9.1.2;5.2 Tableau Procedures Modulo;259
9.1.3;5.3 Nondeterminisms in Tableau Modulo;262
9.1.3.1;5.3.1 Nondeterminisms in Branch Selection;262
9.1.3.2;5.3.2 Nondeterminisms in Formula Selection;263
9.1.3.3;5.3.3 Nondeterminisms in Mode Selection;264
9.1.4;5.4 Iterative Background Closure;267
9.1.5;5.5 Iterative Inflation;270
9.1.6;5.6 Experimental Results;272
9.1.7;5.7 Summary;275
9.2;Chapter 6 Computing Differential Invariants as Fixed Points;277
9.2.1;6.1 Introduction;278
9.2.1.1;6.1.1 Related Work;279
9.2.1.2;6.1.2 Structure of This Chapter;280
9.2.2;6.2 Inductive Verification by Combining Local Fixed Points;280
9.2.2.1;6.2.1 Verification by Symbolic Decomposition;281
9.2.2.2;6.2.2 Discrete and Differential Induction, Differential Invariants;282
9.2.2.3;6.2.3 Flight Dynamics in Air Traffic Control;284
9.2.2.4;6.2.4 Local Fixed-Point Computation for Differential Invariants;286
9.2.2.5;6.2.5 Dependency-Directed Induction Candidates;287
9.2.2.6;6.2.6 Global Fixed-Point Computation for Loop Invariants;289
9.2.2.7;6.2.7 Interplay of Local and Global Fixed-Point Loops;292
9.2.3;6.3 Soundness;293
9.2.4;6.4 Optimisations;295
9.2.4.1;6.4.1 Sound Interleaving with Numerical Simulation;295
9.2.4.2;6.4.2 Optimisations for the Verification Algorithm;296
9.2.5;6.5 Experimental Results;296
9.2.6;6.6 Summary;297
10;Part III Case Studies and Applications in Hybrid Systems Verification;299
10.1;Chapter 7 European Train Control System;301
10.1.1;7.1 Introduction;302
10.1.1.1;7.1.1 Related Work;304
10.1.1.2;7.1.2 Structure of This Chapter;305
10.1.2;7.2 Parametric European Train Control System;305
10.1.2.1;7.2.1 Overview of the ETCS Cooperation Protocol;305
10.1.2.2;7.2.2 Formal Model of Fully Parametric ETCS;308
10.1.3;7.3 Parametric Verification of Train Control;310
10.1.3.1;7.3.1 Controllability Discovery in Parametric ETCS;311
10.1.3.2;7.3.2 Iterative Control Refinement of ETCS Parameters;312
10.1.3.3;7.3.3 Safety Verification of Refined ETCS;315
10.1.3.4;7.3.4 Liveness Verification of Refined ETCS;317
10.1.4;7.4 Disturbance and the European Train Control System;319
10.1.4.1;7.4.1 Controllability in ETCS with Disturbances;320
10.1.4.2;7.4.2 Iterative Control Refinement of Parameters with Disturbances;322
10.1.4.3;7.4.3 Safety Verification of ETCS with Disturbances;322
10.1.5;7.5 Experimental Results;323
10.1.6;7.6 Summary;325
10.2;Chapter 8 Air Traffic Collision Avoidance;326
10.2.1;8.1 Introduction;327
10.2.1.1;8.1.1 Related Work;330
10.2.1.2;8.1.2 Structure of This Chapter;331
10.2.2;8.2 Curved Flight in Roundabout Manoeuvres;332
10.2.2.1;8.2.1 Flight Dynamics;332
10.2.2.2;8.2.2 Roundabout Manoeuvre Overview;333
10.2.2.3;8.2.3 Compositional Verification Plan;334
10.2.2.4;8.2.4 Tangential Roundabout Manoeuvre Cycles (AC1);335
10.2.2.5;8.2.5 Bounded Control Choices (AC2);338
10.2.2.6;8.2.6 Flyable Entry Procedures (AC3);338
10.2.2.7;8.2.7 Bounded Entry Duration (AC4);341
10.2.2.8;8.2.8 Safe Entry Separation (AC5);342
10.2.3;8.3 Synchronisation of Roundabout Manoeuvres;345
10.2.3.1;8.3.1 Successful Negotiation (AC6);345
10.2.3.2;8.3.2 Safe Exit Separation (AC7);349
10.2.4;8.4 Compositional Verification;351
10.2.5;8.5 Flyable Tangential Roundabout Manoeuvre;352
10.2.6;8.6 Experimental Results;354
10.2.7;8.7 Summary;356
10.3;Chapter 9 Conclusion;358
11;Part IV Appendix;362
11.1;Appendix A First-Order Logic and Theorem Proving;364
11.1.1;A.1 Overview;364
11.1.2;A.2 Syntax of First-Order Logic;369
11.1.2.1;A.2.1 Terms;369
11.1.2.2;A.2.2 First-Order Formulas;370
11.1.3;A.3 Semantics of First-Order Logic;371
11.1.3.1;A.3.1 Valuation of Terms;372
11.1.3.2;A.3.2 Valuation of First-Order Formulas;372
11.1.4;A.4 A Sequent Proof Calculus for First-Order Logic;373
11.1.4.1;A.4.1 Proof Rules for First-Order Logic;374
11.1.4.2;A.4.2 Proof Example: Ground Proving Versus Free-Variable Proving;377
11.1.5;A.5 Soundness;379
11.1.6;A.6 Completeness;379
11.1.7;A.7 Computability Theory and Decidability;380
11.2;Appendix B Differential Equations;381
11.2.1;B.1 Ordinary Differential Equations;381
11.2.2;B.2 Existence Theorems;385
11.2.3;B.3 Existence and Uniqueness Theorems;386
11.2.4;B.4 Linear Differential Equations with Constant Coefficients;387
11.3;Appendix C Hybrid Automata;390
11.3.1;C.1 Syntax and Traces of Hybrid Automata;390
11.3.2;C.2 Embedding Hybrid Automata into Hybrid Programs;392
11.4;Appendix D KeYmaera Implementation;397
11.4.1;D.1 KeYmaera: A Hybrid Theorem Prover for Hybrid Systems;397
11.4.1.1;D.1.1 Structure of This Appendix;399
11.4.2;D.2 Computational Back-ends for Real Arithmetic;400
11.4.2.1;D.2.1 Real-Closed Fields;401
11.4.2.2;D.2.2 Semialgebraic Geometry and Cylindrical Algebraic Decomposition;403
11.4.2.3;D.2.3 Nullstellensatz and Gr¨obner Bases;406
11.4.2.4;D.2.4 Real Nullstellensatz;412
11.4.2.5;D.2.5 Positivstellensatz and Semidefinite Programming;414
11.4.3;D.3 Discussion;416
11.4.4;D.4 Performance Measurements;419
12;References;421
13;Index;434
14;Operators and Proof Rules;442