ATL Strategic Reasoning Meets Correlated Equilibrium

1 Introduction

On March 2016, Google revealed that its self-driving car hit a bus because it made an incorrect assumption about where it would go [Goo, 2016; TheVerge, 2016]. A simple illustration of the accident is in Figure 1. After its pathway being blocked by sand bags (i.e., scenario (a)), the car on autonomous driving mode intends to merge itself into the tra�c, within which there is a bus coming from the behind. There exist four possibilities that could happen next: the bus lets the car merge into the tra�c first (scenario (b)), which is the one assumed by the car, the car lets the bus pass first (scenario (c)), which is the one assumed by the bus driver, both of them stay still which literally repeats the current scenario (a), and they crash into one another (scenario (d)), which is what actually happened.

The accident provides an example for the study of strategic reasoning by model checking. Model checking [Clarke et al., 1999] is a collection of techniques to automatically verify the correctness of a system against its specification. If described as a multiagent system M and reasoned with existing strategic reasoning frameworks based on ATL model checking [Alur et al., 2002], software model checkers such as MOCHA [Alur et al., 1998], MCK [Huang and van der Meyden, 2014a; Huang, 2015], and MCMAS [ ˇCerm´ak et al., 2014] will be able to claim, by certifying the satisfiability of the relation M; s(a) j= hhcar; busii�:crash on the state s(a) representing the scenario (a), that there exists a joint strategy for the agents to avoid the accident. However, we notice that one of the satisfiable strategies, in which both agents refrain from moving forward, is irrational, so that agents have incentive to deviate from it by committing to other strategies. This observation leads to the restriction of considered strategies to rational strategies, or rational strategic reasoning [Wooldridge et al., 2016]. Furthermore, we notice that randomly selecting an equilibrium from the set of equilibria of certain solution concepts as the joint strategy may lead to the collision of the two agents, including both Nash Equilibria (NEs) and Correlated Equilibria (CEs) [Aumann, 1974].

The main contribution of this paper is to complement the ATL strategic reasoning with new strategic modalities CE ./w G and UCE ./w G for the expressiveness of taking CEs as agents' joint strategies to achieve goal . The semantics of the new modalities optimises the selection of equilibrium over objectives such as the utilitarian value [Greenwald and Hall, 2003]. It is known that deciding the existence of a CE is a computationally easier problem than for NE [Gilboa and Zemel, 1989], and a CE can have a higher utilitarian value than any NE (including both pure and mixed NEs). Beyond cooperative competition 1 through equilibrium, our CE-based model checking can reason about the existence of a CE for a group of agents to compete with the other group of agents in a zerosum way. More specifically, a CE will consider not only the rewards gained for the agents in the group but also the possible behaviour of the other agents which may disable the achievement of some rewards.

1 In this paper, to simply notation, we may call cooperative competition as the collaboration. This is to distinguish with the pure competition in the zero-sum games.

We implement a prototype model checker for CE-based strategic reasoning (which also includes usual ATL strategic reasoning), and thus all the results in our running examples have been formally verified. To the best of our knowledge, this is the first model checker which can reason about CE. Moreover, we study the computational complexity of the model checking problem.

2 Model CheckingMultiagent Systems

We work with the notion of multiagent systems, which comprise of a set of agents running in an environment.

Definition 1 Let Agt be a finite set of agents, each of which has a finite set Acti of actions for i 2 Agt. A multiagent system is a tuple M = (S; I; fNigi2Agt; T; L), where S is a finite set of (environment) states, I � S is a finite set of initial states, Ni : S ! P(Acti) provides agent i with a set of legal actions on every state such that Ni(s) � Acti, T : S � Act ! P(S ) is a (partial) transition function such that Act = �i2AgtActi, and L : S !P(Prop) is a labelling function.

Let ai be agent i's action in the joint action a 2 Act. Agents take their actions independently: for any state s and joint action a such that ai 2 Ni(s) for all i 2 Agt, we have T(s; a) , ;. We define a finite, resp. infinite, path � as a sequence of states s0s1s2::: such that si+1 2 T(si; �) for all i � 0, and denote the set of finite and infinite paths of M starting in s, respectively, by FPathM(s) and IPathM(s), and sets of paths starting from any state by FPathM and IPathM, and omit M if clear from context. For any path � we write �(n) for its (n + 1)-th state, i.e., sn. For a finite path � we write last(�) for its last state. For an infinite path � = s0s1:::, we write �[k::1] for its su�x sk sk+1:::.

