%PDF-1.6
%
1 0 obj
<<
/AcroForm 2 0 R
/Lang (EN)
/Metadata 3 0 R
/Names 4 0 R
/OpenAction [5 0 R /Fit]
/Outlines 6 0 R
/OutputIntents [7 0 R]
/PageLabels 8 0 R
/PageMode /UseOutlines
/Pages 9 0 R
/Type /Catalog
>>
endobj
10 0 obj
<<
/Author (Arnd Hartmanns )
/CreationDate (D:20190328122305+05'30')
/Creator (Springer)
/CrossMarkDomains#5B1#5D (springer.com)
/CrossMarkDomains#5B2#5D (springerlink.com)
/CrossmarkDomainExclusive (true)
/CrossmarkMajorVersionDate (2010-04-23)
/ModDate (D:20190328184454+05'30')
/Subject (Tools and Algorithms for the Construction and Analysis of Systems, doi:10.1007/978-3-030-17462-0_20)
/Title (The Quantitative Verification Benchmark Set)
/doi (10.1007/978-3-030-17462-0_20)
/robots (noindex)
>>
endobj
2 0 obj
<<
/DA (/Helv 0 Tf 0 g )
/DR <<
/Encoding <<
/PDFDocEncoding 11 0 R
>>
/Font <<
/Helv 12 0 R
/ZaDb 13 0 R
>>
>>
/Fields []
>>
endobj
3 0 obj
<<
/Length 32730
/Subtype /XML
/Type /Metadata
>>
stream
2019-03-28T12:23:05+05:30
Springer
2019-03-28T18:44:54+05:30
2019-03-28T18:44:54+05:30
application/pdf
doi:10.1007/978-3-030-17462-0_20
Springer International Publishing
Tools and Algorithms for the Construction and Analysis of Systems, doi:10.1007/978-3-030-17462-0_20
The Quantitative Verification Benchmark Set
Arnd Hartmanns
Michaela Klauck
David Parker
Tim Quatmann
Enno Ruijters
10.1007/978-3-030-17462-0_20
2010-04-23
true
springer.com
springerlink.com
http://dx.doi.org/10.1007/978-3-030-17462-0_20
10.1007/978-3-030-17462-0_20
Book
The Author(s)
2010-04-23
true
10.1007/978-3-030-17462-0_20
noindex
springer.com
springerlink.com
uuid:d3d2c34a-2966-40cd-b3a4-999323c44a3e
uuid:4e839be9-5993-4cd6-a754-d3951960b76f
default
1
converted
uuid:b9f3e3b9-9389-4f72-947f-bfb7b49f4e6b
converted to PDF/A-2b
pdfToolbox
2019-03-28T12:24:10+05:30
converted
uuid:f4690535-baee-459d-bfe7-1ba6749bf2ef
converted to PDF/A-2b
pdfToolbox
2019-03-28T12:25:03+05:30
converted
uuid:55676a8f-03d7-4f22-8349-7e53cd666fdb
converted to PDF/A-2b
pdfToolbox
2019-03-28T18:43:54+05:30
converted
uuid:9f8b2912-db11-4df7-9686-1bdd8b5b3318
converted to PDF/A-2b
pdfToolbox
2019-03-28T18:44:54+05:30
2
B
Arnd Hartmanns
http://orcid.org/0000-0003-3268-8674
David Parker
http://orcid.org/0000-0003-4137-8862
Tim Quatmann
http://orcid.org/0000-0002-2843-5511
Enno Ruijters
http://orcid.org/0000-0002-5855-5282
http://ns.adobe.com/pdfx/1.3/
pdfx
Adobe Document Info PDF eXtension Schema
external
Mirrors crossmark:MajorVersionDate
CrossmarkMajorVersionDate
Text
external
Mirrors crossmark:CrossmarkDomainExclusive
CrossmarkDomainExclusive
Text
internal
Mirrors crossmark:DOI
doi
Text
external
Mirrors crossmark:CrosMarkDomains
CrossMarkDomains
seq Text
internal
A name object indicating whether the document has been modified to include trapping information
robots
Text
internal
ID of PDF/X standard
GTS_PDFXVersion
Text
internal
Conformance level of PDF/X standard
GTS_PDFXConformance
Text
internal
Company creating the PDF
Company
Text
internal
Date when document was last modified
SourceModified
Text
http://crossref.org/crossmark/1.0/
crossmark
Crossmark Schema
internal
Usual same as prism:doi
DOI
Text
external
The date when a publication was published.
MajorVersionDate
Text
internal
CrossmarkDomainExclusive
CrossmarkDomainExclusive
Text
internal
CrossMarkDomains
CrossMarkDomains
seq Text
http://prismstandard.org/namespaces/basic/2.0/
prism
Prism Schema
external
This element provides the url for an article or unit of content. \nThe attribute platform is optionally allowed for situations in which multiple URLs must be specified. PRISM recommends that a subset of the PCV platform values, namely “mobile” and “web”, be used in conjunction with this element. \nNOTE: PRISM recommends against the use of the #other value allowed in the PRISM Platform controlled vocabulary. In lieu of using #other please reach out to the PRISM group at prism-wg@yahoogroups.com to request addition of your term to the Platform Controlled Vocabulary. \n
url
URI
external
The Digital Object Identifier for the article.\nThe DOI may also be used as the dc:identifier. If used as a dc:identifier, the URI form should be captured, and the bare identifier should also be captured using prism:doi. If an alternate unique identifier is used as the required dc:identifier, then the DOI should be specified as a bare identifier within prism:doi only. \nIf the URL associated with a DOI is to be specified, then prism:url may be used in conjunction with prism:doi in order to provide the service endpoint (i.e. the URL). \n
doi
Text
external
ISSN for an electronic version of the issue in which the resource occurs. \nPermits publishers to include a second ISSN, identifying an electronic version of the issue in which the resource occurs (therefore e(lectronic)Issn. If used, prism:eIssn MUST contain the ISSN of the electronic version.
issn
Text
external
The aggregation type specifies the unit of aggregation for a content collection. \nComment \nPRISM recommends that the PRISM Aggregation Type Controlled Vocabulary be used to provide values for this element. \nNote: PRISM recommends against the use of the #other value currently allowed in this controlled vocabulary. In lieu of using #other please reach out to the PRISM group at info@prismstandard.org to request addition of your term to the Aggregation Type Controlled Vocabulary. \n\n
aggregationType
Text
external
Title of the magazine, or other publication, in which a resource was/will be published. \nTypically this will be used to provide the name of the magazine an article appeared in as metadata for the article, along with information such as the article title, the publisher, volume, number, and cover date. \n\nNote: Publication name can be used to differentiate between a print magazine and the online version if the names are different such as “magazine” and “magazine.com.” \n
publicationName
Text
external
Copyright
copyright
Text
http://ns.adobe.com/pdf/1.3/
pdf
Adobe PDF Schema
internal
A name object indicating whether the document has been modified to include trapping information
Trapped
Text
http://ns.adobe.com/xap/1.0/mm/
xmpMM
XMP Media Management Schema
internal
UUID based identifier for specific incarnation of a document
InstanceID
URI
internal
The common identifier for all versions and renditions of a document.
DocumentID
URI
internal
The common identifier for all versions and renditions of a document.
OriginalDocumentID
URI
http://www.aiim.org/pdfa/ns/id/
pdfaid
PDF/A ID Schema
internal
Part of PDF/A standard
part
Integer
internal
Amendment of PDF/A standard
amd
Text
internal
Conformance level of PDF/A standard
conformance
Text
Springer Nature ORCID Schema
http://springernature.com/ns/xmpExtensions/2.0/
sn
authorInfo
Bag AuthorInformation
external
Author information: contains the name of each author and his/her ORCiD (ORCiD: Open Researcher and Contributor ID). An ORCiD is a persistent identifier (a non-proprietary alphanumeric code) to uniquely identify scientific and other academic authors.
editorInfo
Bag EditorInformation
external
Editor information: contains the name of each editor and his/her ORCID identifier.
seriesEditorInfo
Bag EditorInformation
external
Series editor information: contains the name of each series editor and his/her ORCID identifier.
AuthorInformation
http://springernature.com/ns/xmpExtensions/2.0/authorinfo/
author
Specifies the types of author information: name and ORCID of an author.
name
Text
Gives the name of an author.
orcid
URI
Gives the ORCID of an author.
EditorInformation
http://springernature.com/ns/xmpExtensions/2.0/editorInfo/
editor
Specifies the types of editor information: name and ORCID of an editor.
name
Text
Gives the name of an editor.
orcid
URI
Gives the ORCID of an editor.
SeriesEditorInformation
http://springernature.com/ns/xmpExtensions/2.0/seriesEditorInfo/
seriesEditor
Specifies the types of series editor information: name and ORCID of a series editor.
name
Text
Gives the name of a series editor.
orcid
URI
Gives the ORCID of a series editor.
endstream
endobj
4 0 obj
<<
/Dests 14 0 R
>>
endobj
5 0 obj
<<
/Annots [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]
/Contents [29 0 R 30 0 R 31 0 R 32 0 R 33 0 R 34 0 R 35 0 R 36 0 R]
/CropBox [0.0 0.0 439.37 666.142]
/MediaBox [0.0 0.0 439.37 666.142]
/Parent 9 0 R
/Resources 37 0 R
/Rotate 0
/Thumb 38 0 R
/Type /Page
>>
endobj
6 0 obj
<<
/First 39 0 R
/Last 39 0 R
/Type /Outlines
>>
endobj
7 0 obj
<<
/DestOutputProfile 40 0 R
/Info (sRGB IEC61966-2.1)
/OutputCondition (sRGB)
/OutputConditionIdentifier (Custom)
/RegistryName ()
/S /GTS_PDFA1
/Type /OutputIntent
>>
endobj
8 0 obj
<<
/Nums [0 41 0 R]
>>
endobj
9 0 obj
<<
/Count 8
/Kids [42 0 R 5 0 R 43 0 R 44 0 R 45 0 R 46 0 R 47 0 R 48 0 R]
/Type /Pages
>>
endobj
11 0 obj
<<
/Differences [24 /breve /caron /circumflex /dotaccent /hungarumlaut /ogonek /ring /tilde 39
/quotesingle 96 /grave 128 /bullet /dagger /daggerdbl /ellipsis /emdash /endash
/florin /fraction /guilsinglleft /guilsinglright /minus /perthousand /quotedblbase /quotedblleft /quotedblright /quoteleft
/quoteright /quotesinglbase /trademark /fi /fl /Lslash /OE /Scaron /Ydieresis /Zcaron
/dotlessi /lslash /oe /scaron /zcaron 160 /Euro 164 /currency 166
/brokenbar 168 /dieresis /copyright /ordfeminine 172 /logicalnot /.notdef /registered /macron
/degree /plusminus /twosuperior /threesuperior /acute /mu 183 /periodcentered /cedilla /onesuperior
/ordmasculine 188 /onequarter /onehalf /threequarters 192 /Agrave /Aacute /Acircumflex /Atilde
/Adieresis /Aring /AE /Ccedilla /Egrave /Eacute /Ecircumflex /Edieresis /Igrave /Iacute
/Icircumflex /Idieresis /Eth /Ntilde /Ograve /Oacute /Ocircumflex /Otilde /Odieresis /multiply
/Oslash /Ugrave /Uacute /Ucircumflex /Udieresis /Yacute /Thorn /germandbls /agrave /aacute
/acircumflex /atilde /adieresis /aring /ae /ccedilla /egrave /eacute /ecircumflex /edieresis
/igrave /iacute /icircumflex /idieresis /eth /ntilde /ograve /oacute /ocircumflex /otilde
/odieresis /divide /oslash /ugrave /uacute /ucircumflex /udieresis /yacute /thorn /ydieresis]
/Type /Encoding
>>
endobj
12 0 obj
<<
/BaseFont /Helvetica
/Encoding 11 0 R
/Name /Helv
/Subtype /Type1
/Type /Font
>>
endobj
13 0 obj
<<
/BaseFont /ZapfDingbats
/Name /ZaDb
/Subtype /Type1
/Type /Font
>>
endobj
14 0 obj
<<
/Kids [49 0 R]
>>
endobj
15 0 obj
<<
/A <<
/S /URI
/URI (http://crossmark.crossref.org/dialog/?doi=10.1007/978-3-030-17462-0_20&domain=pdf)
>>
/AP <<
/N 50 0 R
>>
/Border [0 0 0]
/C [0 1 1]
/F 4
/H /I
/Rect [20.271 611.964 54.267 645.951]
/Subtype /Link
/Type /Annot
>>
endobj
16 0 obj
<<
/A <<
/S /URI
/URI (http://orcid.org/0000-0003-3268-8674)
>>
/AP <<
/N 51 0 R
>>
/Border [0 0 0]
/C [0 1 1]
/F 4
/H /I
/Rect [208.452 544.815 219.444 555.807]
/Subtype /Link
/Type /Annot
>>
endobj
17 0 obj
<<
/A <<
/S /URI
/URI (http://orcid.org/0000-0003-4137-8862)
>>
/AP <<
/N 52 0 R
>>
/Border [0 0 0]
/C [0 1 1]
/F 4
/H /I
/Rect [192.801 532.863 203.793 543.846]
/Subtype /Link
/Type /Annot
>>
endobj
18 0 obj
<<
/A <<
/S /URI
/URI (http://orcid.org/0000-0002-2843-5511)
>>
/AP <<
/N 53 0 R
>>
/Border [0 0 0]
/C [0 1 1]
/F 4
/H /I
/Rect [280.416 532.863 291.408 543.846]
/Subtype /Link
/Type /Annot
>>
endobj
19 0 obj
<<
/A <<
/S /URI
/URI (http://orcid.org/0000-0002-5855-5282)
>>
/AP <<
/N 54 0 R
>>
/Border [0 0 0]
/C [0 1 1]
/F 4
/H /I
/Rect [249.213 520.911 260.205 531.894]
/Subtype /Link
/Type /Annot
>>
endobj
20 0 obj
<<
/A <<
/S /URI
/URI (http://qcomp.org/)
>>
/AP <<
/N 55 0 R
>>
/Border [0 0 0]
/C [0 1 1]
/F 4
/H /I
/Rect [187.59 308.268 231.324 315.867]
/Subtype /Link
/Type /Annot
>>
endobj
21 0 obj
<<
/AP <<
/N 56 0 R
>>
/Border [0 0 0]
/C [0 1 0]
/Dest (cite.KNP11)
/F 4
/H /I
/Rect [132.384 140.49 143.334 151.449]
/Subtype /Link
/Type /Annot
>>
endobj
22 0 obj
<<
/AP <<
/N 57 0 R
>>
/Border [0 0 0]
/C [0 1 0]
/Dest (cite.LLN18)
/F 4
/H /I
/Rect [277.23 140.49 288.18 151.449]
/Subtype /Link
/Type /Annot
>>
endobj
23 0 obj
<<
/AP <<
/N 58 0 R
>>
/Border [0 0 0]
/C [0 1 0]
/Dest (cite.DJLMT15)
/F 4
/H /I
/Rect [245.487 104.625 251.46 115.584]
/Subtype /Link
/Type /Annot
>>
endobj
24 0 obj
<<
/AP <<
/N 59 0 R
>>
/Border [0 0 0]
/C [0 1 0]
/Dest (cite.DJKV17)
/F 4
/H /I
/Rect [254.235 104.625 260.208 115.584]
/Subtype /Link
/Type /Annot
>>
endobj
25 0 obj
<<
/AP <<
/N 60 0 R
>>
/Border [0 0 0]
/C [0 1 0]
/Dest (cite.HLSTZ14)
/F 4
/H /I
/Rect [262.974 104.625 273.924 115.584]
/Subtype /Link
/Type /Annot
>>
endobj
26 0 obj
<<
/AP <<
/N 61 0 R
>>
/Border [0 0 0]
/C [0 1 0]
/Dest (cite.HH14)
/F 4
/H /I
/Rect [276.699 104.625 287.649 115.584]
/Subtype /Link
/Type /Annot
>>
endobj
27 0 obj
<<
/AP <<
/N 62 0 R
>>
/Border [0 0 0]
/C [0 1 0]
/Dest (cite.LST16)
/F 4
/H /I
/Rect [290.424 104.625 301.374 115.584]
/Subtype /Link
/Type /Annot
>>
endobj
28 0 obj
<<
/A <<
/S /URI
/URI (https://doi.org/10.1007/978-3-030-17462-0_20)
>>
/AP <<
/N 63 0 R
>>
/Border [0 0 0]
/C [0 1 1]
/F 4
/H /I
/Rect [38.406 32.895 200.535 41.862]
/Subtype /Link
/Type /Annot
>>
endobj
29 0 obj
<<
/Length 4443
/Filter /FlateDecode
>>
stream
HWɎ$IWd˕n@ā.`PUtψ-UKan˳gï|???~7q7Ë'IOcr9C%-ţyv>o>@?^}?=] ?PGn{ZR[{Hs(y{sQ˸|>B%d