Verification and Control of Partially Observable Probabilistic Real-Time Systems View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2015-08-22

AUTHORS

Gethin Norman , David Parker , Xueyi Zou

ABSTRACT

We propose automated techniques for the verification and control of probabilistic real-time systems that are only partially observable. To formally model such systems, we define an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. We give a probabilistic temporal logic that can express a range of quantitative properties of these models, relating to the probability of an event’s occurrence or the expected value of a reward measure. We then propose techniques to either verify that such a property holds or to synthesise a controller for the model which makes it true. Our approach is based on an integer discretisation of the model’s dense-time behaviour and a grid-based abstraction of the uncountable belief space induced by partial observability. The latter is necessarily approximate since the underlying problem is undecidable, however we show how both lower and upper bounds on numerical results can be generated. We illustrate the effectiveness of the approach by implementing it in the PRISM model checker and applying it to several case studies, from the domains of computer security and task scheduling. More... »

PAGES

240-255

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-22975-1_16

DOI

http://dx.doi.org/10.1007/978-3-319-22975-1_16

DIMENSIONS

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


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": "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"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of York, York, UK", 
          "id": "http://www.grid.ac/institutes/grid.5685.e", 
          "name": [
            "Department of Computer Science, University of York, York, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Zou", 
        "givenName": "Xueyi", 
        "id": "sg:person.013264431037.49", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013264431037.49"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2015-08-22", 
    "datePublishedReg": "2015-08-22", 
    "description": "We propose automated techniques for the verification and control of probabilistic real-time systems that are only partially observable. To formally model such systems, we define an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. We give a probabilistic temporal logic that can express a range of quantitative properties of these models, relating to the probability of an event\u2019s occurrence or the expected value of a reward measure. We then propose techniques to either verify that such a property holds or to synthesise a controller for the model which makes it true. Our approach is based on an integer discretisation of the model\u2019s dense-time behaviour and a grid-based abstraction of the uncountable belief space induced by partial observability. The latter is necessarily approximate since the underlying problem is undecidable, however we show how both lower and upper bounds on numerical results can be generated. We illustrate the effectiveness of the approach by implementing it in the PRISM model checker and applying it to several case studies, from the domains of computer security and task scheduling.", 
    "editor": [
      {
        "familyName": "Sankaranarayanan", 
        "givenName": "Sriram", 
        "type": "Person"
      }, 
      {
        "familyName": "Vicario", 
        "givenName": "Enrico", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-22975-1_16", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-22974-4", 
        "978-3-319-22975-1"
      ], 
      "name": "Formal Modeling and Analysis of Timed Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "probabilistic real-time systems", 
      "PRISM model checker", 
      "probabilistic temporal logic", 
      "real-time systems", 
      "extension of probabilistic", 
      "computer security", 
      "task scheduling", 
      "model checker", 
      "temporal logic", 
      "belief space", 
      "time systems", 
      "partial observability", 
      "such systems", 
      "reward measures", 
      "event occurrence", 
      "verification", 
      "quantitative properties", 
      "upper bounds", 
      "checker", 
      "controller", 
      "case study", 
      "scheduling", 
      "security", 
      "abstraction", 
      "system", 
      "probabilistic", 
      "local state", 
      "automata", 
      "logic", 
      "technique", 
      "model", 
      "observability", 
      "effectiveness", 
      "bounds", 
      "domain", 
      "space", 
      "extension", 
      "numerical results", 
      "probability", 
      "control", 
      "discretisation", 
      "state", 
      "results", 
      "Partially", 
      "latter", 
      "measures", 
      "behavior", 
      "observer", 
      "properties", 
      "values", 
      "range", 
      "study", 
      "occurrence", 
      "approach", 
      "problem"
    ], 
    "name": "Verification and Control of Partially Observable Probabilistic Real-Time Systems", 
    "pagination": "240-255", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1008952778"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-22975-1_16"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-22975-1_16", 
      "https://app.dimensions.ai/details/publication/pub.1008952778"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:52", 
    "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_427.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-22975-1_16"
  }
]
 

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-22975-1_16'

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-22975-1_16'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-22975-1_16'

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-22975-1_16'


 

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