For an agent i, a (memoryless and deterministic) strategy �i : S ! Acti is such that �i(s) 2 Ni(s) for all s 2 S . Let �i be a set of strategies for agent i. A joint (pure) strategy �G for a set G � Agt of agents is a vector of strategies (�i)i2G such that �i 2 �i. Let �G = �i2G�i be a set of joint strategies for a set G of agents. When G = Agt, a joint strategy �G is called a strategy profile. The application of a strategy �i on M can be represented as M�i = (S; I; fNigi2Agtnfig S f�ig; T; L) which replace the legal action function Ni of agent i with the strategy �i. Such application can be generalised to a joint strategy �G and obtain M�G.

ATL [Alur et al., 2002] is an expressive language to describe the specifications of a multi-agent system M.

where p 2 Prop and G � Agt. ATL has the expressiveness of CTL [Clarke et al., 1999] as hhAgtii� � 9�. We may also use other standard operators such as �1 ^ �2, ^ �, 8�, etc.

The semantics of ATL over the system M and a state s 2 S is given as the relation M; s j= �, which is defined recursively over the structure of the ATL formula �. Let M0 be the original system without the application of any strategy.

• � Propositional cases are omitted.
• � M; s j= hhGii if there exists some joint strategy �G 2 �G such that M0�G; � j= for all � 2 IPathM0�G (s).

The relation M; � j= is defined recursively for � 2 IPathM.

• � M; � j= � if M; �(0) j= �, for � a state formula
• � M; � j=�� if M; �[1::1] j= �,
• � M; � j= �1U�2 if there exists a number m � 0 such that M; �[k::1] j= �1 for 0 � k � m�1 and M; �[m::1] j= �2,
• � M; � j= � � if M; �[k::1] j= � for all k � 0.

Definition 2 Given a multiagent system M and an ATL formula �, the model checking problem, written as M j= �, is to determine whether M; s j= � for all initial states s 2 I.

3 The Need of Rational Strategy

Consider as a running example a multiagent system in which the decision making scenario of the Google car accident occurs repeatedly.

Example 1 Two autonomous cars, moving in the same direction, repeatedly need to share a common lane as that of scenario (a) in Figure 1 due to the obstacles on the road. In our modelling, each car has three local states fsa; sd; sog, where sa represents that it is approaching the next sharing lane, sd represents the state on which it decides how to handle the situation (give way or occupy), and so represents that it is occupying the lane. If decided to give way, a car will stay in the state sd so that the other car can proceed to occupy the lane. Every car has to occupy the shared lane once to move ahead.

Each car has two actions fm; wg representing the behaviour of moving and waiting, respectively. The environment states are S = fsa; sd; sog�fsa; sd; sog. Initially, we let I = f(sa; sa)g, representing that cars are approaching the first shared lane. The legal action function Ni is Ni(sa) = m, Ni(sd) = fm; wg, and Ni(so) = m. Intuitively, a car may choose to either move to occupy the lane or give way if it is in state sd, and can only move otherwise. The transition function T is deterministic as follows: T((s1; s2); (a1; a2)) = f(s 0 1 ; s 0 2 )g is such that, for all i 2 f1; 2g, if ai = m then (si; s 0 i ) 2 f(sa; sd); (sd; so); (so; sa)g, and if ai = w then si = s 0 i .

Let crash be an atomic proposition that will be labeled on those states on which both cars are in state so. The formula

expresses the existence of strategy profile �Agt to avoid a crash. Assume the following two strategies for agents 2 :

• � �x((sd; sd)) = w and �x(s) = m for s , (sd; sd), and
• � �y(s) = m for s 2 S .

Let agent 1 be the bus and agent 2 be the car in the Google car accident. We can see that, the joint strategy �xy = (�x; �y) results in scenario (b), �yx = (�y; �x) results in scenario (c), �xx = (�x; �x) results in an infinite loop on the decision scenario, and �yy = (�y; �y) results in the accident. It can be concluded that the relation M; s j= �1 for any s 2 S is satisfiable with any joint strategy other than �yy.

2 As there are 6 states, the number of strategies is 2 6 = 64. But to simplify the discussion, we assume that agents always move when they are not in the state (sd; sd); hence this reduces to two strategies.

