Malvone, Vadim
(2018)
Strategic Reasoning in Game Theory.
[Tesi di dottorato]
| Item Type: |
Tesi di dottorato
|
| Resource language: |
English |
| Title: |
Strategic Reasoning in Game Theory |
| Creators: |
| Creators | Email |
|---|
| Malvone, Vadim | vadim.malvone@unina.it |
|
| Date: |
2018 |
| Number of Pages: |
191 |
| Institution: |
Università degli Studi di Napoli Federico II |
| Department: |
dep12 |
| Dottorato: |
phd090 |
| Ciclo di dottorato: |
30 |
| Coordinatore del Corso di dottorato: |
| nome | email |
|---|
| De Giovanni, Francesco | francesco.degiovanni2@unina.it |
|
| Tutor: |
| nome | email |
|---|
| Murano, Aniello | UNSPECIFIED |
|
| Date: |
2018 |
| Number of Pages: |
191 |
| Keywords: |
Games; Logics; Strategies |
| Settori scientifico-disciplinari del MIUR: |
Area 01 - Scienze matematiche e informatiche > INF/01 - Informatica |
[error in script]
[error in script]
| Date Deposited: |
18 Dec 2017 14:05 |
| Last Modified: |
08 Apr 2019 10:29 |
| URI: |
http://www.fedoa.unina.it/id/eprint/12091 |
Collection description
Game theory in AI is a powerful mathematical framework largely applied in the last three decades for the strategic reasoning in multi-agent systems. Seminal works along this line started with turn-based two-player games (under perfect and imperfect information) to check the correctness of a system against an unpredictable environment. Then, large effort has been devoted to extend those works to the multi-agent setting and, specifically, to efficiently reasoning about important solution concepts such as Nash Equilibria and the like. Breakthrough contributions along this direction concern the introduction of logics for the strategic reasoning such as Alternating-time Temporal Logic (ATL), Strategy Logic (SL), and their extensions.
Two-player games and logics for the strategic reasoning are nowadays very active areas of research. In this thesis we significantly advance the work along both these two lines of research by providing fresh studies and results of practical application.
We start with two-player reachability games and first investigate the problem of checking whether a designed player has more than a winning strategy to reach a target. We investigate this question under both perfect and imperfect information. We provide an automata-based solution that requires linear-time, in the perfect information setting, and exponential-time, in the imperfect one. In both cases, the results are tight. Then, we move to multi-player concurrent games and study the following specific setting: (i) Player_0's objective is to reach a target W, and (ii) the opponents are trying to stop this but have partial observation about Player_0's actions. We study the problem of deciding whether the opponents can prevent Player_0 to reach W. We show, using an automata-theoretic approach that, assuming the opponents have the same partial observation and play under uniformity, the problem is in ExpTime. We recall that, in general, multi-player reachability games with imperfect information are undecidable.
Then, we move to the more expressive framework of logics for the strategic reasoning. We first introduce and study two graded extensions of SL, namely GSL and GradedSL. By the former, we define a graded version over single strategy variables, i.e. "there exist at least g different strategies", where the strategies are counted semantically. We study the model checking-problem for GSL and show that for its fragment called vanilla GSL[1G] the problem is PTime-complete. By GradedSL, we consider a graded version over tuple of strategy variables and use a syntactic counting over strategies. By means of GradedSL we show how to count the number of different strategy profiles that are Nash equilibria (NE). By analyzing the structure of the specific formulas involved, we conclude that the important problem of checking for the existence of a unique NE can be solved in 2ExpTime, which is not harder than merely checking for the existence of such an equilibrium.
Finally, we adopt the view of bounded rationality, and look only at "simple" strategies in specifications of agents’ abilities. We formally define what "simple" means, and propose a variant of plain ATL, namely NatATL, that takes only such strategies into account. We study the model checking problem for the resulting semantics of ability and obtain tight results. The positive results achieved with NatATL encourage for the investigation of simple strategies over more powerful logics, including SL.
Downloads per month over past year
Actions (login required)
 |
View Item |
