Automated Verification and Strategy Synthesis for Probabilistic Systems View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2013

AUTHORS

Marta Kwiatkowska , David Parker

ABSTRACT

Probabilistic model checking is an automated technique to verify whether a probabilistic system, e.g., a distributed network protocol which can exhibit failures, satisfies a temporal logic property, for example, “the minimum probability of the network recovering from a fault in a given time period is above 0.98”. Dually, we can also synthesise, from a model and a property specification, a strategy for controlling the system in order to satisfy or optimise the property, but this aspect has received less attention to date. In this paper, we give an overview of methods for automated verification and strategy synthesis for probabilistic systems. Primarily, we focus on the model of Markov decision processes and use property specifications based on probabilistic LTL and expected reward objectives. We also describe how to apply multi-objective model checking to investigate trade-offs between several properties, and extensions to stochastic multi-player games. The paper concludes with a summary of future challenges in this area. More... »

PAGES

5-22

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-02444-8_2

DOI

http://dx.doi.org/10.1007/978-3-319-02444-8_2

DIMENSIONS

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


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": "Department of Computer Science, University of Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of 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 Computer Science, University of Birmingham, UK", 
          "id": "http://www.grid.ac/institutes/grid.6572.6", 
          "name": [
            "School of Computer Science, University of 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": "2013", 
    "datePublishedReg": "2013-01-01", 
    "description": "Probabilistic model checking is an automated technique to verify whether a probabilistic system, e.g., a distributed network protocol which can exhibit failures, satisfies a temporal logic property, for example, \u201cthe minimum probability of the network recovering from a fault in a given time period is above 0.98\u201d. Dually, we can also synthesise, from a model and a property specification, a strategy for controlling the system in order to satisfy or optimise the property, but this aspect has received less attention to date. In this paper, we give an overview of methods for automated verification and strategy synthesis for probabilistic systems. Primarily, we focus on the model of Markov decision processes and use property specifications based on probabilistic LTL and expected reward objectives. We also describe how to apply multi-objective model checking to investigate trade-offs between several properties, and extensions to stochastic multi-player games. The paper concludes with a summary of future challenges in this area.", 
    "editor": [
      {
        "familyName": "Van Hung", 
        "givenName": "Dang", 
        "type": "Person"
      }, 
      {
        "familyName": "Ogawa", 
        "givenName": "Mizuhito", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-02444-8_2", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-319-02443-1", 
        "978-3-319-02444-8"
      ], 
      "name": "Automated Technology for Verification and Analysis", 
      "type": "Book"
    }, 
    "keywords": [
      "probabilistic systems", 
      "property specifications", 
      "stochastic multi-player games", 
      "multi-player games", 
      "probabilistic model checking", 
      "strategy synthesis", 
      "temporal logic properties", 
      "Markov decision process", 
      "network protocols", 
      "model checking", 
      "logic properties", 
      "multi-objective model", 
      "automated technique", 
      "reward objective", 
      "decision process", 
      "minimum probability", 
      "verification", 
      "specification", 
      "overview of methods", 
      "checking", 
      "system", 
      "network", 
      "LTL", 
      "game", 
      "model", 
      "protocol", 
      "future challenges", 
      "faults", 
      "challenges", 
      "less attention", 
      "technique", 
      "extension", 
      "satisfies", 
      "example", 
      "order", 
      "overview", 
      "method", 
      "probability", 
      "aspects", 
      "strategies", 
      "process", 
      "objective", 
      "attention", 
      "area", 
      "time period", 
      "properties", 
      "summary", 
      "failure", 
      "date", 
      "synthesis", 
      "period", 
      "paper", 
      "probabilistic LTL"
    ], 
    "name": "Automated Verification and Strategy Synthesis for Probabilistic Systems", 
    "pagination": "5-22", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1002450464"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-02444-8_2"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-02444-8_2", 
      "https://app.dimensions.ai/details/publication/pub.1002450464"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T20:10", 
    "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_442.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-02444-8_2"
  }
]
 

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-02444-8_2'

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-02444-8_2'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-02444-8_2'

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-02444-8_2'


 

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