Note that, every agent has a number j�ij = 2 of strategies, which results in a number j�f1;2gj = 4 of joint strategies.

It is reasonable to assume that in the Google car accident, both the bus and the car are rational agents. However, when reasoning with hhGii , the synthesised strategy can be irrational for the agents (as will be explained in Example 2). If so, a rational agent may refuse to adhere to the strategy, and therefore the strategic reasoning becomes useless.

Following the solution concepts studied in game theory, we define the rationality of a set of agents as the fact that they follow a joint strategy which is an equilibrium with respect to certain solution concept. In this paper, we consider two notable concepts: Nash Equilibirum (NE) [Nash, 1950] and Correlated Equilibrium (CE) [Aumann, 1974]. Intuitively, NE means that every agent knows the strategies of the other agents, and no agent has anything to gain (i.e., the incentive) by changing only his or her own strategy. CE has an intuition that each agent chooses their action according to their observation of the value of the same public signal.

It is known that CE is more general than NE in the sense that all NEs are CEs in a game. More notably, comparing with NE which is PPAD-complete [Daskalakis et al., 2009], CE has a computational advantage that it is polynomial time computable for matrix games [Gilboa and Zemel, 1989]. Moreover, CEs may achieve better performance than NEs: any convex combination of NEs is a CE, but the payo� of a CE can be outside of the convex hull of the NEs' payo�s [Aumann, 1987].

Example 2 (Continue with Example 1) The joint strategy �xx is a strategy for the relation M; s j= �1. However, it can be verified that �xx is neither NE nor CE, and agents find that it is irrational. Intuitively, the joint strategy of both agents refraining from moving forward is undesirable, because it traps the system into an infinite self-loop, and moreover both agents want to deviate from it, because the deviation will bring obvious benefit for them with respect to either NE or CE.

A possible fix to this is to lift formula �1 with components describing the rejection of undesirable situations. However, such a fix means that the formula �1 has to be problem specific by enumerating all undesirable situations, which may not be practical. In this paper, we follow the approach of handling this problem by considering restricting the focus of strategic reasoning on those strategies that are equilibria of certain solution concepts. Each equilibrium corresponds to a collective rational decision of the agents involved.

To formally define equilibrium notions in particular CE 3 , we associate each agent with a set of goals and rewards.

Definition 3 Let Goali be a set of goal-reward pairs (�; w) of agent i, where � is a CTL formula to express a goal that i wants to achieve and w � 0 is a real-valued number representing the reward that i will receive if � is achieved.

We take CTL as the specification language to describe goals because it is su�ciently expressive for many cases and has relatively lower computational complexity on model checking problem comparing to other logics such as LTL. The framework can be easily generalised to other logics.

3 For space limit, we do not present the detail of NE. CE is formally given in Definition 4.

Example 3 (Continue with Example 1) Let pi@x be an atomic proposition that is labelled on those states s such that agent i is on state sx. For example, p2@a means that agent 2 is on state sa. We use formula �2 � 8�:crash to denote that there will never be a crash, and �3(i) � 8�(pi@d ) 9� pi@o) to denote that agent i can move first on the shared lane.

For both agents i 2 f1; 2g, we let Goali include the following goal-reward pairs, where j , i denotes the other agent:

• � (�2 ^ �3(i); 5) (i.e., selfish)
• � (�2 ^ V j,i; j2Agt(:�3(i) ) :�3( j)); 4) (i.e., competitive)
• � (�2 ^ W j,i; j2Agt �3( j); 2) (i.e., selfless)
• � (:�2; 0) (i.e., reckless)

Intuitively, a selfish agent can achieve a reward 5 by ensuring that it can move ahead of the other agent on shared lane. A competitive agent can achieve a reward 4 by ensuring that if it cannot move ahead of the other agent then the other agent cannot either. An selfless agent gets a reward 2 by allowing the other agent to move first. All these three goals are required to avoid crashes. Finally, a reckless agent is discouraged and can only receive a reward 0.

Let M y = (M; fGoaligi2Agt) be the system M enhanced with an additional structure fGoaligi2Agt. For simplicity, in the following we still write M for M y .

4 CE-based Strategic Logic

We extend ATL with two new operators CE and UCE to express correlated equilibrium and call the resulting language ATLUCE. Formally, ATLUCE has the syntax as follows.

