Reasoning about equilibria in game-like concurrent systems (Q345709)

The main purpose of this paper is to design a logical framework for reasoning about equilibria in multi-agent games. The arenas of such games are simple labelled graphs such that the games are of infinite duration and the players' goals are considered to be temporal, i.e.\ expressible as formulas of some temporal logic. The authors then present a logic that syntactically extends the temporal branching-time logic CTL\(^*\) with a new kind of quantification which is to be read as ``on all paths obtained as the outcome of a (Nash) equilibrium strategy profile''. The main technical result of this paper is the classification of the computational complexity of the model checking problem for this logic which is in fact rather a family of logics, parametrised by the way that outcomes are specified in the underlying games and possibly by restrictions on the use of the equilibrium quantifiers. The general result portrays the model checking as quite difficult, namely hard for doubly exponential time, in very simple cases already. The paper is very much written in an overview style. Focus is given to the motivation of this framework through various examples, as well as first results on the computational problems that naturally come with the introduction of a formal logic. Proof details are hardly given; instead this paper links to other papers from which techniques are taken or where similarities can be discovered. It also points out various aspects that have yet to be uncovered, resp.\ problems on such logics that have yet to be solved like general upper bounds for instance.