Permissive Controller Synthesis for Probabilistic Systems View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2014

AUTHORS

Klaus Dräger , Vojtěch Forejt , Marta Kwiatkowska , David Parker , Mateusz Ujma

ABSTRACT

We propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty system components. Our aim is to generate robust controllers that are resilient to unexpected system changes at runtime, and flexible enough to be adapted if additional constraints need to be imposed. We develop a permissive controller synthesis framework, which generates multi-strategies for the controller, offering a choice of control actions to take at each time step. We formalise the notion of permissiveness using penalties, which are incurred each time a possible control action is blocked by a multi-strategy. Permissive controller synthesis aims to generate a multi-strategy that minimises these penalties, whilst guaranteeing the satisfaction of a specified system property. We establish several key results about the optimality of multi-strategies and the complexity of synthesising them. Then, we develop methods to perform permissive controller synthesis using mixed integer linear programming and illustrate their effectiveness on a selection of case studies. More... »

PAGES

531-546

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-54862-8_44

DOI

http://dx.doi.org/10.1007/978-3-642-54862-8_44

DIMENSIONS

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


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"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "EECS, Queen Mary, University of London, UK", 
          "id": "http://www.grid.ac/institutes/grid.4464.2", 
          "name": [
            "EECS, Queen Mary, University of London, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Dr\u00e4ger", 
        "givenName": "Klaus", 
        "id": "sg:person.014124732361.06", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014124732361.06"
        ], 
        "type": "Person"
      }, 
      {
        "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": "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": "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"
      }, 
      {
        "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": "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 propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty system components. Our aim is to generate robust controllers that are resilient to unexpected system changes at runtime, and flexible enough to be adapted if additional constraints need to be imposed. We develop a permissive controller synthesis framework, which generates multi-strategies for the controller, offering a choice of control actions to take at each time step. We formalise the notion of permissiveness using penalties, which are incurred each time a possible control action is blocked by a multi-strategy. Permissive controller synthesis aims to generate a multi-strategy that minimises these penalties, whilst guaranteeing the satisfaction of a specified system property. We establish several key results about the optimality of multi-strategies and the complexity of synthesising them. Then, we develop methods to perform permissive controller synthesis using mixed integer linear programming and illustrate their effectiveness on a selection of case studies.", 
    "editor": [
      {
        "familyName": "\u00c1brah\u00e1m", 
        "givenName": "Erika", 
        "type": "Person"
      }, 
      {
        "familyName": "Havelund", 
        "givenName": "Klaus", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-54862-8_44", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-54861-1", 
        "978-3-642-54862-8"
      ], 
      "name": "Tools and Algorithms for the Construction and Analysis of Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "probabilistic systems", 
      "specified system properties", 
      "controller synthesis", 
      "control actions", 
      "integer linear programming", 
      "two-player games", 
      "controller synthesis framework", 
      "controller synthesis technique", 
      "unreliable sensors", 
      "unexpected system changes", 
      "faulty system components", 
      "possible control actions", 
      "synthesis framework", 
      "system components", 
      "linear programming", 
      "system properties", 
      "additional constraints", 
      "controller", 
      "robust controller", 
      "time step", 
      "runtime", 
      "synthesis technique", 
      "programming", 
      "case study", 
      "complexity", 
      "system", 
      "penalty", 
      "optimality", 
      "game", 
      "constraints", 
      "framework", 
      "sensors", 
      "environment", 
      "system changes", 
      "effectiveness", 
      "technique", 
      "example", 
      "selection", 
      "players", 
      "step", 
      "uncertainty", 
      "probability", 
      "method", 
      "notion", 
      "key results", 
      "time", 
      "components", 
      "satisfaction", 
      "results", 
      "choice", 
      "action", 
      "aim", 
      "properties", 
      "study", 
      "changes", 
      "synthesis", 
      "novel controller synthesis techniques", 
      "permissive controller synthesis framework", 
      "Permissive controller synthesis"
    ], 
    "name": "Permissive Controller Synthesis for Probabilistic Systems", 
    "pagination": "531-546", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1001975875"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-54862-8_44"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-54862-8_44", 
      "https://app.dimensions.ai/details/publication/pub.1001975875"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-11-01T18:52", 
    "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_233.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-54862-8_44"
  }
]
 

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-642-54862-8_44'

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-642-54862-8_44'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-54862-8_44'

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-642-54862-8_44'


 

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

