Probabilistic Model Checking: Advances and Applications View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2017-06-22

AUTHORS

Marta Kwiatkowska , Gethin Norman , David Parker

ABSTRACT

Probabilistic model checking is a powerful technique for formally verifying quantitative properties of systems that exhibit stochastic behaviour. Such systems are found in many application domains: for example, probabilistic behaviour may arise due to the presence of failures in unreliable hardware, message loss in wireless communication channels, or the use of randomisation in distributed protocols. This chapter starts with an introduction to the technique of probabilistic model checking. We then survey some recent advances in the area, including controller synthesis, compositional verification, probabilistic real-time systems and parametric model checking. We illustrate the application of the various techniques with a combination of toy examples and descriptions of larger case studies. The chapter concludes with a discussion of some of the key challenges in the field. More... »

PAGES

73-121

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-57685-5_3

DOI

http://dx.doi.org/10.1007/978-3-319-57685-5_3

DIMENSIONS

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


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/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": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, 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, Glasgow, UK", 
          "id": "http://www.grid.ac/institutes/grid.8756.c", 
          "name": [
            "School of Computing Science, University of Glasgow, 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": "School of Computer Science, University of Birmingham, Birmingham, UK", 
          "id": "http://www.grid.ac/institutes/grid.6572.6", 
          "name": [
            "School of Computer Science, University of Birmingham, Birmingham, 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": "2017-06-22", 
    "datePublishedReg": "2017-06-22", 
    "description": "Probabilistic model checking is a powerful technique for formally verifying quantitative properties of systems that exhibit stochastic behaviour. Such systems are found in many application domains: for example, probabilistic behaviour may arise due to the presence of failures in unreliable hardware, message loss in wireless communication channels, or the use of randomisation in distributed protocols. This chapter starts with an introduction to the technique of probabilistic model checking. We then survey some recent advances in the area, including controller synthesis, compositional verification, probabilistic real-time systems and parametric model checking. We illustrate the application of the various techniques with a combination of toy examples and descriptions of larger case studies. The chapter concludes with a discussion of some of the key challenges in the field.", 
    "editor": [
      {
        "familyName": "Drechsler", 
        "givenName": "Rolf", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-57685-5_3", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-319-57683-1", 
        "978-3-319-57685-5"
      ], 
      "name": "Formal System Verification", 
      "type": "Book"
    }, 
    "keywords": [
      "probabilistic model checking", 
      "model checking", 
      "probabilistic real-time systems", 
      "real-time systems", 
      "Parametric Model Checking", 
      "presence of failures", 
      "wireless communication channels", 
      "unreliable hardware", 
      "application domains", 
      "compositional verification", 
      "large case study", 
      "message loss", 
      "communication channels", 
      "use of randomisation", 
      "toy example", 
      "checking", 
      "such systems", 
      "probabilistic behavior", 
      "key challenges", 
      "controller synthesis", 
      "quantitative properties", 
      "hardware", 
      "powerful technique", 
      "case study", 
      "stochastic behavior", 
      "system", 
      "applications", 
      "verification", 
      "technique", 
      "example", 
      "protocol", 
      "recent advances", 
      "advances", 
      "challenges", 
      "domain", 
      "channels", 
      "description", 
      "chapter", 
      "use", 
      "field", 
      "behavior", 
      "introduction", 
      "area", 
      "combination", 
      "discussion", 
      "failure", 
      "properties", 
      "loss", 
      "study", 
      "presence", 
      "synthesis", 
      "randomisation"
    ], 
    "name": "Probabilistic Model Checking: Advances and Applications", 
    "pagination": "73-121", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1086140835"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-57685-5_3"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-57685-5_3", 
      "https://app.dimensions.ai/details/publication/pub.1086140835"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-01-01T19:12", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220101/entities/gbq_results/chapter/chapter_209.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-57685-5_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-319-57685-5_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-319-57685-5_3'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-57685-5_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-319-57685-5_3'


 

This table displays all metadata directly associated to this object as RDF triples.

136 TRIPLES      23 PREDICATES      77 URIs      69 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-57685-5_3 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 anzsrc-for:0803
4 schema:author N0781294f3f554612baa07fad1577ffdd
5 schema:datePublished 2017-06-22
6 schema:datePublishedReg 2017-06-22
7 schema:description Probabilistic model checking is a powerful technique for formally verifying quantitative properties of systems that exhibit stochastic behaviour. Such systems are found in many application domains: for example, probabilistic behaviour may arise due to the presence of failures in unreliable hardware, message loss in wireless communication channels, or the use of randomisation in distributed protocols. This chapter starts with an introduction to the technique of probabilistic model checking. We then survey some recent advances in the area, including controller synthesis, compositional verification, probabilistic real-time systems and parametric model checking. We illustrate the application of the various techniques with a combination of toy examples and descriptions of larger case studies. The chapter concludes with a discussion of some of the key challenges in the field.
8 schema:editor N175f5da647984d00b3358579bd6a472b
9 schema:genre chapter
10 schema:inLanguage en
11 schema:isAccessibleForFree false
12 schema:isPartOf N1922113b75014754936a632b8fc48824
13 schema:keywords Parametric Model Checking
14 advances
15 application domains
16 applications
17 area
18 behavior
19 case study
20 challenges
21 channels
22 chapter
23 checking
24 combination
25 communication channels
26 compositional verification
27 controller synthesis
28 description
29 discussion
30 domain
31 example
32 failure
33 field
34 hardware
35 introduction
36 key challenges
37 large case study
38 loss
39 message loss
40 model checking
41 powerful technique
42 presence
43 presence of failures
44 probabilistic behavior
45 probabilistic model checking
46 probabilistic real-time systems
47 properties
48 protocol
49 quantitative properties
50 randomisation
51 real-time systems
52 recent advances
53 stochastic behavior
54 study
55 such systems
56 synthesis
57 system
58 technique
59 toy example
60 unreliable hardware
61 use
62 use of randomisation
63 verification
64 wireless communication channels
65 schema:name Probabilistic Model Checking: Advances and Applications
66 schema:pagination 73-121
67 schema:productId N70505db7097b4721a7496f3d2f709902
68 N8ea3ab4bfb4c4d84ba37384e41b58ff3
69 schema:publisher N10f1296d7460436b8ba45dd5ab1ee8ea
70 schema:sameAs https://app.dimensions.ai/details/publication/pub.1086140835
71 https://doi.org/10.1007/978-3-319-57685-5_3
72 schema:sdDatePublished 2022-01-01T19:12
73 schema:sdLicense https://scigraph.springernature.com/explorer/license/
74 schema:sdPublisher N12cfb32cdc3246a48ff669d232df080d
75 schema:url https://doi.org/10.1007/978-3-319-57685-5_3
76 sgo:license sg:explorer/license/
77 sgo:sdDataset chapters
78 rdf:type schema:Chapter
79 N0781294f3f554612baa07fad1577ffdd rdf:first sg:person.011375012273.39
80 rdf:rest Ne0cc0fa67fbd4d6cb66b7aba63b5ec6b
81 N10f1296d7460436b8ba45dd5ab1ee8ea schema:name Springer Nature
82 rdf:type schema:Organisation
83 N12cfb32cdc3246a48ff669d232df080d schema:name Springer Nature - SN SciGraph project
84 rdf:type schema:Organization
85 N175f5da647984d00b3358579bd6a472b rdf:first N3d10a46f15804e1e87b4db91f5dd5892
86 rdf:rest rdf:nil
87 N1922113b75014754936a632b8fc48824 schema:isbn 978-3-319-57683-1
88 978-3-319-57685-5
89 schema:name Formal System Verification
90 rdf:type schema:Book
91 N3d10a46f15804e1e87b4db91f5dd5892 schema:familyName Drechsler
92 schema:givenName Rolf
93 rdf:type schema:Person
94 N70505db7097b4721a7496f3d2f709902 schema:name dimensions_id
95 schema:value pub.1086140835
96 rdf:type schema:PropertyValue
97 N8ea3ab4bfb4c4d84ba37384e41b58ff3 schema:name doi
98 schema:value 10.1007/978-3-319-57685-5_3
99 rdf:type schema:PropertyValue
100 Nc8d26f847d594775b4cb930525573f06 rdf:first sg:person.014007552600.37
101 rdf:rest rdf:nil
102 Ne0cc0fa67fbd4d6cb66b7aba63b5ec6b rdf:first sg:person.016323171577.36
103 rdf:rest Nc8d26f847d594775b4cb930525573f06
104 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
105 schema:name Information and Computing Sciences
106 rdf:type schema:DefinedTerm
107 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
108 schema:name Computation Theory and Mathematics
109 rdf:type schema:DefinedTerm
110 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
111 schema:name Computer Software
112 rdf:type schema:DefinedTerm
113 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
114 schema:familyName Kwiatkowska
115 schema:givenName Marta
116 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
117 rdf:type schema:Person
118 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
119 schema:familyName Parker
120 schema:givenName David
121 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
122 rdf:type schema:Person
123 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
124 schema:familyName Norman
125 schema:givenName Gethin
126 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
127 rdf:type schema:Person
128 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, Oxford, UK
129 schema:name Department of Computer Science, University of Oxford, Oxford, UK
130 rdf:type schema:Organization
131 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, Birmingham, UK
132 schema:name School of Computer Science, University of Birmingham, Birmingham, UK
133 rdf:type schema:Organization
134 grid-institutes:grid.8756.c schema:alternateName School of Computing Science, University of Glasgow, Glasgow, UK
135 schema:name School of Computing Science, University of Glasgow, Glasgow, UK
136 rdf:type schema:Organization
 




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


...