Automated temporal equilibrium analysis: Verification and synthesis of multi-player games
- Submitting institution
-
University of Oxford
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 12011
- Type
- D - Journal article
- DOI
-
10.1016/j.artint.2020.103353
- Title of journal
- Artificial Intelligence
- Article number
- 103353
- First page
- -
- Volume
- 287
- Issue
- -
- ISSN
- 0004-3702
- Open access status
- Compliant
- Month of publication
- June
- Year of publication
- 2020
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
3
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper is concerned with automatically verifying temporal logic properties of game theoretic equilibria in multi-agent systems. Using a widely adopted model for multi-agent systems called concurrent games, the article presents the first dedicated algorithms for this computationally complex problem. The algorithms make use of sophisticated transformations between various classes of infinite tree automata. In addition to presenting mathematical correctness proofs for the algorithms, the paper describes an implementation of the approach in the EVE system, and presents detailed experimental results showing that EVE enjoys considerably better performance than other existing systems for this problem.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -