PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2020-07-14

AUTHORS

Marta Kwiatkowska , Gethin Norman , David Parker , Gabriel Santos

ABSTRACT

We present a major new release of the PRISM-games model checker, featuring multiple significant advances in its support for verification and strategy synthesis of stochastic games. Firstly, concurrent stochastic games bring more realistic modelling of agents interacting in a concurrent fashion. Secondly, equilibria-based properties provide a means to analyse games in which competing or collaborating players are driven by distinct objectives. Thirdly, a real-time extension of (turn-based) stochastic games facilitates verification and strategy synthesis for systems where timing is a crucial aspect. This paper describes the advances made in the tool’s modelling language, property specification language and model checking engines in order to implement this new functionality. We also summarise the performance and scalability of the tool, and describe a selection of case studies, ranging from security protocols to robot coordination, which highlight the benefits of the new features. More... »

PAGES

475-487

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-030-53291-8_25

DOI

http://dx.doi.org/10.1007/978-3-030-53291-8_25

DIMENSIONS

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


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 Computing Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computing 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 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 Computing Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computing Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Santos", 
        "givenName": "Gabriel", 
        "id": "sg:person.016331342360.82", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016331342360.82"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2020-07-14", 
    "datePublishedReg": "2020-07-14", 
    "description": "We present a major new release of the PRISM-games model checker, featuring multiple significant advances in its support for verification and strategy synthesis of stochastic games. Firstly, concurrent stochastic games bring more realistic modelling of agents interacting in a concurrent fashion. Secondly, equilibria-based properties provide a means to analyse games in which competing or collaborating players are driven by distinct objectives. Thirdly, a real-time extension of (turn-based) stochastic games facilitates verification and strategy synthesis for systems where timing is a crucial aspect. This paper describes the advances made in the tool\u2019s modelling language, property specification language and model checking engines in order to implement this new functionality. We also summarise the performance and scalability of the tool, and describe a selection of case studies, ranging from security protocols to robot coordination, which highlight the benefits of the new features.", 
    "editor": [
      {
        "familyName": "Lahiri", 
        "givenName": "Shuvendu K.", 
        "type": "Person"
      }, 
      {
        "familyName": "Wang", 
        "givenName": "Chao", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-030-53291-8_25", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-030-53290-1", 
        "978-3-030-53291-8"
      ], 
      "name": "Computer Aided Verification", 
      "type": "Book"
    }, 
    "keywords": [
      "modelling language", 
      "PRISM-games model checker", 
      "property specification language", 
      "real-time extension", 
      "model checking engines", 
      "stochastic games", 
      "strategy synthesis", 
      "concurrent stochastic games", 
      "major new release", 
      "robot coordination", 
      "security protocols", 
      "specification language", 
      "model checker", 
      "concurrent fashion", 
      "new functionalities", 
      "new features", 
      "new release", 
      "verification", 
      "game", 
      "distinct objectives", 
      "language", 
      "scalability", 
      "crucial aspect", 
      "concurrency", 
      "checker", 
      "case study", 
      "realistic modelling", 
      "engine", 
      "functionality", 
      "tool", 
      "protocol", 
      "advances", 
      "performance", 
      "features", 
      "system", 
      "significant advances", 
      "modelling", 
      "extension", 
      "selection", 
      "players", 
      "coordination", 
      "order", 
      "support", 
      "fashion", 
      "aspects", 
      "benefits", 
      "time", 
      "objective", 
      "means", 
      "agents", 
      "properties", 
      "study", 
      "timing", 
      "equilibrium", 
      "synthesis", 
      "release", 
      "paper"
    ], 
    "name": "PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time", 
    "pagination": "475-487", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1129377952"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-030-53291-8_25"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-030-53291-8_25", 
      "https://app.dimensions.ai/details/publication/pub.1129377952"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:46", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220519/entities/gbq_results/chapter/chapter_333.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-030-53291-8_25"
  }
]
 

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-030-53291-8_25'

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-030-53291-8_25'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-53291-8_25'

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-030-53291-8_25'


 

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

