Automated Verification Techniques for Probabilistic Systems View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2011

AUTHORS

Vojtěch Forejt , Marta Kwiatkowska , Gethin Norman , David Parker

ABSTRACT

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. More... »

PAGES

53-113

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-21455-4_3

DOI

http://dx.doi.org/10.1007/978-3-642-21455-4_3

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1043781609


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

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

HOW TO GET THIS DATA PROGRAMMATICALLY:

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
 




Preview window. Press ESC to close (or click here)


...