where p 2 Prop, G � Agt, ./2 f>; �; �; <g, w 2 R, and w � 0. We define the semantics for the new operators below. CE, in its original definition [Aumann, 1974], addresses the cooperative competition (abbrv. collaboration) within a group. On the other hand, ATL, with formula hhGii , mainly focuses on the pure competition between groups. The general idea of our new formula CE ./w G is to reason about the collaboration of agents in a group G in the form of CE to play against the other agents in achieving a group objective and at the same time optimise the utilitarian value of the group. Based on this, UCE ./w G checks moreover whether the obtained CE is unique.

Collaboration and Competition Formula CE ./w G includes a set G of agents as one of its parameters. Given a pure joint strategy �G, the system M0�G may have other agents Agt nG whose strategies have not been fixed. We follow the intuition used in the original ATL model checking that, for the joint strategy �G to be valid, the system M0�G needs to satisfy the formula 8 , which intuitively means that the strategy �G is able to counter all possible behaviour of agents in Agt n G to ensure the satisfaction of formula . The formula can be seen as a group objective of G.

Meanwhile, whether an agent i 2 G can get a reward w under joint strategy �G and state s is dependent on the satisfaction of both its own goals Goali and the group objective . Formally, we use rs;i(�G; ) to denote the highest reward agent i can get with respect to s; �G; , i.e., rs;i(�G; ) = w if the following three conditions hold

• � M0�G; s j= 8 ,
• � there exists a (�; w) 2 Goali such that M0�G; s j= � and
• � there does not exist a (� 0 ; w 0 ) 2 Goali such that w 0 > w and M0�G; s j= � 0 .

We let rs;i(�G; ) = 0 when either of the first two conditions is not satisfiable. The last two conditions ensure that w is the highest reward agent i can get. Moreover, we let rs;i(�G; ) = 1 if Goali = ; and M0�G; s j= 8 . Now we can define CE in our context.

Definition 4 (Correlated Equilibrium) Given a system M y and a set G of agents with a group objective , a correlated equilibrium on a state s is a probabilistic distribution �G : �G ! [0; 1] such that

Intuitively, Equation (1) says that a CE �G is a probabilistic distribution over the set of pure joint strategies of G, and Equation (2) says that, on a CE �G, if agent i is informed (by e.g., a signal) to play strategy � 1 i then it has no incentive to deviate from this for another strategy � 2 i . The deviation is defined as the di�erence between achievable rewards (i.e., rs;i(�Gnfig� 1 i ; )�rs;i(�Gnfig� 2 i ; )), normalised over the distribution �G on those joint strategies in which agent i takes strategy � 1 i . It is important to note that, when informing agent i to play its strategy � 1 i , the signal does not tell i the strategies for the other agents in G.

Example 4 (Continue with Example 3) Simply taking Equation (1) and (2) with formula = T, our model checker can find a CE �G such that �G(�xy) = �G(�yx) = 0:4, �G(�xx) = 0 and �G(�yy) = 0:2. However, with this CE, there is a non-zero probability that both agents are informed by the signal to play the strategy �y, which will lead to an accident.

This is similar for NE. There are three Nash equilibria, �xy, �yx, and a mixed strategy equilibrium. The mixed strategy NE has a non-zero probability for the accident to occur.

Therefore, in addition to the notorious equilibrium selection problem that agents may follow di�erent equilibria and crash, the above example explains that the accident may still occur even when agents follow the same equilibrium: though both the car and the bus act rationally, there may exist a non-zero probability for a disastrous result to occur. That is, agents' rational behaviour with respect to a random equilibrium may be insu�cient. Moreover, we note that the other two non-mixed NEs have lower utilitarian values comparing to the optimal CE, which will be explained below.

