Authors: Xiaowei Huang and Ji Ruan
Abstract: This paper is motivated by analysing a Google self-driving car accident, i.e., the car hit a bus, with the framework and the tools of strategic reasoning by model checking. First of all, we find that existing ATL model checking may find a solution to the accident with irrational joint strategy of the bus and the car. This leads to a restriction of treating both the bus and the car as rational agents, by which their joint strategy is an equilibrium of certain solution concepts. Second, we find that a randomly-selected joint strategy from the set of equilibria may result in the collision of the two agents, i.e., the accident. Based on these, we suggest taking Correlated Equilibrium (CE) as agents' joint strategy and optimising over the utilitarian value which is the expected sum of the agents' total rewards. The language ATL is extended with two new modalities to express the existence of a CE and a unique CE, respectively. We implement the extension into a software model checker and use the tool to analyse the examples in the paper. We also study the complexity of the model checking problem.
Keywords: Knowledge Representation, Reasoning, and Logic: Automated Reasoning and Theorem Proving Agent-based and Multi-agent Systems: Coordination and cooperation Agent-based and Multi-agent Systems: Formal verification, validation and synthesis
Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence Main track. Pages 1102-1108. https://doi.org/10.24963/ijcai.2017/153
BibTex:
author = {Xiaowei Huang, Ji Ruan},
title = {ATL Strategic Reasoning Meets Correlated Equilibrium},
booktitle = {Proceedings of the Twenty-Sixth International Joint Conference on
Artificial Intelligence, {IJCAI-17}},
pages = {1102--1108},
year = {2017},
doi = {10.24963/ijcai.2017/153},
url = {https://doi.org/10.24963/ijcai.2017/153},
}
