On the counting of strategies
In game theory, a classic qualitative question is to check whether a designated set of players has a winning strategy. In several safety-critical applications, however, it is important to ensure that some redundant strategies also exist, to be possibly used in case of some fault. In this paper, we i...
| 主要な著者: | , , , |
|---|---|
| フォーマット: | Conference item |
| 出版事項: |
Institute of Electrical and Electronics Engineers
2016
|
| _version_ | 1826260489562226688 |
|---|---|
| author | Malvone, V Mogavero, F Murano, A Sorrentino, L |
| author_facet | Malvone, V Mogavero, F Murano, A Sorrentino, L |
| author_sort | Malvone, V |
| collection | OXFORD |
| description | In game theory, a classic qualitative question is to check whether a designated set of players has a winning strategy. In several safety-critical applications, however, it is important to ensure that some redundant strategies also exist, to be possibly used in case of some fault. In this paper, we introduce Graded Strategy Logic (GSL), an extension of Strategy Logic (SL) with graded quantifiers. SL is a powerful formalism that allows to describe useful game concepts in multi-agent settings by explicitly quantifying over strategies treated as first-order citizens. In GSL, by means of the existential construct 〈〈x ≥ g〉〉φ one can enforce that there exist at least g strategies satisfying φ. Dually, via the universal construct [[x <; g]]φ one can ensure that all but less than g strategies satisfy φ. As different strategies may induce the same outcome, although looking different, they need to be counted as one. While this interpretation is natural, it heavily complicates the definition and thus the reasoning about GSL. In order to accomplish this specific way of counting, we formally introduce a suitable equivalence relation over profiles based on the strategic behavior they induce. To give evidence of GSL usability, we investigate basic questions of one of its vanilla fragment, namely GSL[1G]. In particular, we report on positive results about the determinacy of games and the related model-checking problem, which we show to be PTIME-COMPLETE. |
| first_indexed | 2024-03-06T19:06:26Z |
| format | Conference item |
| id | oxford-uuid:154c56f9-2238-46e5-813a-6165ced04286 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T19:06:26Z |
| publishDate | 2016 |
| publisher | Institute of Electrical and Electronics Engineers |
| record_format | dspace |
| spelling | oxford-uuid:154c56f9-2238-46e5-813a-6165ced042862022-03-26T10:24:42ZOn the counting of strategiesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:154c56f9-2238-46e5-813a-6165ced04286Symplectic Elements at OxfordInstitute of Electrical and Electronics Engineers2016Malvone, VMogavero, FMurano, ASorrentino, LIn game theory, a classic qualitative question is to check whether a designated set of players has a winning strategy. In several safety-critical applications, however, it is important to ensure that some redundant strategies also exist, to be possibly used in case of some fault. In this paper, we introduce Graded Strategy Logic (GSL), an extension of Strategy Logic (SL) with graded quantifiers. SL is a powerful formalism that allows to describe useful game concepts in multi-agent settings by explicitly quantifying over strategies treated as first-order citizens. In GSL, by means of the existential construct 〈〈x ≥ g〉〉φ one can enforce that there exist at least g strategies satisfying φ. Dually, via the universal construct [[x <; g]]φ one can ensure that all but less than g strategies satisfy φ. As different strategies may induce the same outcome, although looking different, they need to be counted as one. While this interpretation is natural, it heavily complicates the definition and thus the reasoning about GSL. In order to accomplish this specific way of counting, we formally introduce a suitable equivalence relation over profiles based on the strategic behavior they induce. To give evidence of GSL usability, we investigate basic questions of one of its vanilla fragment, namely GSL[1G]. In particular, we report on positive results about the determinacy of games and the related model-checking problem, which we show to be PTIME-COMPLETE. |
| spellingShingle | Malvone, V Mogavero, F Murano, A Sorrentino, L On the counting of strategies |
| title | On the counting of strategies |
| title_full | On the counting of strategies |
| title_fullStr | On the counting of strategies |
| title_full_unstemmed | On the counting of strategies |
| title_short | On the counting of strategies |
| title_sort | on the counting of strategies |
| work_keys_str_mv | AT malvonev onthecountingofstrategies AT mogaverof onthecountingofstrategies AT muranoa onthecountingofstrategies AT sorrentinol onthecountingofstrategies |