Optimal Equilibrium w.r.t. Utilitarian Value The set of correlated equilibria forms a polytope in the space [0; 1] j�Gj and di�erent equilibria can have very di�erent performance on selection criteria such as utilitarian (i.e., expected sum of the players' total rewards), egalitarian (i.e., expected sum of the weakest player's reward) and plutocratic (i.e., expected sum of the strongest player's reward), in which the expectation is based on the CE which is a distribution.

In this paper, we adopt utilitarian criterion 4 [Greenwald and Hall, 2003] and choose a maximal point from the polytope by maximising the expected sum of the players' total rewards. Formally, to find a maximal CE is to maximise over the following objective function, under the constraints in Equation (1) and (2):

Proposition 1 The size of the linear program (1-3) is polynomial with respect to j�Gj.

Let satG(M; s; ) 2 fT; Fg be the result of whether there exists a solution to the defined optimisation problem, where T and F stand for the propositional true and false, respectively. If satG(M; s; ) = T, we let uG(M; s; ) be the maximal utilitarian value and �G(M; s; ) be one of its associated CEs. It is noted that, there may exist multiple CEs whose utilitarian values are optimal.

Semantics The semantics of the formula CE ./w G is defined as follows.

• � M; s j= CE ./w G if satG(M; s; ) = T and uG(M; s; ) ./ w.

It is noted that, M; s j= CE >0 G implies M; s j= hhGii , but not vice versa. The implication can be seen from the fact that M; s j= CE >0 G implies that there must exist at least one pure joint strategy �G such that M�G; s j= . The latter means that M; s j= hhGii . The unsatisfiability of the other direction can be seen from the possibility that all pure joint strategies satisfying M�G; s j= achieve a reward 0, depending on the definition of goals.

Example 5 (Continue with Example 3) Consider the formula

which asks for the optimal utilitarian value for the agents f1; 2g. By setting group objective as T, the agents do not care about the behaviour of the environment (when no other agents in the system). By checking the relation M; s j= �4 on the initial state s = (sa; sa), we are able to find a CE �G such that �G(�xy) = �G(�yx) = 0:25, �G(�xx) = 0:5 and �G(�yy) = 0, whose associated utilitarian value uf1;2g(M; s; T) is 7:5. It is noted that, the undesirable joint strategy �yy will never occur. The two NEs �xy and �yx have utilitarian value 7.

We show that agents do not have an incentive to deviate from the strategy suggested by the signal. Assume that agent 1 (i.e., the bus) is suggested to follow the strategy �x and wait in front of a shared lane. If the other agent 2 (i.e., the car) sticks with the strategy being suggested by the signal then, because agent 1 does not know which strategy agent 2 is asked to follow, it learns from the CE that agent 2 is asked to follow �x with probability 2=3 and follow �y with probability 1=3. Therefore, the expected sum of its own reward is 1=3�rs;1(�xy; T)+2=3�rs;1(�xx; T) = 1=3�2+2=3�4 = 10=3. If it changes its strategy into �y then the expected sum of its own reward is 1=3�rs;1(�yy; T)+2=3�rs;1(�yx; T) = 1=3�0+2=3�5 = 10=3 � 10=3. Other cases follow the same reasoning.

4 The approach can be generalised to work with other mentioned criteria by updating Equation (3).

The following example illustrates the group objective.

Example 6 (Continue with Example 5) Let �5 = 8�((p1@d ^ p2@d) ) 8� :(p1@d ^ p2@d)) expresses that agents will not loop over the state in which both are at a decision phase. Consider

which asks for the optimal utilitarian value when agents are pursuing the group objective �5. By checking the relation M; s j= �6 on the initial state s = (sa; sa), we are able to find a CE �G such that �G(�xy) = 1 and �G(�yx) = �G(�xx) = �G(�yy) = 0, whose associated utilitarian value is 7:0 < 7:5. To see why �G(�xx) = 0, it is noted that for the group objective �5, the joint strategy �xx will disable agents to achieve rewards because it will make rs;1(�xx; �5) = rs;2(�xx; �5) = 0. So, only joint strategies �xy and �yx are valid strategies.

Moreover, because of the symmetry of the two strategies �xy and �yx, there are an infinite number of CEs �G such that �G(�yx) = p, �G(�xy) = 1 � p, and �G(�xx) = �G(�yy) = 0, for any p 2 [0; 1]. Their optimal utilitarian value is the same.

Now consider the case in which the group of agents have opponents while the group has a trivial objective T.

Example 7 (Continue with Example 5) Assume that there is another agent 3 who can interfere with the group f1; 2g of agents. Its interference behaviour is described as follows: prevent agent 2 from moving when both 1 and 2 are in the decision states. Intuitively, this can be explained as a tra�c rule that a car has to give way to a bus, involuntarily or not. Let M 0 be the new system M by adding agent 3.

By checking M 0 ; s j= �4 on the initial state s = (sa; sa), we are able to find a CE �G which is the same as that in Example 6, i.e., �G(�yx) = 1 and �G(�xy) = �G(�xx) = �G(�yy) = 0. The di�erence exists in their generalisations. For this case, any �G is optimal if it is such that �G(�yx) = p, �G(�yy) = 1 � p, and �G(�xx) = �G(�xy) = 0, for some p 2 [0; 1]. To see this, we note that no matter what agent 2's strategy is, after interfered by the new agent, it is the same as �x.

