Ontology type: schema:Chapter Open Access: True
2011
AUTHORSVojtěch Forejt , Marta Kwiatkowska , Gethin Norman , David Parker
ABSTRACTThis tutorial provides an introduction to probabilistic model checking, a technique for automatically verifying quantitative properties of probabilistic systems. We focus on Markov decision processes (MDPs), which model both stochastic and nondeterministic behaviour. We describe methods to analyse a wide range of their properties, including specifications in the temporal logics PCTL and LTL, probabilistic safety properties and cost- or reward-based measures. We also discuss multi-objective probabilistic model checking, used to analyse trade-offs between several different quantitative properties. Applications of the techniques in this tutorial include performance and dependability analysis of networked systems, communication protocols and randomised distributed algorithms. Since such systems often comprise several components operating in parallel, we also cover techniques for compositional modelling and verification of multi-component probabilistic systems. Finally, we describe three large case studies which illustrate practical applications of the various methods discussed in the tutorial. More... »
PAGES53-113
Formal Methods for Eternal Networked Software Systems
ISBN
978-3-642-21454-7
978-3-642-21455-4
http://scigraph.springernature.com/pub.10.1007/978-3-642-21455-4_3
DOIhttp://dx.doi.org/10.1007/978-3-642-21455-4_3
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1043781609
JSON-LD is the canonical representation for SciGraph data.
TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT
[
{
"@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json",
"about": [
{
"id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Information and Computing Sciences",
"type": "DefinedTerm"
},
{
"id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0801",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Artificial Intelligence and Image Processing",
"type": "DefinedTerm"
},
{
"id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Computation Theory and Mathematics",
"type": "DefinedTerm"
},
{
"id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0803",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Computer Software",
"type": "DefinedTerm"
}
],
"author": [
{
"affiliation": {
"alternateName": "Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK",
"id": "http://www.grid.ac/institutes/grid.4991.5",
"name": [
"Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK"
],
"type": "Organization"
},
"familyName": "Forejt",
"givenName": "Vojt\u011bch",
"id": "sg:person.012103627631.41",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012103627631.41"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK",
"id": "http://www.grid.ac/institutes/grid.4991.5",
"name": [
"Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK"
],
"type": "Organization"
},
"familyName": "Kwiatkowska",
"givenName": "Marta",
"id": "sg:person.011375012273.39",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK",
"id": "http://www.grid.ac/institutes/grid.8756.c",
"name": [
"School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK"
],
"type": "Organization"
},
"familyName": "Norman",
"givenName": "Gethin",
"id": "sg:person.016323171577.36",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK",
"id": "http://www.grid.ac/institutes/grid.4991.5",
"name": [
"Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK"
],
"type": "Organization"
},
"familyName": "Parker",
"givenName": "David",
"id": "sg:person.014007552600.37",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37"
],
"type": "Person"
}
],
"datePublished": "2011",
"datePublishedReg": "2011-01-01",
"description": "This tutorial provides an introduction to probabilistic model checking, a technique for automatically verifying quantitative properties of probabilistic systems. We focus on Markov decision processes (MDPs), which model both stochastic and nondeterministic behaviour. We describe methods to analyse a wide range of their properties, including specifications in the temporal logics PCTL and LTL, probabilistic safety properties and cost- or reward-based measures. We also discuss multi-objective probabilistic model checking, used to analyse trade-offs between several different quantitative properties. Applications of the techniques in this tutorial include performance and dependability analysis of networked systems, communication protocols and randomised distributed algorithms. Since such systems often comprise several components operating in parallel, we also cover techniques for compositional modelling and verification of multi-component probabilistic systems. Finally, we describe three large case studies which illustrate practical applications of the various methods discussed in the tutorial.",
"editor": [
{
"familyName": "Bernardo",
"givenName": "Marco",
"type": "Person"
},
{
"familyName": "Issarny",
"givenName": "Val\u00e9rie",
"type": "Person"
}
],
"genre": "chapter",
"id": "sg:pub.10.1007/978-3-642-21455-4_3",
"inLanguage": "en",
"isAccessibleForFree": true,
"isPartOf": {
"isbn": [
"978-3-642-21454-7",
"978-3-642-21455-4"
],
"name": "Formal Methods for Eternal Networked Software Systems",
"type": "Book"
},
"keywords": [
"probabilistic model checking",
"probabilistic systems",
"Markov decision process",
"model checking",
"probabilistic safety properties",
"reward-based measures",
"temporal logic PCTL",
"verification techniques",
"dependability analysis",
"large case study",
"communication protocols",
"nondeterministic behavior",
"safety properties",
"quantitative properties",
"logic PCTL",
"networked systems",
"compositional modelling",
"such systems",
"decision process",
"checking",
"tutorial",
"case study",
"practical applications",
"system",
"algorithm",
"PCTL",
"applications",
"technique",
"verification",
"specification",
"LTL",
"properties",
"protocol",
"performance",
"method",
"cost",
"wide range",
"modelling",
"parallel",
"process",
"components",
"behavior",
"introduction",
"range",
"measures",
"analysis",
"study"
],
"name": "Automated Verification Techniques for Probabilistic Systems",
"pagination": "53-113",
"productId": [
{
"name": "dimensions_id",
"type": "PropertyValue",
"value": [
"pub.1043781609"
]
},
{
"name": "doi",
"type": "PropertyValue",
"value": [
"10.1007/978-3-642-21455-4_3"
]
}
],
"publisher": {
"name": "Springer Nature",
"type": "Organisation"
},
"sameAs": [
"https://doi.org/10.1007/978-3-642-21455-4_3",
"https://app.dimensions.ai/details/publication/pub.1043781609"
],
"sdDataset": "chapters",
"sdDatePublished": "2022-05-10T10:43",
"sdLicense": "https://scigraph.springernature.com/explorer/license/",
"sdPublisher": {
"name": "Springer Nature - SN SciGraph project",
"type": "Organization"
},
"sdSource": "s3://com-springernature-scigraph/baseset/20220509/entities/gbq_results/chapter/chapter_246.jsonl",
"type": "Chapter",
"url": "https://doi.org/10.1007/978-3-642-21455-4_3"
}
]
Download the RDF metadata as: json-ld nt turtle xml License info
JSON-LD is a popular format for linked data which is fully compatible with JSON.
curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-21455-4_3'
N-Triples is a line-based linked data format ideal for batch operations.
curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-21455-4_3'
Turtle is a human-readable linked data format.
curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-21455-4_3'
RDF/XML is a standard XML format for linked data.
curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-21455-4_3'
This table displays all metadata directly associated to this object as RDF triples.
144 TRIPLES
23 PREDICATES
75 URIs
66 LITERALS
7 BLANK NODES
Subject | Predicate | Object | |
---|---|---|---|
1 | sg:pub.10.1007/978-3-642-21455-4_3 | schema:about | anzsrc-for:08 |
2 | ″ | ″ | anzsrc-for:0801 |
3 | ″ | ″ | anzsrc-for:0802 |
4 | ″ | ″ | anzsrc-for:0803 |
5 | ″ | schema:author | Ncf446774679445a1b25461a5c935fccd |
6 | ″ | schema:datePublished | 2011 |
7 | ″ | schema:datePublishedReg | 2011-01-01 |
8 | ″ | schema:description | This tutorial provides an introduction to probabilistic model checking, a technique for automatically verifying quantitative properties of probabilistic systems. We focus on Markov decision processes (MDPs), which model both stochastic and nondeterministic behaviour. We describe methods to analyse a wide range of their properties, including specifications in the temporal logics PCTL and LTL, probabilistic safety properties and cost- or reward-based measures. We also discuss multi-objective probabilistic model checking, used to analyse trade-offs between several different quantitative properties. Applications of the techniques in this tutorial include performance and dependability analysis of networked systems, communication protocols and randomised distributed algorithms. Since such systems often comprise several components operating in parallel, we also cover techniques for compositional modelling and verification of multi-component probabilistic systems. Finally, we describe three large case studies which illustrate practical applications of the various methods discussed in the tutorial. |
9 | ″ | schema:editor | Nf18bd651404248a882fcad3c9836f51f |
10 | ″ | schema:genre | chapter |
11 | ″ | schema:inLanguage | en |
12 | ″ | schema:isAccessibleForFree | true |
13 | ″ | schema:isPartOf | N3055ac90fd22417b8e705fff6c3a49af |
14 | ″ | schema:keywords | LTL |
15 | ″ | ″ | Markov decision process |
16 | ″ | ″ | PCTL |
17 | ″ | ″ | algorithm |
18 | ″ | ″ | analysis |
19 | ″ | ″ | applications |
20 | ″ | ″ | behavior |
21 | ″ | ″ | case study |
22 | ″ | ″ | checking |
23 | ″ | ″ | communication protocols |
24 | ″ | ″ | components |
25 | ″ | ″ | compositional modelling |
26 | ″ | ″ | cost |
27 | ″ | ″ | decision process |
28 | ″ | ″ | dependability analysis |
29 | ″ | ″ | introduction |
30 | ″ | ″ | large case study |
31 | ″ | ″ | logic PCTL |
32 | ″ | ″ | measures |
33 | ″ | ″ | method |
34 | ″ | ″ | model checking |
35 | ″ | ″ | modelling |
36 | ″ | ″ | networked systems |
37 | ″ | ″ | nondeterministic behavior |
38 | ″ | ″ | parallel |
39 | ″ | ″ | performance |
40 | ″ | ″ | practical applications |
41 | ″ | ″ | probabilistic model checking |
42 | ″ | ″ | probabilistic safety properties |
43 | ″ | ″ | probabilistic systems |
44 | ″ | ″ | process |
45 | ″ | ″ | properties |
46 | ″ | ″ | protocol |
47 | ″ | ″ | quantitative properties |
48 | ″ | ″ | range |
49 | ″ | ″ | reward-based measures |
50 | ″ | ″ | safety properties |
51 | ″ | ″ | specification |
52 | ″ | ″ | study |
53 | ″ | ″ | such systems |
54 | ″ | ″ | system |
55 | ″ | ″ | technique |
56 | ″ | ″ | temporal logic PCTL |
57 | ″ | ″ | tutorial |
58 | ″ | ″ | verification |
59 | ″ | ″ | verification techniques |
60 | ″ | ″ | wide range |
61 | ″ | schema:name | Automated Verification Techniques for Probabilistic Systems |
62 | ″ | schema:pagination | 53-113 |
63 | ″ | schema:productId | N7e61902ba4724095b0e792ed4f633729 |
64 | ″ | ″ | N910852dacb69496188eaeba276d51bc0 |
65 | ″ | schema:publisher | Neb7da2be22b54db2995712cb0a1251d4 |
66 | ″ | schema:sameAs | https://app.dimensions.ai/details/publication/pub.1043781609 |
67 | ″ | ″ | https://doi.org/10.1007/978-3-642-21455-4_3 |
68 | ″ | schema:sdDatePublished | 2022-05-10T10:43 |
69 | ″ | schema:sdLicense | https://scigraph.springernature.com/explorer/license/ |
70 | ″ | schema:sdPublisher | Nbd3396dc78264cf598a25e511d965bde |
71 | ″ | schema:url | https://doi.org/10.1007/978-3-642-21455-4_3 |
72 | ″ | sgo:license | sg:explorer/license/ |
73 | ″ | sgo:sdDataset | chapters |
74 | ″ | rdf:type | schema:Chapter |
75 | N1d972b2c8b504fd69f10333e722d888a | rdf:first | sg:person.016323171577.36 |
76 | ″ | rdf:rest | Nbce2b5e0e0cd4f4aaf6c08f9aea1851b |
77 | N3055ac90fd22417b8e705fff6c3a49af | schema:isbn | 978-3-642-21454-7 |
78 | ″ | ″ | 978-3-642-21455-4 |
79 | ″ | schema:name | Formal Methods for Eternal Networked Software Systems |
80 | ″ | rdf:type | schema:Book |
81 | N64fd369a66a74b5b8eb21360006c335c | schema:familyName | Bernardo |
82 | ″ | schema:givenName | Marco |
83 | ″ | rdf:type | schema:Person |
84 | N7e61902ba4724095b0e792ed4f633729 | schema:name | doi |
85 | ″ | schema:value | 10.1007/978-3-642-21455-4_3 |
86 | ″ | rdf:type | schema:PropertyValue |
87 | N7fd25a350cd0414290e0da142dba03e1 | rdf:first | N80d3ad263ebd462d8d3d083fd79fc3f9 |
88 | ″ | rdf:rest | rdf:nil |
89 | N80d3ad263ebd462d8d3d083fd79fc3f9 | schema:familyName | Issarny |
90 | ″ | schema:givenName | Valérie |
91 | ″ | rdf:type | schema:Person |
92 | N910852dacb69496188eaeba276d51bc0 | schema:name | dimensions_id |
93 | ″ | schema:value | pub.1043781609 |
94 | ″ | rdf:type | schema:PropertyValue |
95 | Nbce2b5e0e0cd4f4aaf6c08f9aea1851b | rdf:first | sg:person.014007552600.37 |
96 | ″ | rdf:rest | rdf:nil |
97 | Nbd3396dc78264cf598a25e511d965bde | schema:name | Springer Nature - SN SciGraph project |
98 | ″ | rdf:type | schema:Organization |
99 | Ncf446774679445a1b25461a5c935fccd | rdf:first | sg:person.012103627631.41 |
100 | ″ | rdf:rest | Ne0c03754794c4bf8a4613ce5d7144b97 |
101 | Ne0c03754794c4bf8a4613ce5d7144b97 | rdf:first | sg:person.011375012273.39 |
102 | ″ | rdf:rest | N1d972b2c8b504fd69f10333e722d888a |
103 | Neb7da2be22b54db2995712cb0a1251d4 | schema:name | Springer Nature |
104 | ″ | rdf:type | schema:Organisation |
105 | Nf18bd651404248a882fcad3c9836f51f | rdf:first | N64fd369a66a74b5b8eb21360006c335c |
106 | ″ | rdf:rest | N7fd25a350cd0414290e0da142dba03e1 |
107 | anzsrc-for:08 | schema:inDefinedTermSet | anzsrc-for: |
108 | ″ | schema:name | Information and Computing Sciences |
109 | ″ | rdf:type | schema:DefinedTerm |
110 | anzsrc-for:0801 | schema:inDefinedTermSet | anzsrc-for: |
111 | ″ | schema:name | Artificial Intelligence and Image Processing |
112 | ″ | rdf:type | schema:DefinedTerm |
113 | anzsrc-for:0802 | schema:inDefinedTermSet | anzsrc-for: |
114 | ″ | schema:name | Computation Theory and Mathematics |
115 | ″ | rdf:type | schema:DefinedTerm |
116 | anzsrc-for:0803 | schema:inDefinedTermSet | anzsrc-for: |
117 | ″ | schema:name | Computer Software |
118 | ″ | rdf:type | schema:DefinedTerm |
119 | sg:person.011375012273.39 | schema:affiliation | grid-institutes:grid.4991.5 |
120 | ″ | schema:familyName | Kwiatkowska |
121 | ″ | schema:givenName | Marta |
122 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39 |
123 | ″ | rdf:type | schema:Person |
124 | sg:person.012103627631.41 | schema:affiliation | grid-institutes:grid.4991.5 |
125 | ″ | schema:familyName | Forejt |
126 | ″ | schema:givenName | Vojtěch |
127 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012103627631.41 |
128 | ″ | rdf:type | schema:Person |
129 | sg:person.014007552600.37 | schema:affiliation | grid-institutes:grid.4991.5 |
130 | ″ | schema:familyName | Parker |
131 | ″ | schema:givenName | David |
132 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37 |
133 | ″ | rdf:type | schema:Person |
134 | sg:person.016323171577.36 | schema:affiliation | grid-institutes:grid.8756.c |
135 | ″ | schema:familyName | Norman |
136 | ″ | schema:givenName | Gethin |
137 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36 |
138 | ″ | rdf:type | schema:Person |
139 | grid-institutes:grid.4991.5 | schema:alternateName | Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK |
140 | ″ | schema:name | Oxford University Computing Laboratory, Parks Road, OX1 3QD, Oxford, UK |
141 | ″ | rdf:type | schema:Organization |
142 | grid-institutes:grid.8756.c | schema:alternateName | School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK |
143 | ″ | schema:name | School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK |
144 | ″ | rdf:type | schema:Organization |