Compositional Controller Synthesis for Stochastic Games View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2014

AUTHORS

Nicolas Basset , Marta Kwiatkowska , Clemens Wiltsche

ABSTRACT

Design of autonomous systems is facilitated by automatic synthesis of correct-by-construction controllers from formal models and specifications. We focus on stochastic games, which can model the interaction with an adverse environment, as well as probabilistic behaviour arising from uncertainties. We propose a synchronising parallel composition for stochastic games that enables a compositional approach to controller synthesis. We leverage rules for compositional assume-guarantee verification of probabilistic automata to synthesise controllers for games with multi-objective quantitative winning conditions. By composing winning strategies synthesised for the individual components, we can thus obtain a winning strategy for the composed game, achieving better scalability and efficiency at a cost of restricting the class of controllers. More... »

PAGES

173-187

Book

TITLE

CONCUR 2014 – Concurrency Theory

ISBN

978-3-662-44583-9
978-3-662-44584-6

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-662-44584-6_13

DOI

http://dx.doi.org/10.1007/978-3-662-44584-6_13

DIMENSIONS

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


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"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, United Kingdom", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, United Kingdom"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Basset", 
        "givenName": "Nicolas", 
        "id": "sg:person.014372542370.01", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014372542370.01"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, United Kingdom", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, United Kingdom"
          ], 
          "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": "Department of Computer Science, University of Oxford, United Kingdom", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, United Kingdom"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Wiltsche", 
        "givenName": "Clemens", 
        "id": "sg:person.013041737446.42", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013041737446.42"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2014", 
    "datePublishedReg": "2014-01-01", 
    "description": "Design of autonomous systems is facilitated by automatic synthesis of correct-by-construction controllers from formal models and specifications. We focus on stochastic games, which can model the interaction with an adverse environment, as well as probabilistic behaviour arising from uncertainties. We propose a synchronising parallel composition for stochastic games that enables a compositional approach to controller synthesis. We leverage rules for compositional assume-guarantee verification of probabilistic automata to synthesise controllers for games with multi-objective quantitative winning conditions. By composing winning strategies synthesised for the individual components, we can thus obtain a winning strategy for the composed game, achieving better scalability and efficiency at a cost of restricting the class of controllers.", 
    "editor": [
      {
        "familyName": "Baldan", 
        "givenName": "Paolo", 
        "type": "Person"
      }, 
      {
        "familyName": "Gorla", 
        "givenName": "Daniele", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-662-44584-6_13", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-662-44583-9", 
        "978-3-662-44584-6"
      ], 
      "name": "CONCUR 2014 \u2013 Concurrency Theory", 
      "type": "Book"
    }, 
    "keywords": [
      "assume-guarantee verification", 
      "stochastic games", 
      "construction controllers", 
      "good scalability", 
      "automatic synthesis", 
      "formal model", 
      "autonomous systems", 
      "controller synthesis", 
      "compositional approach", 
      "parallel composition", 
      "probabilistic automata", 
      "probabilistic behavior", 
      "controller", 
      "game", 
      "scalability", 
      "class of controllers", 
      "adverse environments", 
      "verification", 
      "specification", 
      "automata", 
      "rules", 
      "environment", 
      "cost", 
      "system", 
      "individual components", 
      "design", 
      "efficiency", 
      "strategies", 
      "uncertainty", 
      "model", 
      "class", 
      "components", 
      "behavior", 
      "interaction", 
      "conditions", 
      "synthesis", 
      "composition", 
      "approach", 
      "compositional assume-guarantee verification", 
      "Compositional Controller Synthesis"
    ], 
    "name": "Compositional Controller Synthesis for Stochastic Games", 
    "pagination": "173-187", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1011418323"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-662-44584-6_13"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-662-44584-6_13", 
      "https://app.dimensions.ai/details/publication/pub.1011418323"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T19:58", 
    "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_176.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-662-44584-6_13"
  }
]
 

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-662-44584-6_13'

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-662-44584-6_13'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-44584-6_13'

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-662-44584-6_13'


 

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