148 TRIPLES      23 PREDICATES      82 URIs      73 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-22975-1_16 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 anzsrc-for:0803
5 schema:author Na57d9fe148c845b5a2564c8f97b03cb8
6 schema:datePublished 2015-08-22
7 schema:datePublishedReg 2015-08-22
8 schema:description We propose automated techniques for the verification and control of probabilistic real-time systems that are only partially observable. To formally model such systems, we define an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. We give a probabilistic temporal logic that can express a range of quantitative properties of these models, relating to the probability of an event’s occurrence or the expected value of a reward measure. We then propose techniques to either verify that such a property holds or to synthesise a controller for the model which makes it true. Our approach is based on an integer discretisation of the model’s dense-time behaviour and a grid-based abstraction of the uncountable belief space induced by partial observability. The latter is necessarily approximate since the underlying problem is undecidable, however we show how both lower and upper bounds on numerical results can be generated. We illustrate the effectiveness of the approach by implementing it in the PRISM model checker and applying it to several case studies, from the domains of computer security and task scheduling.
9 schema:editor Na9f4015532dc42879370e78fd16a5280
10 schema:genre chapter
11 schema:inLanguage en
12 schema:isAccessibleForFree true
13 schema:isPartOf N52591d30d6ae48ab8d1d6631d6edb73c
14 schema:keywords PRISM model checker
15 Partially
16 abstraction
17 approach
18 automata
19 behavior
20 belief space
21 bounds
22 case study
23 checker
24 computer security
25 control
26 controller
27 discretisation
28 domain
29 effectiveness
30 event occurrence
31 extension
32 extension of probabilistic
33 latter
34 local state
35 logic
36 measures
37 model
38 model checker
39 numerical results
40 observability
41 observer
42 occurrence
43 partial observability
44 probabilistic
45 probabilistic real-time systems
46 probabilistic temporal logic
47 probability
48 problem
49 properties
50 quantitative properties
51 range
52 real-time systems
53 results
54 reward measures
55 scheduling
56 security
57 space
58 state
59 study
60 such systems
61 system
62 task scheduling
63 technique
64 temporal logic
65 time systems
66 upper bounds
67 values
68 verification
69 schema:name Verification and Control of Partially Observable Probabilistic Real-Time Systems
70 schema:pagination 240-255
71 schema:productId N4605efef869b4ce2b61634af355867ab
72 N5ef3bbb1a4fa4111a87a4cce85045195
73 schema:publisher Ne0b83c40e01d4eccad007087dcd9b5c8
74 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008952778
75 https://doi.org/10.1007/978-3-319-22975-1_16
76 schema:sdDatePublished 2022-05-10T10:52
77 schema:sdLicense https://scigraph.springernature.com/explorer/license/
78 schema:sdPublisher N1483f1fcb4ca4692a674e9a00435dba1
79 schema:url https://doi.org/10.1007/978-3-319-22975-1_16
80 sgo:license sg:explorer/license/
81 sgo:sdDataset chapters
82 rdf:type schema:Chapter
83 N02201c635c814358b38b1024f127d85f rdf:first sg:person.013264431037.49
84 rdf:rest rdf:nil
85 N1483f1fcb4ca4692a674e9a00435dba1 schema:name Springer Nature - SN SciGraph project
86 rdf:type schema:Organization
87 N4605efef869b4ce2b61634af355867ab schema:name doi
88 schema:value 10.1007/978-3-319-22975-1_16
89 rdf:type schema:PropertyValue
90 N52591d30d6ae48ab8d1d6631d6edb73c schema:isbn 978-3-319-22974-4
91 978-3-319-22975-1
92 schema:name Formal Modeling and Analysis of Timed Systems
93 rdf:type schema:Book
94 N5ef3bbb1a4fa4111a87a4cce85045195 schema:name dimensions_id
95 schema:value pub.1008952778
96 rdf:type schema:PropertyValue
97 N6f7b4a21a48c494e9e9b331bf6399073 schema:familyName Sankaranarayanan
98 schema:givenName Sriram
99 rdf:type schema:Person
100 N99ddbbc8bb0e468490b0f9616d9f60d7 schema:familyName Vicario
101 schema:givenName Enrico
102 rdf:type schema:Person
103 Na57d9fe148c845b5a2564c8f97b03cb8 rdf:first sg:person.016323171577.36
104 rdf:rest Nb044748a4ee64ba7bec6075a7a711b01
105 Na783c6e6108c474cb239b9c55a66b619 rdf:first N99ddbbc8bb0e468490b0f9616d9f60d7
106 rdf:rest rdf:nil
107 Na9f4015532dc42879370e78fd16a5280 rdf:first N6f7b4a21a48c494e9e9b331bf6399073
108 rdf:rest Na783c6e6108c474cb239b9c55a66b619
109 Nb044748a4ee64ba7bec6075a7a711b01 rdf:first sg:person.014007552600.37
110 rdf:rest N02201c635c814358b38b1024f127d85f
111 Ne0b83c40e01d4eccad007087dcd9b5c8 schema:name Springer Nature
112 rdf:type schema:Organisation
113 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
114 schema:name Information and Computing Sciences
115 rdf:type schema:DefinedTerm
116 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
117 schema:name Artificial Intelligence and Image Processing
118 rdf:type schema:DefinedTerm
119 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
120 schema:name Computation Theory and Mathematics
121 rdf:type schema:DefinedTerm
122 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
123 schema:name Computer Software
124 rdf:type schema:DefinedTerm
125 sg:person.013264431037.49 schema:affiliation grid-institutes:grid.5685.e
126 schema:familyName Zou
127 schema:givenName Xueyi
128 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013264431037.49
129 rdf:type schema:Person
130 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
131 schema:familyName Parker
132 schema:givenName David
133 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
134 rdf:type schema:Person
135 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
136 schema:familyName Norman
137 schema:givenName Gethin
138 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
139 rdf:type schema:Person
140 grid-institutes:grid.5685.e schema:alternateName Department of Computer Science, University of York, York, UK
141 schema:name Department of Computer Science, University of York, York, UK
142 rdf:type schema:Organization
143 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, Birmingham, UK
144 schema:name School of Computer Science, University of Birmingham, Birmingham, UK
145 rdf:type schema:Organization
146 grid-institutes:grid.8756.c schema:alternateName School of Computing Science, University of Glasgow, Glasgow, UK
147 schema:name School of Computing Science, University of Glasgow, Glasgow, UK
148 rdf:type schema:Organization
 




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


...