136 TRIPLES      23 PREDICATES      81 URIs      72 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-02444-8_2 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 anzsrc-for:0803
5 schema:author N50ea28e849ed4b1d800f7e590de3125f
6 schema:datePublished 2013
7 schema:datePublishedReg 2013-01-01
8 schema:description Probabilistic model checking is an automated technique to verify whether a probabilistic system, e.g., a distributed network protocol which can exhibit failures, satisfies a temporal logic property, for example, “the minimum probability of the network recovering from a fault in a given time period is above 0.98”. Dually, we can also synthesise, from a model and a property specification, a strategy for controlling the system in order to satisfy or optimise the property, but this aspect has received less attention to date. In this paper, we give an overview of methods for automated verification and strategy synthesis for probabilistic systems. Primarily, we focus on the model of Markov decision processes and use property specifications based on probabilistic LTL and expected reward objectives. We also describe how to apply multi-objective model checking to investigate trade-offs between several properties, and extensions to stochastic multi-player games. The paper concludes with a summary of future challenges in this area.
9 schema:editor N7190b16fff9440d2bf595d2ca9ecb18b
10 schema:genre chapter
11 schema:inLanguage en
12 schema:isAccessibleForFree false
13 schema:isPartOf N21c5332e0a86404ca254563be5c1d25f
14 schema:keywords LTL
15 Markov decision process
16 area
17 aspects
18 attention
19 automated technique
20 challenges
21 checking
22 date
23 decision process
24 example
25 extension
26 failure
27 faults
28 future challenges
29 game
30 less attention
31 logic properties
32 method
33 minimum probability
34 model
35 model checking
36 multi-objective model
37 multi-player games
38 network
39 network protocols
40 objective
41 order
42 overview
43 overview of methods
44 paper
45 period
46 probabilistic LTL
47 probabilistic model checking
48 probabilistic systems
49 probability
50 process
51 properties
52 property specifications
53 protocol
54 reward objective
55 satisfies
56 specification
57 stochastic multi-player games
58 strategies
59 strategy synthesis
60 summary
61 synthesis
62 system
63 technique
64 temporal logic properties
65 time period
66 verification
67 schema:name Automated Verification and Strategy Synthesis for Probabilistic Systems
68 schema:pagination 5-22
69 schema:productId N4c39873bfd5240d6a528af22f155f8e9
70 Nb7cff0991ab14402bce02b51908e0bb8
71 schema:publisher N409c8af12c574588a8ea3bad15decc9a
72 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002450464
73 https://doi.org/10.1007/978-3-319-02444-8_2
74 schema:sdDatePublished 2021-12-01T20:10
75 schema:sdLicense https://scigraph.springernature.com/explorer/license/
76 schema:sdPublisher Ne01d4fefa5244f6991d41c4af08f96de
77 schema:url https://doi.org/10.1007/978-3-319-02444-8_2
78 sgo:license sg:explorer/license/
79 sgo:sdDataset chapters
80 rdf:type schema:Chapter
81 N21c5332e0a86404ca254563be5c1d25f schema:isbn 978-3-319-02443-1
82 978-3-319-02444-8
83 schema:name Automated Technology for Verification and Analysis
84 rdf:type schema:Book
85 N409c8af12c574588a8ea3bad15decc9a schema:name Springer Nature
86 rdf:type schema:Organisation
87 N4c39873bfd5240d6a528af22f155f8e9 schema:name doi
88 schema:value 10.1007/978-3-319-02444-8_2
89 rdf:type schema:PropertyValue
90 N50ea28e849ed4b1d800f7e590de3125f rdf:first sg:person.011375012273.39
91 rdf:rest Nfff285544bad440f94b23655430202ed
92 N6f41caa0e13c4e39bbe6894510221f05 schema:familyName Ogawa
93 schema:givenName Mizuhito
94 rdf:type schema:Person
95 N7190b16fff9440d2bf595d2ca9ecb18b rdf:first Ne3d3c09ab1bb4c37a2f751a033b3bb11
96 rdf:rest N7b047a5672304fdc90ad508a4708e38d
97 N7b047a5672304fdc90ad508a4708e38d rdf:first N6f41caa0e13c4e39bbe6894510221f05
98 rdf:rest rdf:nil
99 Nb7cff0991ab14402bce02b51908e0bb8 schema:name dimensions_id
100 schema:value pub.1002450464
101 rdf:type schema:PropertyValue
102 Ne01d4fefa5244f6991d41c4af08f96de schema:name Springer Nature - SN SciGraph project
103 rdf:type schema:Organization
104 Ne3d3c09ab1bb4c37a2f751a033b3bb11 schema:familyName Van Hung
105 schema:givenName Dang
106 rdf:type schema:Person
107 Nfff285544bad440f94b23655430202ed rdf:first sg:person.014007552600.37
108 rdf:rest rdf:nil
109 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
110 schema:name Information and Computing Sciences
111 rdf:type schema:DefinedTerm
112 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
113 schema:name Artificial Intelligence and Image Processing
114 rdf:type schema:DefinedTerm
115 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
116 schema:name Computation Theory and Mathematics
117 rdf:type schema:DefinedTerm
118 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
119 schema:name Computer Software
120 rdf:type schema:DefinedTerm
121 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
122 schema:familyName Kwiatkowska
123 schema:givenName Marta
124 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
125 rdf:type schema:Person
126 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
127 schema:familyName Parker
128 schema:givenName David
129 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
130 rdf:type schema:Person
131 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, UK
132 schema:name Department of Computer Science, University of Oxford, UK
133 rdf:type schema:Organization
134 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, UK
135 schema:name School of Computer Science, University of Birmingham, UK
136 rdf:type schema:Organization
 




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


...