Automated Verification of Concurrent Stochastic Games View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2018-08-15

AUTHORS

Marta Kwiatkowska , Gethin Norman , David Parker , Gabriel Santos

ABSTRACT

We present automatic verification techniques for concurrent stochastic multi-player games (CSGs) with rewards. To express properties of such models, we adapt the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards), originally introduced for the simpler model of turn-based games, which enables quantitative reasoning about the ability of coalitions of players to achieve goals related to the probability of an event or reward measures. We propose and implement a modelling approach and model checking algorithms for property verification and strategy synthesis of CSGs, as an extension of PRISM-games. We evaluate the performance, scalability and applicability of our techniques on case studies from domains such as security, networks and finance, showing that we can analyse systems with probabilistic, cooperative and competitive behaviour between concurrent components, including many scenarios that cannot be analysed with turn-based models. More... »

PAGES

223-239

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-99154-2_14

DOI

http://dx.doi.org/10.1007/978-3-319-99154-2_14

DIMENSIONS

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


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"
      }, 
      {
        "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": "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": "2018-08-15", 
    "datePublishedReg": "2018-08-15", 
    "description": "We present automatic verification techniques for concurrent stochastic multi-player games (CSGs) with rewards. To express properties of such models, we adapt the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards), originally introduced for the simpler model of turn-based games, which enables quantitative reasoning about the ability of coalitions of players to achieve goals related to the probability of an event or reward measures. We propose and implement a modelling approach and model checking algorithms for property verification and strategy synthesis of CSGs, as an extension of PRISM-games. We evaluate the performance, scalability and applicability of our techniques on case studies from domains such as security, networks and finance, showing that we can analyse systems with probabilistic, cooperative and competitive behaviour between concurrent components, including many scenarios that cannot be analysed with turn-based models.", 
    "editor": [
      {
        "familyName": "McIver", 
        "givenName": "Annabelle", 
        "type": "Person"
      }, 
      {
        "familyName": "Horvath", 
        "givenName": "Andras", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-99154-2_14", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-99153-5", 
        "978-3-319-99154-2"
      ], 
      "name": "Quantitative Evaluation of Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "automatic verification technique", 
      "stochastic multi-player games", 
      "multi-player games", 
      "PRISM-games", 
      "turn-based games", 
      "verification techniques", 
      "property verification", 
      "concurrent components", 
      "temporal logic", 
      "ability of coalitions", 
      "concurrent stochastic games", 
      "strategy synthesis", 
      "reward measures", 
      "stochastic games", 
      "quantitative reasoning", 
      "verification", 
      "game", 
      "such models", 
      "scalability", 
      "algorithm", 
      "security", 
      "case study", 
      "network", 
      "reasoning", 
      "logic", 
      "technique", 
      "scenarios", 
      "model", 
      "performance", 
      "system", 
      "domain", 
      "goal", 
      "applicability", 
      "extension", 
      "competitive behavior", 
      "players", 
      "probability", 
      "coalition", 
      "components", 
      "reward", 
      "ability", 
      "measures", 
      "simple model", 
      "finance", 
      "behavior", 
      "events", 
      "properties", 
      "study", 
      "synthesis", 
      "approach", 
      "CSGs", 
      "turn-based models"
    ], 
    "name": "Automated Verification of Concurrent Stochastic Games", 
    "pagination": "223-239", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1106158264"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-99154-2_14"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-99154-2_14", 
      "https://app.dimensions.ai/details/publication/pub.1106158264"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-11-01T19:01", 
    "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_5.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-99154-2_14"
  }
]
 

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-319-99154-2_14'

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-319-99154-2_14'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-99154-2_14'

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-319-99154-2_14'


 

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