119 TRIPLES      23 PREDICATES      66 URIs      59 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-662-44584-6_13 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 schema:author N453c1bd4a69e4854b02145d99d7b5d8d
4 schema:datePublished 2014
5 schema:datePublishedReg 2014-01-01
6 schema:description Design of autonomous systems is facilitated by automatic synthesis of correct-by-construction controllers from formal models and specifications. We focus on stochastic games, which can model the interaction with an adverse environment, as well as probabilistic behaviour arising from uncertainties. We propose a synchronising parallel composition for stochastic games that enables a compositional approach to controller synthesis. We leverage rules for compositional assume-guarantee verification of probabilistic automata to synthesise controllers for games with multi-objective quantitative winning conditions. By composing winning strategies synthesised for the individual components, we can thus obtain a winning strategy for the composed game, achieving better scalability and efficiency at a cost of restricting the class of controllers.
7 schema:editor N38bd3accbae14aa1b507faf18fd7615a
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N7e60dd65c29e4d828fcf09e80f16e917
12 schema:keywords Compositional Controller Synthesis
13 adverse environments
14 approach
15 assume-guarantee verification
16 automata
17 automatic synthesis
18 autonomous systems
19 behavior
20 class
21 class of controllers
22 components
23 composition
24 compositional approach
25 compositional assume-guarantee verification
26 conditions
27 construction controllers
28 controller
29 controller synthesis
30 cost
31 design
32 efficiency
33 environment
34 formal model
35 game
36 good scalability
37 individual components
38 interaction
39 model
40 parallel composition
41 probabilistic automata
42 probabilistic behavior
43 rules
44 scalability
45 specification
46 stochastic games
47 strategies
48 synthesis
49 system
50 uncertainty
51 verification
52 schema:name Compositional Controller Synthesis for Stochastic Games
53 schema:pagination 173-187
54 schema:productId N16c43d7b13fb4da8ae8fd6b7b0724307
55 N3b5493df1d5b4fe6b8c9713848e4d67d
56 schema:publisher N7d8d1684bd0b4cdbb201948b013fb098
57 schema:sameAs https://app.dimensions.ai/details/publication/pub.1011418323
58 https://doi.org/10.1007/978-3-662-44584-6_13
59 schema:sdDatePublished 2021-12-01T19:58
60 schema:sdLicense https://scigraph.springernature.com/explorer/license/
61 schema:sdPublisher N634601d8624f4b46b99d11da8f7e5796
62 schema:url https://doi.org/10.1007/978-3-662-44584-6_13
63 sgo:license sg:explorer/license/
64 sgo:sdDataset chapters
65 rdf:type schema:Chapter
66 N16c43d7b13fb4da8ae8fd6b7b0724307 schema:name dimensions_id
67 schema:value pub.1011418323
68 rdf:type schema:PropertyValue
69 N311deefb8d48496c9e82cc9e9dbb0f1f rdf:first sg:person.011375012273.39
70 rdf:rest N71f21e0598d64946b926b2caaafc4186
71 N38bd3accbae14aa1b507faf18fd7615a rdf:first Nd1c34d34686841e38555ac71da0c7cdd
72 rdf:rest Nd43da63085e940229777cdb6bd0a0797
73 N3b5493df1d5b4fe6b8c9713848e4d67d schema:name doi
74 schema:value 10.1007/978-3-662-44584-6_13
75 rdf:type schema:PropertyValue
76 N453c1bd4a69e4854b02145d99d7b5d8d rdf:first sg:person.014372542370.01
77 rdf:rest N311deefb8d48496c9e82cc9e9dbb0f1f
78 N634601d8624f4b46b99d11da8f7e5796 schema:name Springer Nature - SN SciGraph project
79 rdf:type schema:Organization
80 N71f21e0598d64946b926b2caaafc4186 rdf:first sg:person.013041737446.42
81 rdf:rest rdf:nil
82 N7d8d1684bd0b4cdbb201948b013fb098 schema:name Springer Nature
83 rdf:type schema:Organisation
84 N7e60dd65c29e4d828fcf09e80f16e917 schema:isbn 978-3-662-44583-9
85 978-3-662-44584-6
86 schema:name CONCUR 2014 – Concurrency Theory
87 rdf:type schema:Book
88 Nd1c34d34686841e38555ac71da0c7cdd schema:familyName Baldan
89 schema:givenName Paolo
90 rdf:type schema:Person
91 Nd43da63085e940229777cdb6bd0a0797 rdf:first Ne5a89879167c4e70b52924aee65fb079
92 rdf:rest rdf:nil
93 Ne5a89879167c4e70b52924aee65fb079 schema:familyName Gorla
94 schema:givenName Daniele
95 rdf:type schema:Person
96 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
97 schema:name Information and Computing Sciences
98 rdf:type schema:DefinedTerm
99 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
100 schema:name Artificial Intelligence and Image Processing
101 rdf:type schema:DefinedTerm
102 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
103 schema:familyName Kwiatkowska
104 schema:givenName Marta
105 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
106 rdf:type schema:Person
107 sg:person.013041737446.42 schema:affiliation grid-institutes:grid.4991.5
108 schema:familyName Wiltsche
109 schema:givenName Clemens
110 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013041737446.42
111 rdf:type schema:Person
112 sg:person.014372542370.01 schema:affiliation grid-institutes:grid.4991.5
113 schema:familyName Basset
114 schema:givenName Nicolas
115 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014372542370.01
116 rdf:type schema:Person
117 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, United Kingdom
118 schema:name Department of Computer Science, University of Oxford, United Kingdom
119 rdf:type schema:Organization
 




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


...