158 TRIPLES      23 PREDICATES      85 URIs      78 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-54862-8_44 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N0fcf4c508a6b46c28ca06a0c2987d4e7
4 schema:datePublished 2014
5 schema:datePublishedReg 2014-01-01
6 schema:description We propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty system components. Our aim is to generate robust controllers that are resilient to unexpected system changes at runtime, and flexible enough to be adapted if additional constraints need to be imposed. We develop a permissive controller synthesis framework, which generates multi-strategies for the controller, offering a choice of control actions to take at each time step. We formalise the notion of permissiveness using penalties, which are incurred each time a possible control action is blocked by a multi-strategy. Permissive controller synthesis aims to generate a multi-strategy that minimises these penalties, whilst guaranteeing the satisfaction of a specified system property. We establish several key results about the optimality of multi-strategies and the complexity of synthesising them. Then, we develop methods to perform permissive controller synthesis using mixed integer linear programming and illustrate their effectiveness on a selection of case studies.
7 schema:editor N3c764b71d50e48ac96d8003d0334d11d
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N3eeaece3e71a4829a58bf2f3b742befe
12 schema:keywords Permissive controller synthesis
13 action
14 additional constraints
15 aim
16 case study
17 changes
18 choice
19 complexity
20 components
21 constraints
22 control actions
23 controller
24 controller synthesis
25 controller synthesis framework
26 controller synthesis technique
27 effectiveness
28 environment
29 example
30 faulty system components
31 framework
32 game
33 integer linear programming
34 key results
35 linear programming
36 method
37 notion
38 novel controller synthesis techniques
39 optimality
40 penalty
41 permissive controller synthesis framework
42 players
43 possible control actions
44 probabilistic systems
45 probability
46 programming
47 properties
48 results
49 robust controller
50 runtime
51 satisfaction
52 selection
53 sensors
54 specified system properties
55 step
56 study
57 synthesis
58 synthesis framework
59 synthesis technique
60 system
61 system changes
62 system components
63 system properties
64 technique
65 time
66 time step
67 two-player games
68 uncertainty
69 unexpected system changes
70 unreliable sensors
71 schema:name Permissive Controller Synthesis for Probabilistic Systems
72 schema:pagination 531-546
73 schema:productId Nacb79fed059c497ab0c3c2c32791ebb0
74 Nb82b9b300f7543d7809d0c5cf29ff24b
75 schema:publisher Nc4356bd4218845b29d76f37485cfde0b
76 schema:sameAs https://app.dimensions.ai/details/publication/pub.1001975875
77 https://doi.org/10.1007/978-3-642-54862-8_44
78 schema:sdDatePublished 2021-11-01T18:52
79 schema:sdLicense https://scigraph.springernature.com/explorer/license/
80 schema:sdPublisher Nc8b3cae9b4214bdbacd3df144b8f4848
81 schema:url https://doi.org/10.1007/978-3-642-54862-8_44
82 sgo:license sg:explorer/license/
83 sgo:sdDataset chapters
84 rdf:type schema:Chapter
85 N0fcf4c508a6b46c28ca06a0c2987d4e7 rdf:first sg:person.014124732361.06
86 rdf:rest Nb59e7faf32ef4bc0b7ccba46235f638b
87 N1f568ba573f54823803718fa01c9c271 rdf:first sg:person.014007552600.37
88 rdf:rest Nfd834f474fee46d2a939dcca2f0a2109
89 N3c764b71d50e48ac96d8003d0334d11d rdf:first N5d2e8d6f714c4be98cf6f7caf416555e
90 rdf:rest Nc5e284aa5bc04f6fa90477610a044a6f
91 N3eeaece3e71a4829a58bf2f3b742befe schema:isbn 978-3-642-54861-1
92 978-3-642-54862-8
93 schema:name Tools and Algorithms for the Construction and Analysis of Systems
94 rdf:type schema:Book
95 N5d2e8d6f714c4be98cf6f7caf416555e schema:familyName Ábrahám
96 schema:givenName Erika
97 rdf:type schema:Person
98 N5f85d36a9552415d97e5acb8071a6804 schema:familyName Havelund
99 schema:givenName Klaus
100 rdf:type schema:Person
101 Na1160e3b560041edbabf26fa612dc79a rdf:first sg:person.011375012273.39
102 rdf:rest N1f568ba573f54823803718fa01c9c271
103 Nacb79fed059c497ab0c3c2c32791ebb0 schema:name dimensions_id
104 schema:value pub.1001975875
105 rdf:type schema:PropertyValue
106 Nb59e7faf32ef4bc0b7ccba46235f638b rdf:first sg:person.012103627631.41
107 rdf:rest Na1160e3b560041edbabf26fa612dc79a
108 Nb82b9b300f7543d7809d0c5cf29ff24b schema:name doi
109 schema:value 10.1007/978-3-642-54862-8_44
110 rdf:type schema:PropertyValue
111 Nc4356bd4218845b29d76f37485cfde0b schema:name Springer Nature
112 rdf:type schema:Organisation
113 Nc5e284aa5bc04f6fa90477610a044a6f rdf:first N5f85d36a9552415d97e5acb8071a6804
114 rdf:rest rdf:nil
115 Nc8b3cae9b4214bdbacd3df144b8f4848 schema:name Springer Nature - SN SciGraph project
116 rdf:type schema:Organization
117 Nfd834f474fee46d2a939dcca2f0a2109 rdf:first sg:person.011443107516.15
118 rdf:rest rdf:nil
119 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
120 schema:name Information and Computing Sciences
121 rdf:type schema:DefinedTerm
122 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
123 schema:name Computation Theory and Mathematics
124 rdf:type schema:DefinedTerm
125 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
126 schema:familyName Kwiatkowska
127 schema:givenName Marta
128 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
129 rdf:type schema:Person
130 sg:person.011443107516.15 schema:affiliation grid-institutes:grid.4991.5
131 schema:familyName Ujma
132 schema:givenName Mateusz
133 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011443107516.15
134 rdf:type schema:Person
135 sg:person.012103627631.41 schema:affiliation grid-institutes:grid.4991.5
136 schema:familyName Forejt
137 schema:givenName Vojtěch
138 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012103627631.41
139 rdf:type schema:Person
140 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
141 schema:familyName Parker
142 schema:givenName David
143 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
144 rdf:type schema:Person
145 sg:person.014124732361.06 schema:affiliation grid-institutes:grid.4464.2
146 schema:familyName Dräger
147 schema:givenName Klaus
148 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014124732361.06
149 rdf:type schema:Person
150 grid-institutes:grid.4464.2 schema:alternateName EECS, Queen Mary, University of London, UK
151 schema:name EECS, Queen Mary, University of London, UK
152 rdf:type schema:Organization
153 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, UK
154 schema:name Department of Computer Science, University of Oxford, UK
155 rdf:type schema:Organization
156 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, UK
157 schema:name School of Computer Science, University of Birmingham, UK
158 rdf:type schema:Organization
 




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


...