Verification of Markov Decision Processes Using Learning Algorithms View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2014

AUTHORS

Tomáš Brázdil , Krishnendu Chatterjee , Martin Chmelík , Vojtěch Forejt , Jan Křetínský , Marta Kwiatkowska , David Parker , Mateusz Ujma

ABSTRACT

We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties in MDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples. More... »

PAGES

98-114

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-11936-6_8

DOI

http://dx.doi.org/10.1007/978-3-319-11936-6_8

DIMENSIONS

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


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/01", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Mathematical Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "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/0104", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Statistics", 
        "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"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Br\u00e1zdil", 
        "givenName": "Tom\u00e1\u0161", 
        "id": "sg:person.013233626146.14", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013233626146.14"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "IST, Austria", 
          "id": "http://www.grid.ac/institutes/None", 
          "name": [
            "IST, Austria"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Chatterjee", 
        "givenName": "Krishnendu", 
        "id": "sg:person.01046624377.36", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01046624377.36"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "IST, Austria", 
          "id": "http://www.grid.ac/institutes/None", 
          "name": [
            "IST, Austria"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Chmel\u00edk", 
        "givenName": "Martin", 
        "id": "sg:person.012613237527.39", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012613237527.39"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "University of 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": "IST, Austria", 
          "id": "http://www.grid.ac/institutes/None", 
          "name": [
            "IST, Austria"
          ], 
          "type": "Organization"
        }, 
        "familyName": "K\u0159et\u00ednsk\u00fd", 
        "givenName": "Jan", 
        "id": "sg:person.012551375660.17", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012551375660.17"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "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": "University of Birmingham, UK", 
          "id": "http://www.grid.ac/institutes/grid.6572.6", 
          "name": [
            "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"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "University of Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Ujma", 
        "givenName": "Mateusz", 
        "id": "sg:person.011443107516.15", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011443107516.15"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2014", 
    "datePublishedReg": "2014-01-01", 
    "description": "We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties in MDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples.", 
    "editor": [
      {
        "familyName": "Cassez", 
        "givenName": "Franck", 
        "type": "Person"
      }, 
      {
        "familyName": "Raskin", 
        "givenName": "Jean-Fran\u00e7ois", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-11936-6_8", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-11935-9", 
        "978-3-319-11936-6"
      ], 
      "name": "Automated Technology for Verification and Analysis", 
      "type": "Book"
    }, 
    "keywords": [
      "Markov decision process", 
      "machine-learning algorithms", 
      "upper bounds", 
      "decision process", 
      "distinct instantiations", 
      "probabilistic guarantees", 
      "LTL objectives", 
      "exhaustive exploration", 
      "state space", 
      "statistical model", 
      "unbounded properties", 
      "partial exploration", 
      "probabilistic reachability", 
      "general framework", 
      "verification", 
      "algorithm", 
      "experimental results", 
      "first extension", 
      "full knowledge", 
      "related techniques", 
      "framework", 
      "bounds", 
      "particular properties", 
      "instantiation", 
      "guarantees", 
      "reachability", 
      "performance", 
      "primary goal", 
      "approximation", 
      "technique", 
      "exploration", 
      "model", 
      "space", 
      "core properties", 
      "probability", 
      "goal", 
      "extension", 
      "properties", 
      "example", 
      "process", 
      "approach", 
      "knowledge", 
      "terms", 
      "method", 
      "latter", 
      "criteria", 
      "objective", 
      "results", 
      "cases", 
      "contrast", 
      "heuristic-driven partial exploration"
    ], 
    "name": "Verification of Markov Decision Processes Using Learning Algorithms", 
    "pagination": "98-114", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1002629652"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-11936-6_8"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-11936-6_8", 
      "https://app.dimensions.ai/details/publication/pub.1002629652"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-11-01T18:59", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211101/entities/gbq_results/chapter/chapter_41.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-11936-6_8"
  }
]
 

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-11936-6_8'

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-11936-6_8'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-11936-6_8'

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-11936-6_8'


 

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