149 TRIPLES      23 PREDICATES      82 URIs      75 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-030-53291-8_25 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 schema:author N283b9b7eed67481799bb90587a979574
4 schema:datePublished 2020-07-14
5 schema:datePublishedReg 2020-07-14
6 schema:description We present a major new release of the PRISM-games model checker, featuring multiple significant advances in its support for verification and strategy synthesis of stochastic games. Firstly, concurrent stochastic games bring more realistic modelling of agents interacting in a concurrent fashion. Secondly, equilibria-based properties provide a means to analyse games in which competing or collaborating players are driven by distinct objectives. Thirdly, a real-time extension of (turn-based) stochastic games facilitates verification and strategy synthesis for systems where timing is a crucial aspect. This paper describes the advances made in the tool’s modelling language, property specification language and model checking engines in order to implement this new functionality. We also summarise the performance and scalability of the tool, and describe a selection of case studies, ranging from security protocols to robot coordination, which highlight the benefits of the new features.
7 schema:editor Nc637bb10fa054f2a877f614ab550caba
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf Nf4bb1bf85c6b4bd8aad608aa88fde0ff
12 schema:keywords PRISM-games model checker
13 advances
14 agents
15 aspects
16 benefits
17 case study
18 checker
19 concurrency
20 concurrent fashion
21 concurrent stochastic games
22 coordination
23 crucial aspect
24 distinct objectives
25 engine
26 equilibrium
27 extension
28 fashion
29 features
30 functionality
31 game
32 language
33 major new release
34 means
35 model checker
36 model checking engines
37 modelling
38 modelling language
39 new features
40 new functionalities
41 new release
42 objective
43 order
44 paper
45 performance
46 players
47 properties
48 property specification language
49 protocol
50 real-time extension
51 realistic modelling
52 release
53 robot coordination
54 scalability
55 security protocols
56 selection
57 significant advances
58 specification language
59 stochastic games
60 strategy synthesis
61 study
62 support
63 synthesis
64 system
65 time
66 timing
67 tool
68 verification
69 schema:name PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time
70 schema:pagination 475-487
71 schema:productId N0a2e704be9d444d8a6e03ae588dea1f2
72 N0f189662a9d843048ff99ac5e2656115
73 schema:publisher N3c4d2ec5df344e6c95e1d4ab18bb7b21
74 schema:sameAs https://app.dimensions.ai/details/publication/pub.1129377952
75 https://doi.org/10.1007/978-3-030-53291-8_25
76 schema:sdDatePublished 2022-05-20T07:46
77 schema:sdLicense https://scigraph.springernature.com/explorer/license/
78 schema:sdPublisher N211b75b0a73e4e1ab347cfd4270ddd8d
79 schema:url https://doi.org/10.1007/978-3-030-53291-8_25
80 sgo:license sg:explorer/license/
81 sgo:sdDataset chapters
82 rdf:type schema:Chapter
83 N0a2e704be9d444d8a6e03ae588dea1f2 schema:name dimensions_id
84 schema:value pub.1129377952
85 rdf:type schema:PropertyValue
86 N0d5d6a2fcca54064ba0f852cd5dcc403 schema:familyName Lahiri
87 schema:givenName Shuvendu K.
88 rdf:type schema:Person
89 N0f189662a9d843048ff99ac5e2656115 schema:name doi
90 schema:value 10.1007/978-3-030-53291-8_25
91 rdf:type schema:PropertyValue
92 N211b75b0a73e4e1ab347cfd4270ddd8d schema:name Springer Nature - SN SciGraph project
93 rdf:type schema:Organization
94 N283b9b7eed67481799bb90587a979574 rdf:first sg:person.011375012273.39
95 rdf:rest Nde92b252b63c44d1ac7148b75a278639
96 N3a376281a24f4703a97ff48ffca83abb schema:familyName Wang
97 schema:givenName Chao
98 rdf:type schema:Person
99 N3c4d2ec5df344e6c95e1d4ab18bb7b21 schema:name Springer Nature
100 rdf:type schema:Organisation
101 N54b0d2447e9e402caa7fd4d81fb9a2c9 rdf:first sg:person.016331342360.82
102 rdf:rest rdf:nil
103 N7430636aa3ad4791bd4f878b59369d80 rdf:first N3a376281a24f4703a97ff48ffca83abb
104 rdf:rest rdf:nil
105 N9add9758127843bb961e4a0bb37e9743 rdf:first sg:person.014007552600.37
106 rdf:rest N54b0d2447e9e402caa7fd4d81fb9a2c9
107 Nc637bb10fa054f2a877f614ab550caba rdf:first N0d5d6a2fcca54064ba0f852cd5dcc403
108 rdf:rest N7430636aa3ad4791bd4f878b59369d80
109 Nde92b252b63c44d1ac7148b75a278639 rdf:first sg:person.016323171577.36
110 rdf:rest N9add9758127843bb961e4a0bb37e9743
111 Nf4bb1bf85c6b4bd8aad608aa88fde0ff schema:isbn 978-3-030-53290-1
112 978-3-030-53291-8
113 schema:name Computer Aided Verification
114 rdf:type schema:Book
115 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
116 schema:name Information and Computing Sciences
117 rdf:type schema:DefinedTerm
118 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
119 schema:name Artificial Intelligence and Image Processing
120 rdf:type schema:DefinedTerm
121 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
122 schema:familyName Kwiatkowska
123 schema:givenName Marta
124 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
125 rdf:type schema:Person
126 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
127 schema:familyName Parker
128 schema:givenName David
129 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
130 rdf:type schema:Person
131 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
132 schema:familyName Norman
133 schema:givenName Gethin
134 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
135 rdf:type schema:Person
136 sg:person.016331342360.82 schema:affiliation grid-institutes:grid.4991.5
137 schema:familyName Santos
138 schema:givenName Gabriel
139 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016331342360.82
140 rdf:type schema:Person
141 grid-institutes:grid.4991.5 schema:alternateName Department of Computing Science, University of Oxford, Oxford, UK
142 schema:name Department of Computing Science, University of Oxford, Oxford, UK
143 rdf:type schema:Organization
144 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, Birmingham, UK
145 schema:name School of Computer Science, University of Birmingham, Birmingham, UK
146 rdf:type schema:Organization
147 grid-institutes:grid.8756.c schema:alternateName School of Computing Science, University of Glasgow, Glasgow, UK
148 schema:name School of Computing Science, University of Glasgow, Glasgow, UK
149 rdf:type schema:Organization
 




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


...