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": "2021-12-01T20:02", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211201/entities/gbq_results/chapter/chapter_264.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 Ndd8c5796dc1243ad8bc16f071811a181
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 N7f05f1c868b04d2ab21f8c93828df079
9 schema:genre chapter
10 schema:inLanguage en
11 schema:isAccessibleForFree false
12 schema:isPartOf N55e22759f6224759945e1b3633b383dd
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 N1157482ae5fc42abb76fcb6fac4a09d9
68 N3c973bdc1c3f4217b67ed6ee9660feb3
69 schema:publisher N78e1e903d7e4451b86b8ffbfd3940a4d
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 2021-12-01T20:02
73 schema:sdLicense https://scigraph.springernature.com/explorer/license/
74 schema:sdPublisher N845b3ff2dfc94e8cb756870188cdde57
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 N095730c74c6c45dfa4d9af5a51849723 schema:familyName Drechsler
80 schema:givenName Rolf
81 rdf:type schema:Person
82 N0c1af630539a428bbc3704ae058f2aa6 rdf:first sg:person.014007552600.37
83 rdf:rest rdf:nil
84 N1157482ae5fc42abb76fcb6fac4a09d9 schema:name doi
85 schema:value 10.1007/978-3-319-57685-5_3
86 rdf:type schema:PropertyValue
87 N2c5d4860a150498b9137b3e7a32720bf rdf:first sg:person.016323171577.36
88 rdf:rest N0c1af630539a428bbc3704ae058f2aa6
89 N3c973bdc1c3f4217b67ed6ee9660feb3 schema:name dimensions_id
90 schema:value pub.1086140835
91 rdf:type schema:PropertyValue
92 N55e22759f6224759945e1b3633b383dd schema:isbn 978-3-319-57683-1
93 978-3-319-57685-5
94 schema:name Formal System Verification
95 rdf:type schema:Book
96 N78e1e903d7e4451b86b8ffbfd3940a4d schema:name Springer Nature
97 rdf:type schema:Organisation
98 N7f05f1c868b04d2ab21f8c93828df079 rdf:first N095730c74c6c45dfa4d9af5a51849723
99 rdf:rest rdf:nil
100 N845b3ff2dfc94e8cb756870188cdde57 schema:name Springer Nature - SN SciGraph project
101 rdf:type schema:Organization
102 Ndd8c5796dc1243ad8bc16f071811a181 rdf:first sg:person.011375012273.39
103 rdf:rest N2c5d4860a150498b9137b3e7a32720bf
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)


...