182 TRIPLES      23 PREDICATES      79 URIs      70 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-11936-6_8 schema:about anzsrc-for:01
2 anzsrc-for:0104
3 anzsrc-for:08
4 anzsrc-for:0801
5 schema:author N4252112712f34914a8412778e8b6df48
6 schema:datePublished 2014
7 schema:datePublishedReg 2014-01-01
8 schema:description We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties in MDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples.
9 schema:editor N247ffe7f71a346f39d7068bb77b85f6a
10 schema:genre chapter
11 schema:inLanguage en
12 schema:isAccessibleForFree true
13 schema:isPartOf N453c157c26214bff863c74874899bc34
14 schema:keywords LTL objectives
15 Markov decision process
16 algorithm
17 approach
18 approximation
19 bounds
20 cases
21 contrast
22 core properties
23 criteria
24 decision process
25 distinct instantiations
26 example
27 exhaustive exploration
28 experimental results
29 exploration
30 extension
31 first extension
32 framework
33 full knowledge
34 general framework
35 goal
36 guarantees
37 heuristic-driven partial exploration
38 instantiation
39 knowledge
40 latter
41 machine-learning algorithms
42 method
43 model
44 objective
45 partial exploration
46 particular properties
47 performance
48 primary goal
49 probabilistic guarantees
50 probabilistic reachability
51 probability
52 process
53 properties
54 reachability
55 related techniques
56 results
57 space
58 state space
59 statistical model
60 technique
61 terms
62 unbounded properties
63 upper bounds
64 verification
65 schema:name Verification of Markov Decision Processes Using Learning Algorithms
66 schema:pagination 98-114
67 schema:productId N4c53cb00c1154b659f0f2d8b5a5e2ddd
68 N92339a2aed4244e5bb7e6ab5c801edc6
69 schema:publisher N54854513a9fb4345a3131971a0e67761
70 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002629652
71 https://doi.org/10.1007/978-3-319-11936-6_8
72 schema:sdDatePublished 2021-11-01T18:59
73 schema:sdLicense https://scigraph.springernature.com/explorer/license/
74 schema:sdPublisher N08aa5c2535084a84b8f67cbe6bdb45cf
75 schema:url https://doi.org/10.1007/978-3-319-11936-6_8
76 sgo:license sg:explorer/license/
77 sgo:sdDataset chapters
78 rdf:type schema:Chapter
79 N0328d8ba042742ccb6d9f3e97a4d8914 rdf:first sg:person.011375012273.39
80 rdf:rest N48e9b6634dfd49acac7f09d658760c66
81 N08aa5c2535084a84b8f67cbe6bdb45cf schema:name Springer Nature - SN SciGraph project
82 rdf:type schema:Organization
83 N247ffe7f71a346f39d7068bb77b85f6a rdf:first N476305486c104a6cb6875ed61d939f32
84 rdf:rest N56a00d2e20ae4f6c91f001d38ade8870
85 N3f2cf9587d5540d99252318e5a001152 rdf:first sg:person.01046624377.36
86 rdf:rest N69f95286f2244f418170b00f26e19ebd
87 N4252112712f34914a8412778e8b6df48 rdf:first sg:person.013233626146.14
88 rdf:rest N3f2cf9587d5540d99252318e5a001152
89 N450e6359894b42839413eb531d09b06e rdf:first sg:person.011443107516.15
90 rdf:rest rdf:nil
91 N453c157c26214bff863c74874899bc34 schema:isbn 978-3-319-11935-9
92 978-3-319-11936-6
93 schema:name Automated Technology for Verification and Analysis
94 rdf:type schema:Book
95 N476305486c104a6cb6875ed61d939f32 schema:familyName Cassez
96 schema:givenName Franck
97 rdf:type schema:Person
98 N48e9b6634dfd49acac7f09d658760c66 rdf:first sg:person.014007552600.37
99 rdf:rest N450e6359894b42839413eb531d09b06e
100 N4c53cb00c1154b659f0f2d8b5a5e2ddd schema:name doi
101 schema:value 10.1007/978-3-319-11936-6_8
102 rdf:type schema:PropertyValue
103 N54854513a9fb4345a3131971a0e67761 schema:name Springer Nature
104 rdf:type schema:Organisation
105 N56a00d2e20ae4f6c91f001d38ade8870 rdf:first Ne25df9795812414782a77b18677110f7
106 rdf:rest rdf:nil
107 N69f95286f2244f418170b00f26e19ebd rdf:first sg:person.012613237527.39
108 rdf:rest Nfa0b8eac13484d2ba7b75ef8605bfb66
109 N86938b6d05c84b068bf08a0ada51dac8 rdf:first sg:person.012551375660.17
110 rdf:rest N0328d8ba042742ccb6d9f3e97a4d8914
111 N92339a2aed4244e5bb7e6ab5c801edc6 schema:name dimensions_id
112 schema:value pub.1002629652
113 rdf:type schema:PropertyValue
114 Ne25df9795812414782a77b18677110f7 schema:familyName Raskin
115 schema:givenName Jean-François
116 rdf:type schema:Person
117 Nfa0b8eac13484d2ba7b75ef8605bfb66 rdf:first sg:person.012103627631.41
118 rdf:rest N86938b6d05c84b068bf08a0ada51dac8
119 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
120 schema:name Mathematical Sciences
121 rdf:type schema:DefinedTerm
122 anzsrc-for:0104 schema:inDefinedTermSet anzsrc-for:
123 schema:name Statistics
124 rdf:type schema:DefinedTerm
125 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
126 schema:name Information and Computing Sciences
127 rdf:type schema:DefinedTerm
128 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
129 schema:name Artificial Intelligence and Image Processing
130 rdf:type schema:DefinedTerm
131 sg:person.01046624377.36 schema:affiliation grid-institutes:None
132 schema:familyName Chatterjee
133 schema:givenName Krishnendu
134 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01046624377.36
135 rdf:type schema:Person
136 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
137 schema:familyName Kwiatkowska
138 schema:givenName Marta
139 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
140 rdf:type schema:Person
141 sg:person.011443107516.15 schema:affiliation grid-institutes:grid.4991.5
142 schema:familyName Ujma
143 schema:givenName Mateusz
144 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011443107516.15
145 rdf:type schema:Person
146 sg:person.012103627631.41 schema:affiliation grid-institutes:grid.4991.5
147 schema:familyName Forejt
148 schema:givenName Vojtěch
149 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012103627631.41
150 rdf:type schema:Person
151 sg:person.012551375660.17 schema:affiliation grid-institutes:None
152 schema:familyName Křetínský
153 schema:givenName Jan
154 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012551375660.17
155 rdf:type schema:Person
156 sg:person.012613237527.39 schema:affiliation grid-institutes:None
157 schema:familyName Chmelík
158 schema:givenName Martin
159 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012613237527.39
160 rdf:type schema:Person
161 sg:person.013233626146.14 schema:affiliation grid-institutes:grid.10267.32
162 schema:familyName Brázdil
163 schema:givenName Tomáš
164 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013233626146.14
165 rdf:type schema:Person
166 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
167 schema:familyName Parker
168 schema:givenName David
169 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
170 rdf:type schema:Person
171 grid-institutes:None schema:alternateName IST, Austria
172 schema:name IST, Austria
173 rdf:type schema:Organization
174 grid-institutes:grid.10267.32 schema:alternateName Masaryk University, Brno, Czech Republic
175 schema:name Masaryk University, Brno, Czech Republic
176 rdf:type schema:Organization
177 grid-institutes:grid.4991.5 schema:alternateName University of Oxford, UK
178 schema:name University of Oxford, UK
179 rdf:type schema:Organization
180 grid-institutes:grid.6572.6 schema:alternateName University of Birmingham, UK
181 schema:name University of Birmingham, UK
182 rdf:type schema:Organization
 




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


...