%PDF-1.7
%
1 0 obj
<<
/Lang (en)
/MarkInfo <<
/Marked true
>>
/Metadata 2 0 R
/Names 3 0 R
/OpenAction [4 0 R /FitH 850]
/Outlines 5 0 R
/PageLabels 6 0 R
/PageLayout /SinglePage
/PageMode /UseOutlines
/Pages 7 0 R
/StructTreeRoot 8 0 R
/Threads [9 0 R]
/Type /Catalog
/VTeX#3AMarkInfo <<
/LineNMarked false
>>
>>
endobj
10 0 obj
<<
/Author <4B6C617573204472E4676572>
/CreationDate (D:20140604161550+03'00')
/Creator (Elsevier)
/CrossMarkDomains#5B1#5D (elsevier.com)
/CrossMarkDomains#5B2#5D (sciencedirect.com)
/CrossmarkDomainExclusive (true)
/CrossmarkMajorVersionDate (2010-04-23)
/ElsevierWebPDFSpecifications (6.4)
/ModDate (D:20140604161550+03'00')
/Producer (Acrobat Distiller 9.5.5 \(Windows\))
/Subject <5468656F7265746963616C20436F6D707574657220536369656E63652C20353338202832303134292033378535332E2031302E313031362F6A2E7463732E323031332E30372E303133>
/Title (Local abstraction refinement for probabilistic timed programs)
/Trapped /False
/doi (10.1016/j.tcs.2013.07.013)
/robots (noindex)
>>
endobj
2 0 obj
<<
/Length 6984
/Subtype /XML
/Type /Metadata
>>
stream
application/pdf
doi:10.1016/j.tcs.2013.07.013
Local abstraction refinement for probabilistic timed programs
Klaus Dräger
Marta Kwiatkowska
David Parker
Hongyang Qu
Probabilistic verification
Abstraction refinement
Theoretical Computer Science, 538 (2014) 37–53. 10.1016/j.tcs.2013.07.013
Elsevier B.V.
journal
Theoretical Computer Science
Copyright ©2013 Elsevier B.V. All rights reserved.
0304-3975
538
37-53
37
53
10.1016/j.tcs.2013.07.013
http://dx.doi.org/10.1016/j.tcs.2013.07.013
2014-06-12
12 June 2014
C
Quantitative Aspects of Programming Languages and Systems (2011-12)
2010-04-23
true
10.1016/j.tcs.2013.07.013
elsevier.com
sciencedirect.com
6.4
10.1016/j.tcs.2013.07.013
noindex
2010-04-23
true
elsevier.com
sciencedirect.com
Elsevier
2014-06-04T16:15:50+03:00
2014-06-04T16:15:50+03:00
2014-06-04T16:15:50+03:00
True
Acrobat Distiller 9.5.5 (Windows)
False
uuid:df7f6e55-c28c-400f-857d-fb821a01ed4a
uuid:0c05ecc0-514d-4679-83b0-eaa1080d10b7
endstream
endobj
3 0 obj
<<
/Dests 11 0 R
>>
endobj
4 0 obj
<<
/Annots [12 0 R 13 0 R 14 0 R 15 0 R 16 0 R 17 0 R 18 0 R 19 0 R 20 0 R 21 0 R
22 0 R 23 0 R 24 0 R 25 0 R 26 0 R 27 0 R 28 0 R 29 0 R]
/B [30 0 R]
/Contents [31 0 R 32 0 R 33 0 R 34 0 R 35 0 R 36 0 R 37 0 R 38 0 R]
/CropBox [8.504 8.504 552.756 751.181]
/MediaBox [0 0 561.26 759.685]
/Parent 39 0 R
/Resources <<
/ExtGState <<
/GS0 40 0 R
/GS1 41 0 R
>>
/Font <<
/T1_0 42 0 R
/T1_1 43 0 R
/T1_2 44 0 R
/T1_3 45 0 R
/T1_4 46 0 R
/T1_5 47 0 R
/T1_6 48 0 R
/T1_7 49 0 R
>>
/ProcSet [/PDF /Text /ImageC]
/Properties <<
/MC0 50 0 R
>>
/XObject <<
/Im0 51 0 R
/Im1 52 0 R
/Im2 53 0 R
>>
>>
/Rotate 0
/StructParents 1
/TrimBox [8.504 8.504 552.756 751.181]
/Type /Page
>>
endobj
5 0 obj
<<
/Count 18
/First 54 0 R
/Last 54 0 R
>>
endobj
6 0 obj
<<
/Nums [0 55 0 R]
>>
endobj
7 0 obj
<<
/Count 18
/Kids [39 0 R 56 0 R]
/Type /Pages
>>
endobj
8 0 obj
<<
/K [57 0 R 58 0 R 59 0 R 60 0 R 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 81 0 R 82 0 R 83 0 R 84 0 R 85 0 R 86 0 R
87 0 R 88 0 R 89 0 R 90 0 R 91 0 R 92 0 R 93 0 R 94 0 R 95 0 R 96 0 R
97 0 R 98 0 R 99 0 R 100 0 R 101 0 R 102 0 R 103 0 R 104 0 R 105 0 R 106 0 R
107 0 R 108 0 R 109 0 R 110 0 R 111 0 R 112 0 R 113 0 R 114 0 R 115 0 R 116 0 R
117 0 R 118 0 R 119 0 R 120 0 R 121 0 R 122 0 R 123 0 R 124 0 R 125 0 R 126 0 R
127 0 R 128 0 R 129 0 R 130 0 R 131 0 R 132 0 R 133 0 R 134 0 R 135 0 R 136 0 R
137 0 R 138 0 R 139 0 R 140 0 R 141 0 R 142 0 R 143 0 R 144 0 R 145 0 R 146 0 R
147 0 R 148 0 R 149 0 R 150 0 R 151 0 R 152 0 R 153 0 R 154 0 R 155 0 R 156 0 R
157 0 R 158 0 R 159 0 R 160 0 R 161 0 R 162 0 R 163 0 R 164 0 R 165 0 R 166 0 R
167 0 R 168 0 R 169 0 R 170 0 R 171 0 R 172 0 R 173 0 R 174 0 R 175 0 R 176 0 R
177 0 R 178 0 R 179 0 R 180 0 R 181 0 R 182 0 R 183 0 R 184 0 R 185 0 R 186 0 R
187 0 R 188 0 R 189 0 R 190 0 R 191 0 R 192 0 R 193 0 R 194 0 R 195 0 R 196 0 R
197 0 R 198 0 R 199 0 R 200 0 R 201 0 R 202 0 R 203 0 R 204 0 R 205 0 R 206 0 R
207 0 R 208 0 R 209 0 R 210 0 R 211 0 R 212 0 R 213 0 R 214 0 R 215 0 R 216 0 R
217 0 R 218 0 R 219 0 R 220 0 R 221 0 R 222 0 R 223 0 R 224 0 R 225 0 R 226 0 R
227 0 R 228 0 R 229 0 R 230 0 R 231 0 R 232 0 R 233 0 R 234 0 R 235 0 R 236 0 R
237 0 R 238 0 R 239 0 R 240 0 R 241 0 R 242 0 R 243 0 R 244 0 R 245 0 R 246 0 R
247 0 R 248 0 R 249 0 R 250 0 R 251 0 R 252 0 R 253 0 R 254 0 R 255 0 R 256 0 R
257 0 R 258 0 R 259 0 R 260 0 R 261 0 R 262 0 R 263 0 R 264 0 R 265 0 R 266 0 R
267 0 R 268 0 R 269 0 R 270 0 R 271 0 R 272 0 R 273 0 R 274 0 R 275 0 R 276 0 R
277 0 R 278 0 R 279 0 R 280 0 R 281 0 R 282 0 R 283 0 R 284 0 R 285 0 R 286 0 R
287 0 R 288 0 R 289 0 R 290 0 R 291 0 R 292 0 R 293 0 R 294 0 R 295 0 R]
/ParentTree 296 0 R
/ParentTreeNextKey 18
/Type /StructTreeRoot
>>
endobj
9 0 obj
<<
/F 30 0 R
/I <<
/Title (article)
>>
>>
endobj
11 0 obj
<<
/Kids [297 0 R 298 0 R]
>>
endobj
12 0 obj
<<
/A <<
/S /URI
/URI (http://dx.doi.org/10.1016/j.tcs.2013.07.013)
>>
/Border [0 0 0]
/C [1 1 1]
/H /I
/Rect [205.262 709.393 350.658 717.254]
/Subtype /Link
/Type /Annot
>>
endobj
13 0 obj
<<
/A <<
/S /URI
/URI (http://www.ScienceDirect.com/)
>>
/Border [0 0 0]
/C [1 1 1]
/H /I
/Rect [302.157 681.926 354.294 691.455]
/Subtype /Link
/Type /Annot
>>
endobj
14 0 obj
<<
/A <<
/S /URI
/URI (http://www.elsevier.com/locate/tcs)
>>
/Border [0 0 0]
/C [1 1 1]
/H /I
/Rect [225.188 626.126 333.054 635.655]
/Subtype /Link
/Type /Annot
>>
endobj
15 0 obj
<<
/Border [0 0 0]
/C [1 1 1]
/Dest (addressox0.label)
/H /I
/Rect [109.25 554.228 115.408 564.156]
/Subtype /Link
/Type /Annot
>>
endobj
16 0 obj
<<
/Border [0 0 0]
/C [1 1 1]
/Dest (COR1thanks.label)
/H /I
/Rect [116.36 547.744 123.001 564.259]
/Subtype /Link
/Type /Annot
>>
endobj
17 0 obj
<<
/Border [0 0 0]
/C [1 1 1]
/Dest (addressox0.label)
/H /I
/Rect [227.474 554.228 233.632 564.156]
/Subtype /Link
/Type /Annot
>>
endobj
18 0 obj
<<
/Border [0 0 0]
/C [1 1 1]
/Dest (addressbi0.label)
/H /I
/Rect [303.128 554.228 309.775 564.156]
/Subtype /Link
/Type /Annot
>>
endobj
19 0 obj
<<
/Border [0 0 0]
/C [1 1 1]
/Dest (addressox0.label)
/H /I
/Rect [383.21 554.228 389.368 564.156]
/Subtype /Link
/Type /Annot
>>
endobj
20 0 obj
<<
/Border [0 0 0]
/C [1 1 1]
/Dest (DJJL01.cite)
/H /I
/Rect [280.239 296.948 321.267 306.807]
/Subtype /Link
/Type /Annot
>>
endobj
21 0 obj
<<
/Border [0 0 0]
/C [1 1 1]
/Dest (KNP09c.cite)
/H /I
/Rect [496.62 296.948 512.579 306.807]
/Subtype /Link
/Type /Annot
>>
endobj
22 0 obj
<<
/Border [0 0 0]
/C [1 1 1]
/Dest (ZSR+10.cite)
/H /I
/Rect [163.21 286.49 180.181 296.349]
/Subtype /Link
/Type /Annot
>>
endobj
23 0 obj
<<
/Border [0 0 0]
/C [1 1 1]
/Dest (KNP10b.cite)
/H /I
/Rect [161.229 244.641 178.2 254.5]
/Subtype /Link
/Type /Annot
>>
endobj
24 0 obj
<<
/Border [0 0 0]
/C [1 1 1]
/Dest (DJJL01.cite)
/H /I
/Rect [54.5833 223.706 78.0321 233.565]
/Subtype /Link
/Type /Annot
>>
endobj
25 0 obj
<<
/Border [0 0 0]
/C [1 1 1]
/Dest (HWZ08.cite)
/H /I
/Rect [312.512 192.314 329.492 202.173]
/Subtype /Link
/Type /Annot
>>
endobj
26 0 obj
<<
/A <<
/S /URI
/URI (mailto:klaus.draeger@cs.ox.ac.uk)
>>
/Border [0 0 0]
/C [1 1 1]
/H /I
/Rect [101.078 82.0208 177.066 89.8822]
/Subtype /Link
/Type /Annot
>>
endobj
27 0 obj
<<
/A <<
/S /URI
/URI (http://dx.doi.org/10.1016/j.tcs.2013.07.013)
>>
/Border [0 0 0]
/C [1 1 1]
/H /I
/Rect [44.3606 57.0007 169.794 64.8621]
/Subtype /Link
/Type /Annot
>>
endobj
28 0 obj
<<
/A 299 0 R
/BS <<
/S /S
/Type /Border
/W 0
>>
/Border [0 0 0]
/Rect [44.3608 286.49 64.9312 296.349]
/Subtype /Link
/Type /Annot
>>
endobj
29 0 obj
<<
/A 300 0 R
/BS <<
/S /S
/Type /Border
/W 0
>>
/Border [0 0 0]
/Rect [454.004 563.654 511.08 585.014]
/Subtype /Link
/Type /Annot
>>
endobj
30 0 obj
<<
/N 301 0 R
/P 4 0 R
/R [42 81 515 700]
/T 9 0 R
/V 302 0 R
>>
endobj
31 0 obj
<<
/Length 1117
/Filter /FlateDecode
>>
stream
HUnF}'|pHR
Ml.
Rt=͝{~t~~mR`Q>d..ubX1SiRkx/* 3#Ͷl>uTqYv-]JZYT+Qʔ7sW¡(/ݮ×`\]VRK՟,p](M!PQ⪨/n;E0|{3Xzu|
2-LjlPS<&1<rM0;OmQo9wQpj8w:| RpBDt
44@Ds6S+Gsh>ws`ձrѴ\^e8G:e!#TAF
_TQSר~h|sr~
{ GʧVHTQRA2