Ontology type: schema:ScholarlyArticle Open Access: True
2017-03-08
AUTHORSGethin Norman, David Parker, Xueyi Zou
ABSTRACTWe present automated techniques for the verification and control of partially observable, probabilistic systems for both discrete and dense models of time. For the discrete-time case, we formally model these systems using partially observable Markov decision processes; for dense time, we propose an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. We give probabilistic temporal logics 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 synthesise a controller for the model which makes it true. Our approach is based on a grid-based abstraction of the uncountable belief space induced by partial observability and, for dense-time models, an integer discretisation of real-time behaviour. The former 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 task and network scheduling, computer security and planning. More... »
PAGES354-402
http://scigraph.springernature.com/pub.10.1007/s11241-017-9269-4
DOIhttp://dx.doi.org/10.1007/s11241-017-9269-4
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1084030499
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"
}
],
"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"
}
],
"citation": [
{
"id": "sg:pub.10.1007/3-540-45351-2_15",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1002788038",
"https://doi.org/10.1007/3-540-45351-2_15"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/s11134-015-9439-9",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1004357064",
"https://doi.org/10.1007/s11134-015-9439-9"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/bf01211866",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1052049375",
"https://doi.org/10.1007/bf01211866"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/1-4020-8141-3_38",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1005039352",
"https://doi.org/10.1007/1-4020-8141-3_38"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-75596-8_15",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1033876286",
"https://doi.org/10.1007/978-3-540-75596-8_15"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/s10703-005-1632-8",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1017423314",
"https://doi.org/10.1007/s10703-005-1632-8"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-642-33386-6_26",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1033136361",
"https://doi.org/10.1007/978-3-642-33386-6_26"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-642-22110-1_20",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1044108353",
"https://doi.org/10.1007/978-3-642-22110-1_20"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-55719-9_103",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1006689972",
"https://doi.org/10.1007/3-540-55719-9_103"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/bf00206326",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1041027293",
"https://doi.org/10.1007/bf00206326"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-642-28756-5_27",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1004752029",
"https://doi.org/10.1007/978-3-642-28756-5_27"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-642-46516-1",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1043772236",
"https://doi.org/10.1007/978-3-642-46516-1"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-642-21455-4_3",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1043781609",
"https://doi.org/10.1007/978-3-642-21455-4_3"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-1-4684-9455-6",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1003855982",
"https://doi.org/10.1007/978-1-4684-9455-6"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-45069-6_18",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1002688616",
"https://doi.org/10.1007/978-3-540-45069-6_18"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/bfb0015027",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1023196586",
"https://doi.org/10.1007/bfb0015027"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-319-22975-1_16",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1008952778",
"https://doi.org/10.1007/978-3-319-22975-1_16"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/s10703-012-0177-x",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1047241468",
"https://doi.org/10.1007/s10703-012-0177-x"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-642-22110-1_47",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1027900693",
"https://doi.org/10.1007/978-3-642-22110-1_47"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1023/a:1008739929481",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1040056258",
"https://doi.org/10.1023/a:1008739929481"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/s10458-012-9200-2",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1037579583",
"https://doi.org/10.1007/s10458-012-9200-2"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-48778-6_18",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1026111332",
"https://doi.org/10.1007/3-540-48778-6_18"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-78499-9_21",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1027448880",
"https://doi.org/10.1007/978-3-540-78499-9_21"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/s10703-006-0005-2",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1002395349",
"https://doi.org/10.1007/s10703-006-0005-2"
],
"type": "CreativeWork"
}
],
"datePublished": "2017-03-08",
"datePublishedReg": "2017-03-08",
"description": "We present automated techniques for the verification and control of partially observable, probabilistic systems for both discrete and dense models of time. For the discrete-time case, we formally model these systems using partially observable Markov decision processes; for dense time, we propose an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. We give probabilistic temporal logics 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 synthesise a controller for the model which makes it true. Our approach is based on a grid-based abstraction of the uncountable belief space induced by partial observability and, for dense-time models, an integer discretisation of real-time behaviour. The former 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 task and network scheduling, computer security and planning.",
"genre": "article",
"id": "sg:pub.10.1007/s11241-017-9269-4",
"inLanguage": "en",
"isAccessibleForFree": true,
"isFundedItemOf": [
{
"id": "sg:grant.3497570",
"type": "MonetaryGrant"
},
{
"id": "sg:grant.6711417",
"type": "MonetaryGrant"
},
{
"id": "sg:grant.3560167",
"type": "MonetaryGrant"
}
],
"isPartOf": [
{
"id": "sg:journal.1136406",
"issn": [
"0922-6443",
"1573-1383"
],
"name": "Real-Time Systems",
"publisher": "Springer Nature",
"type": "Periodical"
},
{
"issueNumber": "3",
"type": "PublicationIssue"
},
{
"type": "PublicationVolume",
"volumeNumber": "53"
}
],
"keywords": [
"probabilistic systems",
"PRISM model checker",
"dense time model",
"probabilistic temporal logic",
"real-time behavior",
"domains of tasks",
"observable Markov decision process",
"extension of probabilistic",
"computer security",
"Markov decision process",
"model checker",
"temporal logic",
"network scheduling",
"dense model",
"belief space",
"partial observability",
"dense time",
"decision process",
"reward measures",
"event occurrence",
"verification",
"quantitative properties",
"upper bounds",
"checker",
"controller",
"case study",
"scheduling",
"security",
"abstraction",
"system",
"probabilistic",
"local state",
"task",
"automata",
"logic",
"technique",
"model",
"planning",
"observability",
"effectiveness",
"bounds",
"discrete-time case",
"domain",
"space",
"extension",
"time",
"numerical results",
"probability",
"control",
"process",
"discretisation",
"state",
"results",
"measures",
"behavior",
"observer",
"cases",
"properties",
"values",
"range",
"study",
"occurrence",
"problem",
"approach"
],
"name": "Verification and control of partially observable probabilistic systems",
"pagination": "354-402",
"productId": [
{
"name": "dimensions_id",
"type": "PropertyValue",
"value": [
"pub.1084030499"
]
},
{
"name": "doi",
"type": "PropertyValue",
"value": [
"10.1007/s11241-017-9269-4"
]
}
],
"sameAs": [
"https://doi.org/10.1007/s11241-017-9269-4",
"https://app.dimensions.ai/details/publication/pub.1084030499"
],
"sdDataset": "articles",
"sdDatePublished": "2022-05-10T10:19",
"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/article/article_751.jsonl",
"type": "ScholarlyArticle",
"url": "https://doi.org/10.1007/s11241-017-9269-4"
}
]Download the RDF metadata as: json-ld nt turtle xml License info
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/s11241-017-9269-4'
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/s11241-017-9269-4'
Turtle is a human-readable linked data format.
curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s11241-017-9269-4'
RDF/XML is a standard XML format for linked data.
curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s11241-017-9269-4'
This table displays all metadata directly associated to this object as RDF triples.
248 TRIPLES
22 PREDICATES
114 URIs
81 LITERALS
6 BLANK NODES