We remark that, by optimising over the utilitarian value, all the CEs obtained from the above three examples do not allow (with probability 0) the crash to occur. We argue that they are valid theoretical solutions to avoid the Google car accident.

Uniqueness of Optimal Equilibrium After having an optimal utilitarian value and a CE, one might still be interested to learn whether the obtained CE is unique, i.e., whether there exists another CE whose associated utilitarian value is also optimal. A unique CE avoids the equilibrium selection problem, upon which equilibrium notions receive many critiques.

Formally, after obtaining � 0 G = �G(M; s; ), the existence of another optimal CE is equivalent to the existence of an optimal solution to the linear programming problem whose constraints and maximisation objective are those as in Equations (1), (2), and (3), together with one of the following constraints for some �G 2 �G

such that the utilitarian value is the same as uG(M; s; ). Intuitively, Equation (4) means that �G and � 0 G assign di�erent probabilities to at least one of the joint strategies.

Proposition 2 There are a number j2 � �Gj of linear programs (1-4), two for each �G 2 �G.

Let usatG(M; s; ; �G; d) 2 fT; Fg be the existence of a solution to one of the linear programs corresponding to the joint strategy �G and the left or right inequation such that d 2 f>; <g. When usatG(M; s; ; �G; d) = T, we define uuG(M; s; ; �G; d) and u�G(M; s; ; �G; d) as the corresponding utilitarian value and the CE, respectively.

The semantics of the formula UCE ./w G is defined as follows.

• � M; s j= UCE ./w G if M; s j= CE ./w G and there exists some �G 2 �G and d 2 f>; <g such that usatG(M; s; ; �G; d) = T and uuG(M; s; ; �G; d) = uG(M; s; ).

Example 8 (Continue with Example 7) It can be checked that, the CE found in Example 5 is unique, i.e.,

Moreover, as already discussed, the CEs in Example 6 and Example 7 are not unique. We can check that

Implementation of Results in Real-World Scenario For the implementation of a CE-based strategy in real-world scenarios, agents need to agree on playing rationally (i.e., deviate from a strategy only when such deviation can lead to a better reward) according to a correlated equilibrium, before the system starts. Therefore, the computation of CEs can be done o�ine, which is similar with the strategic reasoning by ATLmodel checking. It is noted that such computation needs the goals Goali of all agents i 2 Agt to be publicly known. This is a usual assumption made for complete information systems: for human agents these can be evaluated by rational choice theory [Anand, 1993]; for artificial agents these are pre-preprogrammed before deployment.

During the system execution, agents do not communicate with each other. Instead, there needs to be a signal suggesting them to play specific strategies. As suggested by most CE literature, for each group, the signal is implemented by an extra passive agent changing its state according to the precomputed CE. The state of the passive agent is publicly observable to all agents in the group, and every state of the passive agent is associated with a valid joint strategy in the support of the CE. A notable example of this implementation is the tra�c lights. [Solan and Vieille, 2002] also discusses the correlated devices.

Example 9 (Continue with Example 5) We can use a 4-way tra�c light (0,1,2,3) to act as the signal. On the light 0, agent 1 is informed to follow the strategy �x and agent 2 is informed to follow �y; On the light 1, agent 1 is informed to follow �y and agent 2 is informed to follow �x; On the light 2 and 3, both agents are informed to follow �x. The switches between lights can be implemented with a time-sharing system.

The implementation for Example 6 and 7 can be done in a similar way according to the value p.

5 Software Implementation and Complexity

We implemented the proposed framework into a prototype software model checker 5 . A language based on reactive modules [Alur and Henzinger, 1996] is employed to describe multiagent systems. The prototype tool implements an explicitstate model checking algorithm, see standard textbook such as [Clarke et al., 1999; Alur et al., 2002], to verify temporal formulas. The ATL strategic formulas are checked with the help of a SAT solver. For new formulas CE ./w G and UCE ./w G , a linear constraint solver in SciPy library is used to solve their corresponding linear programming problems (either (1-3) or (1-4)). For satisfiability results, a CE strategy (and its utilitarian value) can be obtained by processing the information returned from the solver. For UCE ./w G , in the worst case, the solver needs to be invoked for 2j�Gj times. All the results in the running example are computed automatically within seconds by the model checker.

