PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2016-04-09

AUTHORS

Marta Kwiatkowska , David Parker , Clemens Wiltsche

ABSTRACT

We present a new release of PRISM-games, a tool for verification and strategy synthesis for stochastic games. PRISM-games 2.0 significantly extends its functionality by supporting, for the first time: (i) long-run average (mean-payoff) and ratio reward objectives, e.g., to express energy consumption per time unit; (ii) strategy synthesis and Pareto set computation for multi-objective properties; and (iii) compositional strategy synthesis, where strategies for a stochastic game modelled as a composition of subsystems are synthesised from strategies for individual components using assume-guarantee contracts on component interfaces. We demonstrate the usefulness of the new tool on four case studies from autonomous transport and energy management. More... »

PAGES

560-566

Book

TITLE

Tools and Algorithms for the Construction and Analysis of Systems

ISBN

978-3-662-49673-2
978-3-662-49674-9

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-662-49674-9_35

DOI

http://dx.doi.org/10.1007/978-3-662-49674-9_35

DIMENSIONS

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


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/0104", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Statistics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, 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, 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 Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "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": "2016-04-09", 
    "datePublishedReg": "2016-04-09", 
    "description": "We present a new release of PRISM-games, a tool for verification and strategy synthesis for stochastic games. PRISM-games 2.0 significantly extends its functionality by supporting, for the first time: (i) long-run average (mean-payoff) and ratio reward objectives, e.g., to express energy consumption per time unit; (ii) strategy synthesis and Pareto set computation for multi-objective properties; and (iii) compositional strategy synthesis, where strategies for a stochastic game modelled as a composition of subsystems are synthesised from strategies for individual components using assume-guarantee contracts on component interfaces. We demonstrate the usefulness of the new tool on four case studies from autonomous transport and energy management.", 
    "editor": [
      {
        "familyName": "Chechik", 
        "givenName": "Marsha", 
        "type": "Person"
      }, 
      {
        "familyName": "Raskin", 
        "givenName": "Jean-Fran\u00e7ois", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-662-49674-9_35", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-662-49673-2", 
        "978-3-662-49674-9"
      ], 
      "name": "Tools and Algorithms for the Construction and Analysis of Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "strategy synthesis", 
      "PRISM-games", 
      "stochastic games", 
      "multi-objective properties", 
      "composition of subsystems", 
      "assume-guarantee contracts", 
      "component interfaces", 
      "news releases", 
      "game", 
      "reward objective", 
      "energy consumption", 
      "time unit", 
      "autonomous transport", 
      "energy management", 
      "tool", 
      "verification", 
      "functionality", 
      "computation", 
      "subsystems", 
      "new tool", 
      "case study", 
      "consumption", 
      "Pareto", 
      "strategies", 
      "individual components", 
      "interface", 
      "usefulness", 
      "management", 
      "time", 
      "objective", 
      "units", 
      "components", 
      "contracts", 
      "synthesis", 
      "first time", 
      "properties", 
      "study", 
      "release", 
      "composition", 
      "transport", 
      "PRISM-games 2.0", 
      "ratio reward objectives", 
      "compositional strategy synthesis", 
      "Multi-objective Strategy Synthesis"
    ], 
    "name": "PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games", 
    "pagination": "560-566", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1033723366"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-662-49674-9_35"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-662-49674-9_35", 
      "https://app.dimensions.ai/details/publication/pub.1033723366"
    ], 
    "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_180.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-662-49674-9_35"
  }
]
 

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-49674-9_35'

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-49674-9_35'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-49674-9_35'

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-49674-9_35'


 

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