148 TRIPLES      23 PREDICATES      78 URIs      70 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-99154-2_14 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 schema:author N3700c404b5604fd0aedec916c74eb2e8
5 schema:datePublished 2018-08-15
6 schema:datePublishedReg 2018-08-15
7 schema:description We present automatic verification techniques for concurrent stochastic multi-player games (CSGs) with rewards. To express properties of such models, we adapt the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards), originally introduced for the simpler model of turn-based games, which enables quantitative reasoning about the ability of coalitions of players to achieve goals related to the probability of an event or reward measures. We propose and implement a modelling approach and model checking algorithms for property verification and strategy synthesis of CSGs, as an extension of PRISM-games. We evaluate the performance, scalability and applicability of our techniques on case studies from domains such as security, networks and finance, showing that we can analyse systems with probabilistic, cooperative and competitive behaviour between concurrent components, including many scenarios that cannot be analysed with turn-based models.
8 schema:editor Nd82f502cb0114035ba9ba770de55340a
9 schema:genre chapter
10 schema:inLanguage en
11 schema:isAccessibleForFree true
12 schema:isPartOf Nbbc2cbe1b5bd43309eb3b68ccb23c7a1
13 schema:keywords CSGs
14 PRISM-games
15 ability
16 ability of coalitions
17 algorithm
18 applicability
19 approach
20 automatic verification technique
21 behavior
22 case study
23 coalition
24 competitive behavior
25 components
26 concurrent components
27 concurrent stochastic games
28 domain
29 events
30 extension
31 finance
32 game
33 goal
34 logic
35 measures
36 model
37 multi-player games
38 network
39 performance
40 players
41 probability
42 properties
43 property verification
44 quantitative reasoning
45 reasoning
46 reward
47 reward measures
48 scalability
49 scenarios
50 security
51 simple model
52 stochastic games
53 stochastic multi-player games
54 strategy synthesis
55 study
56 such models
57 synthesis
58 system
59 technique
60 temporal logic
61 turn-based games
62 turn-based models
63 verification
64 verification techniques
65 schema:name Automated Verification of Concurrent Stochastic Games
66 schema:pagination 223-239
67 schema:productId N2dabe27002f744a897e32f83d5300605
68 Ne83d3712750241a3b53c29c7dc995f43
69 schema:publisher N666a0ff8a3e2460691cc8407447ec067
70 schema:sameAs https://app.dimensions.ai/details/publication/pub.1106158264
71 https://doi.org/10.1007/978-3-319-99154-2_14
72 schema:sdDatePublished 2021-11-01T19:01
73 schema:sdLicense https://scigraph.springernature.com/explorer/license/
74 schema:sdPublisher N0eb0a693da8443978e003ad597e8f224
75 schema:url https://doi.org/10.1007/978-3-319-99154-2_14
76 sgo:license sg:explorer/license/
77 sgo:sdDataset chapters
78 rdf:type schema:Chapter
79 N0eb0a693da8443978e003ad597e8f224 schema:name Springer Nature - SN SciGraph project
80 rdf:type schema:Organization
81 N2dabe27002f744a897e32f83d5300605 schema:name doi
82 schema:value 10.1007/978-3-319-99154-2_14
83 rdf:type schema:PropertyValue
84 N3700c404b5604fd0aedec916c74eb2e8 rdf:first sg:person.011375012273.39
85 rdf:rest Nf6da93768d324c6b81d576c723397ecf
86 N39c985f7539545bcbb27cb6f5de3c3a5 rdf:first sg:person.016331342360.82
87 rdf:rest rdf:nil
88 N64f3467c08b64b0096f27c07451f821c rdf:first sg:person.014007552600.37
89 rdf:rest N39c985f7539545bcbb27cb6f5de3c3a5
90 N666a0ff8a3e2460691cc8407447ec067 schema:name Springer Nature
91 rdf:type schema:Organisation
92 Na8b232b4257a4bae94ef6e708160669e rdf:first Ne8523c225cf84085af295d9a6597ec7a
93 rdf:rest rdf:nil
94 Na9914b3cc4ba45018d51fd589004e638 schema:familyName McIver
95 schema:givenName Annabelle
96 rdf:type schema:Person
97 Nbbc2cbe1b5bd43309eb3b68ccb23c7a1 schema:isbn 978-3-319-99153-5
98 978-3-319-99154-2
99 schema:name Quantitative Evaluation of Systems
100 rdf:type schema:Book
101 Nd82f502cb0114035ba9ba770de55340a rdf:first Na9914b3cc4ba45018d51fd589004e638
102 rdf:rest Na8b232b4257a4bae94ef6e708160669e
103 Ne83d3712750241a3b53c29c7dc995f43 schema:name dimensions_id
104 schema:value pub.1106158264
105 rdf:type schema:PropertyValue
106 Ne8523c225cf84085af295d9a6597ec7a schema:familyName Horvath
107 schema:givenName Andras
108 rdf:type schema:Person
109 Nf6da93768d324c6b81d576c723397ecf rdf:first sg:person.016323171577.36
110 rdf:rest N64f3467c08b64b0096f27c07451f821c
111 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
112 schema:name Information and Computing Sciences
113 rdf:type schema:DefinedTerm
114 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
115 schema:name Artificial Intelligence and Image Processing
116 rdf:type schema:DefinedTerm
117 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
118 schema:name Computation Theory and Mathematics
119 rdf:type schema:DefinedTerm
120 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
121 schema:familyName Kwiatkowska
122 schema:givenName Marta
123 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
124 rdf:type schema:Person
125 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
126 schema:familyName Parker
127 schema:givenName David
128 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
129 rdf:type schema:Person
130 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
131 schema:familyName Norman
132 schema:givenName Gethin
133 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
134 rdf:type schema:Person
135 sg:person.016331342360.82 schema:affiliation grid-institutes:grid.4991.5
136 schema:familyName Santos
137 schema:givenName Gabriel
138 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016331342360.82
139 rdf:type schema:Person
140 grid-institutes:grid.4991.5 schema:alternateName Department of Computing Science, University of Oxford, Oxford, UK
141 schema:name Department of Computing Science, University of Oxford, Oxford, UK
142 rdf:type schema:Organization
143 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, Birmingham, UK
144 schema:name School of Computer Science, University of Birmingham, Birmingham, UK
145 rdf:type schema:Organization
146 grid-institutes:grid.8756.c schema:alternateName School of Computing Science, University of Glasgow, Glasgow, UK
147 schema:name School of Computing Science, University of Glasgow, Glasgow, UK
148 rdf:type schema:Organization
 




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


...