In the following, we analyse the computational complexity of the mode checking problem on ATLUCE . Let ATLCE be the fragment in which the UCE operator is removed. Suppose that the number of agents is constant. The complexity is dependent on the measurement. First, assume that the problem is measured over the number of states jS j, the number of joint actions jActj, and the number of operators in the formula j�j.

Theorem 1 If the complexity is measured over jS j, jActj and j�j then model checking ATLUCE is in 2-EXPTIME and model checking ATLCE is in EXPTIME.

The high complexity is because the set j�Agtj is exponential with respect to jS j. The following theorem confirms that the complexity is lower if it is measured over the number j�Agtj of pure joint strategies and the size of the formula.

Theorem 2 If the complexity is measured over j�Agtj and j�j then model checking ATLUCE and ATLCE is in polynomial time.

6 RelatedWork

It is not new that in strategic model checking the ATL does not have the expressiveness to describe equilibrium notions. There are mainly two lines of research trying to counter this weakness. The first is based on the observation that strategies are explicitly quantified in equilibrium notions but implicitly quantified in ATL syntax. The research is focused on introducing additional syntactic structures to directly name and quantify strategies. In [van der Hoek et al., 2005], a formula Ci(�i; �) means that � holds if agent i chooses the strategy �i.

5 https://gitlab.com/xiaowei.huang/rationality.

With this additional structure, it shows that NE is expressible as a formula. In [Chatterjee et al., 2010], the formulas 8x 2 �i : �(x) and 9x 2 �i : �(x) explicitly quantify over the strategies. The logic SL can express a special NE called winning secure equilibrium. In [Mogavero et al., 2014], the formula (i; x)� is to bind agent i to the strategy associated with the variable x. It shows that NE is expressible with the logic. [Aminof et al., 2016] extends [Mogavero et al., 2014] to express and check for uniqueness of NE, with goals expressed in LTL. In [Huang and van der Meyden, 2014b], the formula ei(x) expresses that agent i has the same local state at the current point with the global state represented in x. NE and perfect cooperative equilibrium are shown to be expressible. The second line of research is to reason about Nash equilibrium without the syntax of strategic logics. In [Toumi et al., 2015], an equilibrium checker is to check whether a given strategy profile is an NE. Some complexity results are reviewed in [Wooldridge et al., 2016], where the multi-agent systems are described with iterated boolean games (IBG). IBG can be exponentially more succinct than state-based systems as we do, and therefore their complexities are higher than ours. It is unclear whether CE can be easier than NE for IBG.

Both the above research lines work with non-probabilistic systems and consider only pure (i.e., non-mixed) Nash equilibria. As noted, CE is a concept based on probabilistic distributions. [Koller and Pfe�er, 1995] presents a tool Gala which computes Nash equilibrium by taking sequence form which is linear in the size of the game tree. Progresses on stochastic games have been survey in [Chatterjee and Henzinger, 2011], including reasoning based on NEs. This thread of research does not work with temporal logics, except for [Huang et al., 2012; Huang and Luo, 2013; Chen et al., 2013], which are based on extending ATL to stochastic systems and cannot reason about equilibrium notions. Moreover, the extension of ATL on probabilistic dimension is also investigated in the probabilistic software model checker PRISM [Chen et al., 2013] on turn-based games (instead of concurrent games as most literature on multiagent systems does). As most of the research reviewed in the above, PRISM cannot compute equilibria.

For the computation of CEs, except for the linear programming approach as we employed, multiagent learning, see e.g., [Shoham et al., 2007; Busoniu et al., 2008] for comprehensive reviews, focuses on extending the reinforcement learning approaches to a multiagent setting. In particular, [Greenwald and Hall, 2003] presents an extension of the Q-learning algorithm to find a CE. However, the algorithm cannot guarantee the convergence because a multiagent setting breaks an essential assumption for Q-learning to converge: the environment is non-stationary for a learner [Sandholm, 2007].

7 Conclusion

In this paper, we integrate correlated equilibrium into ATL strategic model checking. New CE operators are introduced to describe a group of agents collaborating to compete with their opponents and at the same time optimising their utilitarian value. A software model checker has been implemented to enable automated reasoning. The complexity of the model checking problem is also studied.