ATL Strategic Reasoning Meets Correlated Equilibrium

ATL Strategic Reasoning Meets Correlated Equilibrium

Xiaowei Huang, Ji Ruan

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 1102-1108. https://doi.org/10.24963/ijcai.2017/153

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 {\it 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 stratgey 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 an 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 problems.
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