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.
Kratos – A Software Model Checker for SystemC
