%PDF-1.4 % 3 0 obj << /pgfprgb [/Pattern /DeviceRGB] >> endobj 16 0 obj << /S /GoTo /D (Outline0.1) >> endobj 19 0 obj (Motivation) endobj 20 0 obj << /S /GoTo /D (Outline0.2) >> endobj 23 0 obj (Differential Dynamic Logic ) endobj 24 0 obj << /S /GoTo /D (Outline0.2.1.18) >> endobj 27 0 obj (Design Motives) endobj 28 0 obj << /S /GoTo /D (Outline0.2.2.32) >> endobj 31 0 obj (Syntax) endobj 32 0 obj << /S /GoTo /D (Outline0.2.3.37) >> endobj 35 0 obj (Semantics) endobj 36 0 obj << /S /GoTo /D (Outline0.3) >> endobj 39 0 obj (Verification Calculus for Differential Dynamic Logic ) endobj 40 0 obj << /S /GoTo /D (Outline0.3.1.57) >> endobj 43 0 obj (Compositional Verification Calculus) endobj 44 0 obj << /S /GoTo /D (Outline0.3.2.64) >> endobj 47 0 obj (Deduction Modulo by Side Deduction) endobj 48 0 obj << /S /GoTo /D (Outline0.3.3.71) >> endobj 51 0 obj (Deduction Modulo with Free Variables \046 Skolemization) endobj 52 0 obj << /S /GoTo /D (Outline0.3.4.83) >> endobj 55 0 obj (Soundness and Completeness) endobj 56 0 obj << /S /GoTo /D (Outline0.4) >> endobj 59 0 obj (Survey) endobj 60 0 obj << /S /GoTo /D (Outline0.5) >> endobj 63 0 obj (Conclusions \046 Future Work) endobj 64 0 obj << /S /GoTo /D (Outline1) >> endobj 67 0 obj (Appendix) endobj 68 0 obj << /S /GoTo /D (Outline1.6) >> endobj 71 0 obj (Background Material) endobj 72 0 obj << /S /GoTo /D (Outline1.6.1.95) >> endobj 75 0 obj (Formal Semantics) endobj 76 0 obj << /S /GoTo /D (Outline1.6.2.99) >> endobj 79 0 obj (Soundness Proof) endobj 80 0 obj << /S /GoTo /D (Outline1.6.3.101) >> endobj 83 0 obj (Completeness Proof) endobj 84 0 obj << /S /GoTo /D (Outline1.7) >> endobj 87 0 obj (Differential Algebraic Dynamic Logic ) endobj 88 0 obj << /S /GoTo /D (Outline1.7.1.126) >> endobj 91 0 obj (Air Traffic Control) endobj 92 0 obj << /S /GoTo /D (Outline1.7.2.133) >> endobj 95 0 obj () endobj 96 0 obj << /S /GoTo /D (Outline1.7.3.137) >> endobj 99 0 obj () endobj 100 0 obj << /S /GoTo /D (Outline1.8) >> endobj 103 0 obj (Computing Differential Invariants as Fixedpoints) endobj 104 0 obj << /S /GoTo /D (Outline1.8.1.159) >> endobj 107 0 obj (Derivations and Differentiation) endobj 108 0 obj << /S /GoTo /D (Outline1.9) >> endobj 111 0 obj (Differential Temporal Dynamic Logic ) endobj 112 0 obj << /S /GoTo /D (Outline1.9.1.179) >> endobj 115 0 obj (Motivation) endobj 116 0 obj << /S /GoTo /D (Outline1.9.2.181) >> endobj 119 0 obj (Compositional Verification Calculus) endobj 120 0 obj << /S /GoTo /D (Outline1.10) >> endobj 123 0 obj (Deduction Modulo Real Algebraic and Computer Algebraic Constraints) endobj 124 0 obj << /S /GoTo /D (Outline1.11) >> endobj 127 0 obj (Parametric European Train Control System) endobj 128 0 obj << /S /GoTo /D (Outline1.12) >> endobj 131 0 obj (Collision Avoidance Maneuvers in Air Traffic Control) endobj 132 0 obj << /S /GoTo /D (Outline1.13) >> endobj 135 0 obj (Hybrid Automata Embedding) endobj 136 0 obj << /S /GoTo /D [137 0 R /Fit ] >> endobj 152 0 obj << /Length 1121 /Filter /FlateDecode >> stream xWo6_G(Y6a@= VR$|'7$wDDX@)ْ lnpxGeƑǹ(Ӽ+%)@3=R3A9&_#P8~48^hD8 "RD*^y :T:XycGqH6#(IODM&礧U`.3h~7p۟*A֘1ytFڸ G|XA?IX Hؗhv$}tz968ĦFIIQ"g^`,$NB^It$>76RҡCh'*5}PÚkfENUN9=Vi^Yt̙ܗOp.,fԴ.Cccf9;rg{ٍQQ̏U#.{ s>QkΙϙȘ54^96fb[`~#Tkk