%PDF-1.4 13 0 obj << /S /GoTo /D (Outline1) >> endobj 16 0 obj (Motivation) endobj 17 0 obj << /S /GoTo /D (Outline2) >> endobj 20 0 obj (Temporal Dynamic Logic ) endobj 21 0 obj << /S /GoTo /D (Outline2.1.16) >> endobj 24 0 obj (Syntax) endobj 25 0 obj << /S /GoTo /D (Outline2.2.20) >> endobj 28 0 obj (Trace Semantics) endobj 29 0 obj << /S /GoTo /D (Outline2.3.38) >> endobj 32 0 obj (Conservative Extension) endobj 33 0 obj << /S /GoTo /D (Outline2.4.40) >> endobj 36 0 obj (Safety Invariants in Train Control) endobj 37 0 obj << /S /GoTo /D (Outline3) >> endobj 40 0 obj (Verification Calculus for ) endobj 41 0 obj << /S /GoTo /D (Outline3.1.41) >> endobj 44 0 obj (Sequent Calculus) endobj 45 0 obj << /S /GoTo /D (Outline3.2.48) >> endobj 48 0 obj (Verifying Safety Invariants in Train Control) endobj 49 0 obj << /S /GoTo /D (Outline3.3.52) >> endobj 52 0 obj (Soundness) endobj 53 0 obj << /S /GoTo /D (Outline4) >> endobj 56 0 obj (Conclusions \046 Future Work) endobj 57 0 obj << /S /GoTo /D [58 0 R /Fit ] >> endobj 67 0 obj << /Length 1554 /Filter /FlateDecode >> stream xXIoFW̭2/)5EĶERX#+ _pAz9o[(8~<&,MW-l|!Jbʇxi͙JFf1R3vDw-$Kmnl(- .*taxG1CvYsG<`>yء\pwSQilFSsst4Ac ްoDls]p XC`BT$c$*H~.$&QRPӔ6TIg&mpE5bm((rZIB`2oyPny>7_$""Ng!^C}EaV7Fz=%Ӫm:Y}l+:L|N4̋ve@*%䩍W?wO ~ذ2CWy[0*Wg~*\ɘfc>y?nB JvM|,>oTNMILр`CTx+^tpqu魅c+P<7$\{^i(\UX&s%T(Od/F6fQ.}v?v$;zz(+YN j5Or&FG{̅+>mf9-E2#=,?%E7l_Fʃ(#Yy"К-+s|.^ڤlЄ;j2h^Oϟ\v2aJen"x`@*N)pG(TM%18Gl$y; %[jR<N`d,TyќG6`uJõڎ:(ʃa:<.QP<EyKg`_6g#:K2d*rl/W_-UciDi+bK]fnAfh2-bΒWogwq <>d 7Ӥk=-]Jp(gm)~>~$F_//T$Ap*SP"seI7(^A=q愇3Z09@i 3(oH_|HHrg-ʅhN}Ј)Q)4/&x#'=MV>rӪp4Vԗ<: QdI?*(4zR*ݖ'$I#|Y{}<p)ѕGӠ c1<6L>S+2ĚǖJ@ t.V*B@Ϧ6L/F[t}.`ڀ^9t0f x1";?CE\;*i*4$ޕ5zZ*`,FiĘp"O3EEw4EaMR2`=+zn-'c?#XG?!zG3MqTVQ ,: ! ma{͆:I_DAOWvZwendstream endobj 58 0 obj << /Type /Page /Contents 67 0 R /Resources 66 0 R /MediaBox [0 0 362.8347 272.1261] /Trans << /S /R >> /Parent 84 0 R /Annots [ 81 0 R ] >> endobj 9 0 obj << /R 22050 /Length 8 /Filter /FlateDecode >> stream x endstream endobj 60 0 obj << /Type /XObject /Subtype /Form /BBox [0 0 8 8] /FormType 1 /Matrix [1 0 0 1 0 0] /Resources 85 0 R /Length 15 /Filter /FlateDecode >> stream xP( endstream endobj 85 0 obj << /Shading << /Sh << /ShadingType 3 /ColorSpace /DeviceRGB /Domain [0 1] /Coords [4.00005 4.00005 0.0 4.00005 4.00005 4.00005] /Function << /FunctionType 2 /Domain [0 1] /C0 [0.5 0.5 0.5] /C1 [1 1 1] /N 1 >> /Extend [true false] >> >> /ProcSet [ /PDF ] >> endobj 61 0 obj << /Type /XObject /Subtype /Form /BBox [0 0 16 16] /FormType 1 /Matrix [1 0 0 1 0 0] /Resources 86 0 R /Length 15 /Filter /FlateDecode >> stream xP( endstream endobj 86 0 obj << /Shading << /Sh << /ShadingType 3 /ColorSpace /DeviceRGB /Domain [0.0 8.00009] /Coords [8.00009 8.00009 0.0 8.00009 8.00009 8.00009] /Function << /FunctionType 3 /Domain [0.0 8.00009] /Functions [ << /FunctionType 2 /Domain [0.0 8.00009] /C0 [0.5 0.5 0.5] /C1 [0.5 0.5 0.5] /N 1 >> << /FunctionType 2 /Domain [0.0 8.00009] /C0 [0.5 0.5 0.5] /C1 [1 1 1] /N 1 >> ] /Bounds [ 4.00005] /Encode [0 1 0 1] >> /Extend [true false] >> >> /ProcSet [ /PDF ] >> endobj 59 0 obj << /Type /XObject /Subtype /Form /BBox [0 0 850.3937 8] /FormType 1 /Matrix [1 0 0 1 0 0] /Resources 87 0 R /Length 15 /Filter /FlateDecode >> stream xP( endstream endobj 87 0 obj << /Shading << /Sh << /ShadingType 2 /ColorSpace /DeviceRGB /Domain [0.0 8.00009] /Coords [0 0.0 0 8.00009] /Function << /FunctionType 3 /Domain [0.0 8.00009] /Functions [ << /FunctionType 2 /Domain [0.0 8.00009] /C0 [1 1 1] /C1 [0.5 0.5 0.5] /N 1 >> << /FunctionType 2 /Domain [0.0 8.00009] /C0 [0.5 0.5 0.5] /C1 [0.5 0.5 0.5] /N 1 >> ] /Bounds [ 4.00005] /Encode [0 1 0 1] >> /Extend [false false] >> >> /ProcSet [ /PDF ] >> endobj 62 0 obj << /Interpolate false /Type /XObject /Subtype /Form /FormType 1 /PTEX.FileName (./images/cmu-logo.pdf) /PTEX.PageNumber 1 /PTEX.InfoDict 88 0 R /Matrix [1.00000000 0.00000000 0.00000000 1.00000000 0.00000000 0.00000000] /BBox [0.00000000 0.00000000 553.00000000 83.00000000] /Resources << /ProcSet [ /PDF ] /ExtGState << /R7 89 0 R >>>> /Length 90 0 R /Filter /FlateDecode >> stream xm[n-9rE53tM=6a0г^;JBW)BdwlR::gcWX|Ԏ+q^,Kt=9^eyNQZ N^GȽrJG㕻o#yψq̯C{8B/G+TQzynI{ʟq^K[=8QVHG5ռ45k~S-sGsGs|nNX:`jə-æF;҉rz,q2jC_894#W$Ѵ J\L般ܜ/qj"]Rg/&tI.IinP! u>CԀ!]=Qv1Ko 2H]2Z!̌ $͘HҬhS^I:bcmr($MKMMkF 4cs:U:䐺$Wa1dtȾFh'K,xk/$n*C^+rQDSJXNծxͧ6Y_mVpY2%oK|Њ6mNKWoJ>Fy8Sۑd9f+Ϗ}9(G"(mǐ&鲸x!ɟyl!)4ѴED,8P#PΈtx$mve?E.Y愽8%ܰLYX#H'Nҽ\DkuPƐ5/τsZI]1R ^M&S*hУMCL#)sԇj$D,}ۢq.jk:4nNLXt@I/OK/Z2^F$wS6zys,z##L2 GrV|M??f@$VrgwXO;|~