%PDF-1.4
%
3 0 obj
<< /pgfprgb [/Pattern /DeviceRGB] >>
endobj
8 0 obj
<< /S /GoTo /D (Outline0.1) >>
endobj
11 0 obj
(Introduction)
endobj
12 0 obj
<< /S /GoTo /D (Outline0.2) >>
endobj
15 0 obj
(Model checking safety properties)
endobj
16 0 obj
<< /S /GoTo /D (Outline0.3) >>
endobj
19 0 obj
(Results)
endobj
20 0 obj
<< /S /GoTo /D (Outline0.4) >>
endobj
23 0 obj
(Conclusions)
endobj
24 0 obj
<< /S /GoTo /D [25 0 R /Fit ] >>
endobj
47 0 obj <<
/Length 855
/Filter /FlateDecode
>>
stream
xWKO1Wq#5V%=DAU}vl$j)P
DHR fdBBˎӳI`y>/e`0&8AN
}!)Ah5vaOH5 bP[Vsph)A:eJX?ljPmd\@G"C") *Gc4t[&܊Ywn5pƠ<1oFqj`~p\{4vZO;eNcgK;'$[8*wLYNttS): AI2JjTzM\HSQY 3BIdUsDeD(c4Sy
݇7qWnG8uB5T^w[k)cۛNH3n"iV>/jORrzw,8-vI_cC>u%6JVو dܽ|yGՍHD%^NY2Y*(Z1Q߈mp$*>/#afwM}gA[̜( Y
9>9\F4KVxhqv;]Rm"ڗ*˪JR;[CvMo(omi/c3a1b1/]6jΧ{ږ@e)EtP՛!l!iB7^1VL t
endstream
endobj
25 0 obj <<
/Type /Page
/Contents 47 0 R
/Resources 46 0 R
/MediaBox [0 0 362.835 272.126]
/Trans << /S /R >>
/Parent 53 0 R
/Annots [ 26 0 R 27 0 R 28 0 R 29 0 R 30 0 R 31 0 R 32 0 R 33 0 R 34 0 R 35 0 R 36 0 R 37 0 R 38 0 R 39 0 R 40 0 R 41 0 R 42 0 R 43 0 R 44 0 R 45 0 R ]
>> endobj
26 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [230.631 0.996 238.601 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
27 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [236.608 0.996 246.571 10.461]
/Subtype/Link/A<>
>> endobj
28 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [244.578 0.996 252.549 10.461]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
29 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [252.32 0.996 259.294 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
30 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [257.302 0.996 264.275 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
31 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [262.283 0.996 269.257 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
32 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [267.264 0.996 274.238 10.461]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
33 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [274.01 0.996 280.984 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
34 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [278.991 0.996 285.965 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
35 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [283.972 0.996 290.946 10.461]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
36 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [288.954 0.996 295.928 10.461]
/A << /S /GoTo /D (Navigation3) >>
>> endobj
37 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [295.699 0.996 302.673 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
38 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [300.681 0.996 307.654 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
39 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [305.662 0.996 312.636 10.461]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
40 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [310.643 0.996 317.617 10.461]
/A << /S /GoTo /D (Navigation3) >>
>> endobj
41 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [317.389 0.996 328.348 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
42 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [326.355 0.996 339.307 10.461]
/A << /S /GoTo /D (Navigation13) >>
>> endobj
43 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [339.078 0.996 348.045 10.461]
/Subtype/Link/A<>
>> endobj
44 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [346.052 0.996 354.022 10.461]
/Subtype/Link/A<>
>> endobj
45 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [352.03 0.996 360.996 10.461]
/Subtype/Link/A<>
>> endobj
48 0 obj <<
/D [25 0 R /XYZ 28.346 272.126 null]
>> endobj
51 0 obj <<
/D [25 0 R /XYZ -28.346 0 null]
>> endobj
52 0 obj <<
/D [25 0 R /XYZ -28.346 0 null]
>> endobj
46 0 obj <<
/ColorSpace 3 0 R /Pattern 2 0 R /ExtGState 1 0 R
/Font << /F18 49 0 R /F16 50 0 R >>
/ProcSet [ /PDF /Text ]
>> endobj
83 0 obj <<
/Length 809
/Filter /FlateDecode
>>
stream
xWn0+hrH˵E[4@I|+z9 %)
);F&iŧYpDJH<{#҈4"A[%A9%PYX0QzQ`
V5/`:9e=;$GPU0A40IUP6@O]pɜNkP$8jy%.b#{FHMÂ,EDq,EM&dhEzZ',4Tb3o$#(fEp:!Μ'Ј#Z>vxDNTFug^X*I/`:I>QE+ QcJ0uip,E%{3n
K*O/ji55A["8-dezxR=@-_qVԿ͒>yYdh6$E(T5[(9c->!|`?W5Kz)%0=o/z5!f{ZNO'l}
I7mjygf9MpN*o'$uRm۫vtIo7Hjo7ĮRҎGG5YN
-
endstream
endobj
82 0 obj <<
/Type /Page
/Contents 83 0 R
/Resources 81 0 R
/MediaBox [0 0 362.835 272.126]
/Trans << /S /R >>
/Parent 53 0 R
/Annots [ 61 0 R 62 0 R 63 0 R 64 0 R 65 0 R 66 0 R 67 0 R 68 0 R 69 0 R 70 0 R 71 0 R 72 0 R 73 0 R 74 0 R 75 0 R 76 0 R 77 0 R 78 0 R 79 0 R 80 0 R 57 0 R 58 0 R 59 0 R 60 0 R ]
>> endobj
61 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [230.631 0.996 238.601 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
62 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [236.608 0.996 246.571 10.461]
/Subtype/Link/A<>
>> endobj
63 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [244.578 0.996 252.549 10.461]
/A << /S /GoTo /D (Navigation3) >>
>> endobj
64 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [252.32 0.996 259.294 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
65 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [257.302 0.996 264.275 10.461]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
66 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [262.283 0.996 269.257 10.461]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
67 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [267.264 0.996 274.238 10.461]
/A << /S /GoTo /D (Navigation3) >>
>> endobj
68 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [274.01 0.996 280.984 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
69 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [278.991 0.996 285.965 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
70 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [283.972 0.996 290.946 10.461]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
71 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [288.954 0.996 295.928 10.461]
/A << /S /GoTo /D (Navigation3) >>
>> endobj
72 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [295.699 0.996 302.673 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
73 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [300.681 0.996 307.654 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
74 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [305.662 0.996 312.636 10.461]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
75 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [310.643 0.996 317.617 10.461]
/A << /S /GoTo /D (Navigation3) >>
>> endobj
76 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [317.389 0.996 328.348 10.461]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
77 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [326.355 0.996 339.307 10.461]
/A << /S /GoTo /D (Navigation13) >>
>> endobj
78 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [339.078 0.996 348.045 10.461]
/Subtype/Link/A<>
>> endobj
79 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [346.052 0.996 354.022 10.461]
/Subtype/Link/A<>
>> endobj
80 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [352.03 0.996 360.996 10.461]
/Subtype/Link/A<>
>> endobj
57 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [27.35 204.529 85.191 214.097]
/A << /S /GoTo /D (Navigation3) >>
>> endobj
58 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [27.35 159.605 178.737 171.295]
/A << /S /GoTo /D (Navigation6) >>
>> endobj
59 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [27.35 118.924 61.782 128.492]
/A << /S /GoTo /D (Navigation11) >>
>> endobj
60 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [27.35 76.122 82.555 85.69]
/A << /S /GoTo /D (Navigation13) >>
>> endobj
54 0 obj <<
/D [82 0 R /XYZ -28.346 0 null]
>> endobj
84 0 obj <<
/D [82 0 R /XYZ -28.346 0 null]
>> endobj
81 0 obj <<
/ColorSpace 3 0 R /Pattern 2 0 R /ExtGState 1 0 R
/Font << /F16 50 0 R >>
/ProcSet [ /PDF /Text ]
>> endobj
109 0 obj <<
/Length 1228
/Filter /FlateDecode
>>
stream
xW[o6~ $5˛(ȲX5[UmaZJ^%+J5i)wnd ~Ja~
A\2xX0eK}#b+ r? KqƤ))Q
P.t4|Xq,T+F*3Ef2#YJ(*1`$q]G-r?P7'0ȲL=h<'rrT
zՆ3D?ng)4t2+PIJp̜OʦH`Ton$&C{ >oB6AFI?!/`Cfi*a2ȇz;=x{]
TC_3W:@|Eo{
zib/ճoQjfT)}j~Xi; Ax$Tk*#'qxier H%pB
"c^{+EPXJU 7Sކ:)6(. Qd:C &{ "D>E 4CI_ ٌoik7w.x2[X7&I*͖45x¦7Hޟ {H4ռ=%Lc