126 TRIPLES      23 PREDICATES      69 URIs      62 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-662-49674-9_35 schema:about anzsrc-for:01
2 anzsrc-for:0104
3 schema:author N0b46d15219e944ef9046f2d7d6bd78fc
4 schema:datePublished 2016-04-09
5 schema:datePublishedReg 2016-04-09
6 schema:description We present a new release of PRISM-games, a tool for verification and strategy synthesis for stochastic games. PRISM-games 2.0 significantly extends its functionality by supporting, for the first time: (i) long-run average (mean-payoff) and ratio reward objectives, e.g., to express energy consumption per time unit; (ii) strategy synthesis and Pareto set computation for multi-objective properties; and (iii) compositional strategy synthesis, where strategies for a stochastic game modelled as a composition of subsystems are synthesised from strategies for individual components using assume-guarantee contracts on component interfaces. We demonstrate the usefulness of the new tool on four case studies from autonomous transport and energy management.
7 schema:editor Nbcc6d109256b42e8aa3a88f5df7975a1
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf Naced304f6f7b47498454f4ff96f2f6bc
12 schema:keywords Multi-objective Strategy Synthesis
13 PRISM-games
14 PRISM-games 2.0
15 Pareto
16 assume-guarantee contracts
17 autonomous transport
18 case study
19 component interfaces
20 components
21 composition
22 composition of subsystems
23 compositional strategy synthesis
24 computation
25 consumption
26 contracts
27 energy consumption
28 energy management
29 first time
30 functionality
31 game
32 individual components
33 interface
34 management
35 multi-objective properties
36 new tool
37 news releases
38 objective
39 properties
40 ratio reward objectives
41 release
42 reward objective
43 stochastic games
44 strategies
45 strategy synthesis
46 study
47 subsystems
48 synthesis
49 time
50 time unit
51 tool
52 transport
53 units
54 usefulness
55 verification
56 schema:name PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games
57 schema:pagination 560-566
58 schema:productId Nade5a1e03c524b1cb60ab25dc529942d
59 Nb7bd5e5ce8904450a9ee21e25486a59e
60 schema:publisher Nf9614b837aef4097bb9e07e496e7c506
61 schema:sameAs https://app.dimensions.ai/details/publication/pub.1033723366
62 https://doi.org/10.1007/978-3-662-49674-9_35
63 schema:sdDatePublished 2021-12-01T19:58
64 schema:sdLicense https://scigraph.springernature.com/explorer/license/
65 schema:sdPublisher Nf7388ee7b4924a789bc5b331c1a5d598
66 schema:url https://doi.org/10.1007/978-3-662-49674-9_35
67 sgo:license sg:explorer/license/
68 sgo:sdDataset chapters
69 rdf:type schema:Chapter
70 N0b46d15219e944ef9046f2d7d6bd78fc rdf:first sg:person.011375012273.39
71 rdf:rest Na46f5af6b91e4236ab6a823691ec7330
72 N2221634d4f704a3c894134ed0214f39e rdf:first Nf15e1c9f6c794f7bbac81363693cd5e7
73 rdf:rest rdf:nil
74 N2fd487c9278545ca84da94cf76bfefec schema:familyName Chechik
75 schema:givenName Marsha
76 rdf:type schema:Person
77 Na46f5af6b91e4236ab6a823691ec7330 rdf:first sg:person.014007552600.37
78 rdf:rest Na677c7fc7c804ac789e4ae16f406636a
79 Na677c7fc7c804ac789e4ae16f406636a rdf:first sg:person.013041737446.42
80 rdf:rest rdf:nil
81 Naced304f6f7b47498454f4ff96f2f6bc schema:isbn 978-3-662-49673-2
82 978-3-662-49674-9
83 schema:name Tools and Algorithms for the Construction and Analysis of Systems
84 rdf:type schema:Book
85 Nade5a1e03c524b1cb60ab25dc529942d schema:name dimensions_id
86 schema:value pub.1033723366
87 rdf:type schema:PropertyValue
88 Nb7bd5e5ce8904450a9ee21e25486a59e schema:name doi
89 schema:value 10.1007/978-3-662-49674-9_35
90 rdf:type schema:PropertyValue
91 Nbcc6d109256b42e8aa3a88f5df7975a1 rdf:first N2fd487c9278545ca84da94cf76bfefec
92 rdf:rest N2221634d4f704a3c894134ed0214f39e
93 Nf15e1c9f6c794f7bbac81363693cd5e7 schema:familyName Raskin
94 schema:givenName Jean-François
95 rdf:type schema:Person
96 Nf7388ee7b4924a789bc5b331c1a5d598 schema:name Springer Nature - SN SciGraph project
97 rdf:type schema:Organization
98 Nf9614b837aef4097bb9e07e496e7c506 schema:name Springer Nature
99 rdf:type schema:Organisation
100 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
101 schema:name Mathematical Sciences
102 rdf:type schema:DefinedTerm
103 anzsrc-for:0104 schema:inDefinedTermSet anzsrc-for:
104 schema:name Statistics
105 rdf:type schema:DefinedTerm
106 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
107 schema:familyName Kwiatkowska
108 schema:givenName Marta
109 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
110 rdf:type schema:Person
111 sg:person.013041737446.42 schema:affiliation grid-institutes:grid.4991.5
112 schema:familyName Wiltsche
113 schema:givenName Clemens
114 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013041737446.42
115 rdf:type schema:Person
116 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
117 schema:familyName Parker
118 schema:givenName David
119 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
120 rdf:type schema:Person
121 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, Oxford, UK
122 schema:name Department of Computer Science, University of Oxford, Oxford, UK
123 rdf:type schema:Organization
124 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, Birmingham, UK
125 schema:name School of Computer Science, University of Birmingham, Birmingham, UK
126 rdf:type schema:Organization
 




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


...