Abstract
This paper is motivated by analysing a Google selfdriving 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