Paper deep dive
Representation Theorems for Actual Powers over Two-Agent General Concurrent Game Frames
Zixuan Chen, Fengkui Ju, Thomas Ă gotnes
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 93%
Last extracted: 10/14/2026, 9:06:58 AM
Summary
This paper establishes representation theorems for actual powers in two-agent general concurrent game frames. It demonstrates that eight classes of general concurrent game frames, defined by combinations of seriality, independence, and determinism, correspond to eight corresponding classes of actual neighborhood frames. This work generalizes previous results by van Benthem et al. (2019) which were restricted to singleton coalitions, providing a finer-grained account of coalition power than alpha effectivity.
Entities (15)
Relation Signals (10)
Actual Power â distinguishesfrom â Alpha Power
confidence 95% ¡ Actual powers, by contrast, record the precise outcome set generated by an available coalition action... they are generally not upward closed.
Chen, Ju, and Ă gotnes â proposed â Actual Representation Theorem
confidence 95% ¡ In this paper, assuming two agents, we prove that, in terms of actual powers, the eight classes of general concurrent game frames are represented by eight corresponding classes of neighborhood frames.
Actual Neighborhood Frame â represents â General Concurrent Game Frame
confidence 95% ¡ we prove that, in terms of actual powers, the eight classes of general concurrent game frames are represented by eight corresponding classes of neighborhood frames.
General Concurrent Game Frame â characterizedby â Seriality
confidence 90% ¡ GCGF is serial if, for all CâAG and all sâST, we have av C (s)â â
General Concurrent Game Frame â characterizedby â Independence
confidence 90% ¡ GCGF is independent if, for all sâST and all disjoint coalitions C,DâAG, whenever Ď C âav C (s) and Ď D âav D (s), we have Ď C âŞĎ D âav CâŞD (s)
General Concurrent Game Frame â characterizedby â determinism
confidence 90% ¡ GCGF is deterministic if, for all sâST and all Ď AG âav AG (s), the set out AG (s,Ď AG ) is a singleton.
van Benthem, Bezhanishvili, and Enqvist â critiqued â Alpha Power
confidence 90% ¡ as pointed out by van Benthem, Bezhanishvili, and Enqvist (2019), that fact can obscure relevant information about the power structure in the game
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:One of the most well-known connections between logic and games is Pauly's representation theorem: the induced powers of individuals and coalitions in concurrent game frames correspond, in a precise sense, to a certain class of neighborhood frames. The precise sense here is what is called alpha effectivity (or alpha power): the power of a coalition is characterized by the sets of states in which it can ensure that the outcome lies by taking some joint action. This definition is inherently monotonic, and, as pointed out by van Benthem, Bezhanishvili, and Enqvist (2019), that fact can obscure relevant information about the power structure in the game: we do not know whether two sets that a coalition has the power to enforce correspond to the same joint action or to different joint actions. An alternative is to characterize the power of a coalition by its actual power (called basic power by van Benthem, Bezhanishvili, and Enqvist (2019)): the collection of sets of states, each of which corresponds to one joint action by the coalition and all possible joint actions by the other agents. It has recently been argued by Li and Ju (2025, 2026) that standard concurrent game frames rely on three assumptions that may, in some cases, be too strong: seriality, independence of agents, and determinism. This yields a total of eight different classes of general concurrent game frames. In this paper, assuming two agents, we prove that, in terms of actual powers, the eight classes of general concurrent game frames are represented by eight corresponding classes of neighborhood frames. This generalizes a result by van Benthem, Bezhanishvili, and Enqvist (2019).
Tags
Links
- Source: https://arxiv.org/abs/2610.15476v1
- Canonical: https://arxiv.org/abs/2610.15476v1
Trouble viewing inline? Open PDF directly â
Full Text
48,268 characters extracted from source content.
Expand or collapse full text
G. Bacci, M. Randour (Eds.): Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2026) EPTCS 454, 2026, p. 67â83, doi:10.4204/EPTCS.454.6 Š Z. Chen, F. Ju & T. Ă gotnes This work is licensed under the Creative Commons Attribution License. Representation Theorems for Actual Powers over Two-Agent General Concurrent Game Frames Zixuan Chen Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, The Netherlands zixuan.chen21@outlook.com Fengkui Ju * School of Philosophy, Beijing Normal University, Beijing, China fengkui.ju@bnu.edu.cn Thomas Ă gotnes Department of Information Science and Media Studies, University of Bergen, Bergen, Norway School of Philosophy, Shanxi University, Taiyuan, China thomas.agotnes@uib.no One of the most well-known connections between logic and games is Paulyâs representation theo- rem: that the induced powers of individuals and coalitions in concurrent game frames correspond, in a precise sense, to a certain class of neighborhood frames. The precise sense here is what is called alpha effectivity(oralpha power): the power of a coalition is characterized by the sets of states which it can ensure the outcome to lie in by taking some joint action. This definition is inherently mono- tonic, and, as pointed out by [3], that fact can obscure relevant information about the power structure in the game: we donât know whether two sets a coalition has the power to enforce correspond to the same or different joint actions. An alternative is to characterise the power of a coalition by its actual power(calledbasic powerin [3]): the set of sets of states where each corresponds to one joint action by the coalition and all possible joint actions by the other agents. It has recently been argued [8, 9] that standard concurrent game frames rely on three assumptions that in some cases may be too strong: seriality, independence of agents, and determinism. This gives a total of eight different classes ofgeneralconcurrent game frames. In this paper, assuming two agents, we prove that for actual powers, the eight classes of general concurrent game frames are represented by eight corresponding classes of neighborhood frames. This generalises a result in [3]. 1 Introduction Concurrent game framesare a standard semantic framework for logics of strategic reasoning. Many influential logics in this area are interpreted over concurrent game frames, including Coalition LogicCL [11] and Alternating-time Temporal LogicATL[2]. Roughly speaking, a concurrent game frame consists of states and agents (forming coalitions), where, at each state, every coalition has available joint actions, and each such action induces a set of possible outcome states. Two notions of coalition power arise from concurrent game frames:alpha powersandactual powers. Analpha powerof a coalition is a set of possible futures such that the coalition has an action that forces every resulting outcome to lie in that set. Alpha power is also known as alpha effectivity. Anactual powerof a coalition is a set of possible futures such that the coalition has an action satisfying both of the * Corresponding author 68Representation Theorems for Actual Powers following conditions: (1) the action forces every resulting outcome to lie in the set, and (2) every future state in the set is realizable by the complement coalition (and the environment). Thus, unlike alpha powers, actual powers explicitly involve agents outside the coalition. Note that actual powers contain more information about the power structure than alpha powers: we can get the latter from the former, but not the other way around. Correspondingly, one obtains two kinds of neighborhood frames:alpha neighborhood framesand actual neighborhood frames. In an alpha neighborhood frame, each coalition is assigned analpha neigh- borhood functionthat, at every state, specifies analpha neighborhood, i.e., a set of alpha powers. In an actual neighborhood frame, each coalition is assigned anactual neighborhood functionthat, at every state, specifies anactual neighborhood, i.e., a set of actual powers. Alpha powersare widely used in game theory; see, e.g., [10]. By contrast, there appears to be com- paratively little work onactualpowers. To the best of our knowledge, the main reference is van Benthem, Bezhanishvili, and Enqvist [3]. Working primarily from the perspective of game equivalence, they in- vestigatebasicpowers of singleton coalitions in turn-based two-agent extensive games with imperfect information, defined in terms of (uniform) strategies. Conceptually, this notion of basic power coincides with what we callactualpower. Alpha and actual powers abstract away from the underlying actions in different ways. Alpha powers record guarantees: if a coalition has an action whose possible outcomes are contained in a setX, then the same action also guarantees any superset ofX. Hence alpha powers are upward closed. Actual powers, by contrast, record the precise outcome set generated by an available coalition action: the set of states left possible once that action is fixed and the choices of the remaining agents are left open. They are therefore generally not upward closed. As observed in [3], describing a game solely in terms of its alpha powers can therefore lose information about its power structure, whereas actual powers provide a finer-grained account. Because actual powers retain the outcomes left open to agents outside the coalition, they are useful for modeling social scenarios in which a coalitionâs ability depends not only on what it can guarantee, but also on what its action leaves open to others. A central logical example is Socially Friendly Coali- tion Logic [6]. Its operator[C](Ď;Ď 1 ,...,Ď k )expresses that coalition C has a collective actionĎ C that guaranteesĎwhile allowing the complementary coalition C to realize each of the alternativesĎ 1 ,...,Ď k by a suitable response. This semantic clause is the coalition-indexed, action-based counterpart of the instantial neighborhood operatorâĄ(Ď;Ď 1 ,...,Ď k )of [4]. Equivalently, in actual-neighborhood terms, there must be an actual powerXof C such that every state inXsatisfiesĎand, for everyiâ¤k,Xcon- tains some state satisfyingĎ i . The latter requirement depends on the precise outcome range and cannot be captured by alpha powers alone. Every concurrent game frame induces an alpha neighborhood frame. Pauly [11] and Goranko, Jam- roga, and Turrini [7] showed that the class of concurrent game frames isrepresentedby a class of alpha neighborhood frames characterized by certainbasicproperties of neighborhood functions, in the fol- lowing sense: (1) every alpha neighborhood frame induced by a concurrent game frame satisfies these properties, and (2) every alpha neighborhood frame satisfying these properties is induced by some con- current game frame. This result is thealpha representation theoremfor concurrent game frames. Every concurrent game frame also induces an actual neighborhood frame. Do there existbasicprop- erties of neighborhood functions such that (1) every actual neighborhood frame induced by a concurrent game frame satisfies these properties, and (2) every actual neighborhood frame satisfying these proper- ties is induced by some concurrent game frame? If so, this would be anactual representation theorem for concurrent game frames. Z. Chen, F. Ju & T. Ă gotnes69 This question has not yet been fully settled in the literature. As far as we are aware, the only closely related result is due to van Benthem, Bezhanishvili, and Enqvist [3]. There, the authors establish a representation theorem forbasic(strategy-based) powers in turn-based two-agent extensive games with imperfect information, under the restriction to singleton coalitions. Via a standard power-invariance transformation between the class of two-agent concurrent game frames and an appropriate class of turn- based two-agent extensive games with imperfect information, their proof readily yields a representation theorem for actual powers in two-agent concurrent game frames, again restricted to singleton coalitions (see [5] for details). Let us briefly discuss the significance of representation theorems for alpha and actual powers. What are the powers of players, and coalitions of players, in games? Which sets of outcomes â known as eventsin probability theory orpropositionsin logic â is it in their power to make come about, in the sense that they can choose a (joint) action such that no matter what the other agents do, this is what will happen? This abstracts away the particulars of a game, and leaves an abstract representation of power which is exactly what we are often interested in when we analyse games. In order to understand power in games, the central question then is: what are theproperties(oraxiomsorlaws) of individual and coalitional power induced from games in this way? That is exactly what Paulyâs representation theorem [11] answers, for alpha powers. This is the main motivation, and the main significance of also the representation theorems for actual power: giving us a deeper understanding of the power in games. Representation theorems can also yield alternative neighborhood semantics for some logics origi- nally interpreted over concurrent game models. This makes the whole toolchest developed to deal with neighbourhood semantics available. Such semantics are also often more economical and convenient. Whereas a concurrent game frame explicitly records action names, availability functions, and outcome functions, many modal languages for strategic reasoning depend only on the powers induced by actions: what coalitions can force in the case of alpha powers, or the exact outcome ranges generated by coalition actions in the case of actual powers. Representation theorems therefore justify replacing action-based models with neighborhood-based models, without changing truth conditions. Paulyâs representation the- orem for alpha powers provides a prominent example: it allows the semantics ofCLover concurrent game frames to be transferred to alpha neighborhood frames. Pauly [11] used such frames to prove com- pleteness ofCL, while Ă gotnes and Alechina [1] employed the same semantic framework to extendCL with knowledge. Li and Ju [8, 9] argued that standard concurrent game frames impose three assumptions that may be too strong in practice:seriality,independence of agents, anddeterminism. For motivating examples, see [8]. They introduced eight classes of general concurrent game frames, corresponding to the eight possible combinations of these assumptions, and studied the generalized coalition logic associated with each class. In this paper, assuming two agents, we establish the following result: for actual powers, the eight classes of general concurrent game frames are represented by eight corresponding classes of actual neighborhood frames. Our proof method relies essentially on the two-agent setting, and does not ex- tend directly to settings with three or more agents. We briefly explain this at the end of Section 4. The remainder of the paper is organized as follows. In Section 2, we introduce the general frame- work used throughout the paper, including action frames, alpha and actual powers, actual neighborhood frames, and representability of action frames by actual neighborhood frames. In Section 3, we define the eight classes of general concurrent game frames. In Section 4, we define eight classes of actual neigh- borhood frames via eight finite sets of properties of actual neighborhood functions, and show that, for actual powers, the eight classes of general concurrent game frames (with two agents) are represented by 70Representation Theorems for Actual Powers the corresponding eight classes of actual neighborhood frames. In Section 5, we conclude the paper with final remarks. Due to space limitations, we omit some material that can be found in the full paper [5]. Moreover, building on the representation result for actual powers established in this paper, the full paper shows that, for alpha powers, the same eight classes are represented by eight corresponding classes of alpha neighborhood frames. 2 Preliminaries In this section, we proceed as follows. First, we introduceaction framesin an abstract form; specific constraints will be imposed later. Second, we discussalpha powersandactual powers, and briefly compare them. Third, we presentactual neighborhood frames. These are again introduced at an abstract level, with additional constraints to be added in subsequent sections. Finally, we define how action frames are represented by actual neighborhood frames. 2.1 Action frames LetAGbe a finite nonempty set of agents. Subsets ofAGare calledcoalitions, andAGitself is called the grand coalition. In what follows, whenever no confusion arises, we writeainstead ofaforaâAG. LetACbe a nonempty set of actions. For each CâAG, defineJA C =Ď C |Ď C : CâAC, the set of joint actionsof C. NoteJA /0 =/0. For C,DâAGsuch that CâD, and for everyĎ D âJA D , we denote byĎ D | C therestrictionofĎ D to C, which is an element ofJA C . In the sequel, we sometimes represent joint actions of coalitions as action sequences, implicitly assuming a fixed order of agents. Definition 2.1(Action frames).Anaction frameis a tuple AF= (ST,AC,av C |CâAG,out C |CâAG), where: â˘STis a nonempty set of states. â˘ACis a nonempty set of actions. ⢠For each CâAG,av C :STâP(JA C )is anavailability functionfor C. Here,av C (s)is the set of all joint actions of coalitionCthat are available at state s. ⢠For each CâAG,out C :STĂJA C âP(ST)is anoutcome functionfor C. Here,out C (s,Ď C )is the set of possible outcome states when coalitionCperforms joint actionĎ C at state s. Note that the action setACmay vary across action frames. Different constraints may be imposed on action frames. Intuitively,out /0 (s,/0)contains all states to whichsmay evolve, i.e., all possible successors ofs. 2.2 Alpha and actual powers Fix an action frame AF= (ST,AC,av C |CâAG,out C |CâAG), Z. Chen, F. Ju & T. Ă gotnes71 a statesâST, a coalition CâAG, and an available joint actionĎ C âav C (s). We say that a set of states XâSTissafeforĎ C atsifout C (s,Ď C )âX, that is, performingĎ C atsguarantees that the next state lies inX. We say thatXistightforĎ C atsifXâout C (s,Ď C ), that is, every state inXcan occur as an outcome compatible with performingĎ C ats. Analpha powerof C atsis a set of statesXâSTthat is safe for some available joint action of C ats. Anactual powerof C atsis a set of statesXâSTthat is both safe and tight for some available joint action of C ats. Equivalently, actual powers of C atsare exactly the sets of the formout C (s,Ď C ) forĎ C âav C (s). We say that an (alpha or actual) powerXenablesa statetâSTatsiftâX. Alpha powers are monotonic: ifXis an alpha power, then every supersetX ⲠâXis also an alpha power. By contrast, actual powers are generally non-monotonic, since tightness rules out adding states that are not actually reachable. The following example illustrates the distinction between alpha and actual powers. Example 2.2.Consider two AI-driven robots,aandb, controlling a warehouse gate. The robots send their commands to the gate controller simultaneously, but robotahas higher authority than robotb. There are two relevant states,W=w 1 ,w 2 , wherew 1 represents the gate being closed andw 2 represents the gate being open. Robotahas three actions:open a ,close a , anddelegate a . The first opens the gate, the second closes it, and the third delegates the decision to robotb. Robotbhas two actions:open b andclose b . We consider two scenarios. In both, ifachoosesopen a , the gate opens, and ifachoosesclose a , the gate closes, regardless ofbâs action. The scenarios differ only in the effect ofdelegate a . In the first scenario, delegation works as intended: whenadelegates,bâs action determines whether the gate opens or closes. In the second scenario, delegation is ineffective: whenadelegates, the gate closes regardless ofbâs action. The two scenarios induce the same alpha powers for every coalition: coalitionalpha powers /0W a w 1 ,w 2 ,W bW a,b w 1 ,w 2 ,W . Their actual powers differ. In the first scenario, the actual powers ofaare w 1 ,w 2 ,W , corresponding to closing, opening, and delegating, respectively. In the second scenario, they are only w 1 ,w 2 . Indeed, delegation no longer leaves both outcomes open, but instead has the same exact outcome set asclose a . 2.3 Actual neighborhood frames Definition 2.3(Actual neighborhood frames).Anactual neighborhood frameis a tuple NF ac = (ST,N ac C |CâAG), where: â˘STis a nonempty set of states; ⢠For each CâAG, N ac C :STâP(P(ST))is anactual neighborhood functionof C. 72Representation Theorems for Actual Powers Different constraints may be imposed on actual neighborhood frames. The set N ac C (s)is called the actual neighborhoodof C ats. Intuitively, N ac C (s)consists of the actual powers of coalition C at state s. In the intended interpretation, S N ac /0 (s)consists of all states to whichsmay evolve, i.e., the possible successors ofs. Structurally, actual neighborhood frames are ordinary coalition-indexed neighborhood frames. The qualifier âactualâ merely emphasizes that their neighborhoods are interpreted as representing the actual powers of coalitions. 2.4 Representation of action frames by actual neighborhood frames Definition 2.4(Actual effectivity functions of action frames).LetAF= (ST,AC,av C |CâAG,out C | CâAG)be an action frame. For each CâAG, define: ⢠theactual effectivity functionEF ac C for C inAFby setting, for everysâST, EF ac C (s) =out C (s,Ď C )|Ď C âav C (s). Definition 2.5(AC-representability of action frames).LetAF= (ST,AC,av C |CâAG,out C |CâAG) be an action frame. We say thatAFisAC-representedby an actual neighborhood frame NF ac = (ST,N ac C |CâAG) if, for every CâAG, we have EF ac C =N ac C . Intuitively,AC-representability means that the actual neighborhood frame captures all information about the actual powers of coalitions in the action frame. Definition 2.6(AC-representability of classes of action frames).LetAFbe a class of action frames. We say thatAFisAC-representedby a class of actual neighborhood framesAC-NFif: ⢠Every action frame inAFisAC-represented by some actual neighborhood frame inAC-NF; ⢠Every actual neighborhood frame inAC-NFAC-represents some action frame inAF. Suppose that a class of action frames isAC-represented by a class of actual neighborhood frames. Intuitively, this means that, as far as actual powers are concerned, one can translate the information carried by action frames into the corresponding neighborhood frames. Now fix a class of action framesAFand a collection of properties of actual neighborhood frames. To show thatAFisAC-represented by the class of actual neighborhood frames satisfying these properties, it suffices to establish the following two statements: â˘Havingness(necessity): every actual neighborhood frame thatAC-represents an action frame in AFsatisfies these properties; â˘Enoughness(sufficiency): every actual neighborhood frame satisfying the propertiesAC-represents an action frame inAF. Later we will follow exactly this pattern. Z. Chen, F. Ju & T. Ă gotnes73 3 General concurrent game frames and eight classes In this section, we present the eight classes of general concurrent game frames considered by Li and Ju [8, 9]. Later, assuming two agents, we establish theirAC-representability. Definition 3.1(General concurrent game frames).An action frame GCGF= (ST,AC,av C |CâAG,out C |CâAG) is ageneral concurrent game frameif the following conditions hold: ⢠Thegrand-coalition-induced outcome condition(simply theGCI-condition): for every CâAG, everysâST, and everyĎ C âJA C , out C (s,Ď C ) = [ out AG (s,Ď AG )|Ď AG âJA AG andĎ AG | C =Ď C . ⢠Theoutcome-driven availability condition(simply theODA-condition): for every CâAGand everysâST, av C (s) =Ď C âJA C |out C (s,Ď C )̸=/0. Thus, under the GCI-condition and the ODA-condition, the functionsout C andav C (for all CâAG) are determined by the grand-coalition outcome functionout AG . Definition 3.2(Seriality, independence, and determinism).LetGCGF= (ST,AC,av C |CâAG,out C | CâAG)be a general concurrent game frame. We say that: â˘GCGFisserialif, for all CâAGand allsâST, we haveav C (s)̸=/0; â˘GCGFisindependentif, for allsâSTand all disjoint coalitions C,DâAG, wheneverĎ C âav C (s) andĎ D âav D (s), we haveĎ C âŞĎ D âav CâŞD (s); â˘GCGFisdeterministicif, for allsâSTand allĎ AG âav AG (s), the setout AG (s,Ď AG )is a singleton. LetS,I, andDdenote seriality, independence, and determinism, respectively. Let ES=Îľ,S,I,D,SI,SD,ID,SID be the set of the eight strings encoding all combinations of these three properties. HereÎľdenotes the empty combination. ForXâES, we say that a general concurrent game frame is anX-frameif it satisfies the properties indicated byX. The following facts will be used implicitly throughout the sequel. Fact 3.3.Let GCGF= (ST,AC,av C |CâAG,out C |CâAG) be a general concurrent game frame. Then the following hold: 1.Outcome monotonicity:for all sâST, allCâDâAG, allĎ C âJA C , and allĎ D âJA D such that Ď D | C =Ď C , we have out D (s,Ď D )âout C (s,Ď C ). 2.Alternative GCI-condition:for all sâST, allCâAG, and allĎ C âJA C , out C (s,Ď C ) = [ out AG (s,Ď AG )|Ď AG âav AG (s)andĎ AG | C =Ď C . The first item is an immediate consequence of the GCI-condition, and the second is a reformulation of the GCI-condition using the ODA-condition (since unavailable grand-coalition actions have empty outcome sets). 74Representation Theorems for Actual Powers 4 Representing actual powers In this section, we proceed as follows. First, we define eight classes ofAC-representative actual neigh- borhood frames and establish several basic facts about them. Second, under the assumption that there are exactly two agents, we show that each of the eight classes of general concurrent game frames intro- duced in the previous section isAC-represented by the corresponding class ofAC-representative actual neighborhood frames. The representability result has two directions:havingnessandenoughness. 4.1 Eight classes ofAC-representative actual neighborhood frames The following definitions are stated for an arbitrary finite set of agentsAG. Later, we prove the represen- tation theorem under the assumption that|AG|=2 for the enoughness direction. The havingness direction does not require the two-agent restriction. Definition 4.1(AC-representative actual neighborhood frames).LetNF ac = (ST,N ac C |CâAG)be an actual neighborhood frame. We say thatNF ac isAC-representativeif the following conditions are satis- fied: 1.Actual triviality of the empty coalition:for allsâST, if N ac /0 (s)is nonempty, then it is a singleton. Intuitively, this condition says that the empty coalition has at most one actual power. Having more than one actual power would amount to having more than one choice, hence the name. 2.Liveness:for allsâSTand all CâAG, we have /0/âN ac C (s). Intuitively, this condition rules out the degenerate actual power/0for any coalition. Note that liveness does not force coalitions to have powers; it only rules out treating the empty set as a âpowerâ when powers exist. 3.Actual power inclusion:for allsâSTand all C,DâAGwith CâD, for allXâN ac D (s)there existsYâN ac C (s)such thatXâY. Intuitively, every actual power of a larger coalition is included in some actual power of a smaller coalition. 4.Actual power decomposition:for allsâSTand all C,DâAGwith CâD, for everyXâN ac C (s) there existsââN ac D (s)such thatX= S â. Intuitively, every actual power of a smaller coalition can be decomposed into (possibly many) actual powers of a larger coalition. We use âAC-representativeâ for actual neighborhood frames satisfying the intrinsic conditions in- tended to characterize those thatAC-represent general concurrent game frames. Note âAC-representativeâ and âAC-representableâ are defined in different ways. Definition 4.2(Seriality, independence, and determinism ofAC-representative actual neighborhood fra- mes).LetNF ac = (ST,N ac C |CâAG)be anAC-representative actual neighborhood frame. We say that: â˘NF ac isAC-serialif for allsâSTand all CâAG, we have N ac C (s)̸=/0. â˘NF ac isAC-independentif, for allsâSTand all C,DâAGwith CâŠD=/0, wheneverXâN ac C (s) andYâN ac D (s), there existsZâN ac CâŞD (s)such thatZâXâŠY. Intuitively, for disjoint coalitions, any two actual powers can be jointly refined to an actual power of their union that is compatible with both. Z. Chen, F. Ju & T. Ă gotnes75 â˘NF ac isAC-deterministicif for allsâSTand allXâN ac AG (s),Xis a singleton. As before, we let the three symbolsS,I, andDdenoteAC-seriality,AC-independence, andAC- determinism, respectively. We also reuse the set ES=Îľ,S,I,D,SI,SD,ID,SID, whose elements serve as labels for the eight possible combinations of these three properties. For eachXâES and eachAC-representative actual neighborhood frameNF ac , we say thatNF ac is an X-frameif it satisfies the properties corresponding toX. What follows are several basic facts aboutAC-representative actual neighborhood frames. These facts are useful both for intuition and for later technical developments. Again, we refer to [5] for their proofs. The first fact shows that the set of states reachable from a given state is independent of the coalition: all coalitions share the same set of successors of that state. Fact 4.3.LetNF ac = (ST,N ac C |CâAG)be anAC-representative actual neighborhood frame. For all sâSTand allCâAG, we have [ N ac C (s) = [ N ac /0 (s). The next fact shows that emptiness of the set of actual powers at a state does not depend on the coalition: either every coalition has actual power ats, or none does. Fact 4.4.LetNF ac = (ST,N ac C |CâAG)be anAC-representative actual neighborhood frame. For all sâSTand allCâAG, N ac C (s) =/0iffN ac /0 (s) =/0. The following fact shows that if the empty coalition has any actual power at a states, then it has exactly one: namely, the overall successor set ofs. Fact 4.5.LetNF ac = (ST,N ac C |CâAG)be anAC-representative actual neighborhood frame. For all sâST, ifN ac /0 (s)̸=/0, then N ac /0 (s) = [ N ac AG (s) . The final fact states that, when moving from a smaller coalition to a larger one, every actual powerX of the smaller coalition can be recovered as the union of those actual powers of the larger coalition that are included inX. Fact 4.6.LetNF ac = (ST,N ac C |CâAG)be anAC-representative actual neighborhood frame. For every sâST, allC,DâAGwithCâD, and every XâN ac C (s), [ ZâN ac D (s)|ZâX=X. 4.2 Representation theorems for actual powers Theorem 4.7(Actual havingness theorem).LetXâES. For every actual neighborhood frame, if it AC-represents a general concurrent gameX-frame, then it is anAC-representative actual neighborhood X-frame. Proof.LetNF ac = (ST,N ac C |CâAG)be an actual neighborhood frame. Suppose thatNF ac AC- represents a general concurrent gameX-frame GCGF= (ST,AC,av C |CâAG,out C |CâAG). Then for every coalition CâAGand every statesâST, we have N ac C (s) =EF ac C (s). 76Representation Theorems for Actual Powers We show thatNF ac is anX-frame.We verify that each of the propertiesS,I, andDis preserved under AC-representation. It then follows, sinceGCGFis anX-frame, thatNF ac is anX-frame. â˘Seriality.Assume thatGCGFis serial. FixsâSTand CâAG. Thenav C (s)̸=/0, and hence EF ac C (s) =out C (s,Ď C )|Ď C âav C (s)̸=/0. Therefore N ac C (s)̸=/0, and thusNF ac isAC-serial. â˘Independence.Assume thatGCGFis independent. FixsâSTand disjoint coalitions C,DâAG with CâŠD=/0. LetXâN ac C (s)andYâN ac D (s). Since N ac C =EF ac C and N ac D =EF ac D , there exist Ď C âav C (s)andĎ D âav D (s)such thatout C (s,Ď C ) =Xandout D (s,Ď D ) =Y. By independence ofGCGF, we haveĎ C âŞĎ D âav CâŞD (s). LetZ=out CâŞD (s,Ď C âŞĎ D ). ThenZâ EF ac CâŞD (s) =N ac CâŞD (s). Moreover, sinceĎ C âĎ C âŞĎ D andĎ D âĎ C âŞĎ D , by outcome monotonicity, we haveZâXandZâY, and henceZâXâŠY. ThereforeNF ac isAC-independent. â˘Determinism.AssumeGCGFis deterministic. FixsâSTandXâN ac AG (s). ThenXâEF ac AG (s), so there existsĎ AG âav AG (s)such thatout AG (s,Ď AG ) =X. By determinism ofGCGF,out AG (s,Ď AG )is a singleton; hence so isX. ThereforeNF ac isAC-deterministic. We show thatNF ac satisfies the fourAC-representativeness conditions. 1.Actual triviality of the empty coalition.FixsâST. Note that out /0 (s,/0) = [ out AG (s,Ď AG )|Ď AG âJA AG . Ifout /0 (s,/0)̸=/0, then by definition of EF ac /0 we have N ac /0 (s) =EF ac /0 (s) =out /0 (s,/0), so N ac /0 (s)is a singleton. Ifout /0 (s,/0) =/0, thenav /0 (s) =/0 and hence N ac /0 (s) =EF ac /0 (s) =/0. 2.Liveness.FixsâSTand CâAG. Since EF ac C (s) =out C (s,Ď C )|Ď C âav C (s) and eachĎ C âav C (s)satisfiesout C (s,Ď C )̸=/0, we obtain /0/âEF ac C (s). Thus /0/âN ac C (s). 3.Actual power inclusion.FixsâSTand coalitions CâDâAG. LetXâN ac D (s) =EF ac D (s). Then there existsĎ D âav D (s)such thatout D (s,Ď D ) =X. WriteĎ D =Ď C âŞĎ D withĎ C âJA C and Ď D âJA D . SinceĎ D is available for D, its restrictionĎ C is available for C, i.e.,Ď C âav C (s). Moreover,out D (s,Ď D )âout C (s,Ď C ).LetY=out C (s,Ď C ). ThenYâEF ac C (s) =N ac C (s)andXâY, as required. 4.Actual power decomposition.FixsâSTand coalitions CâDâAG. LetXâN ac C (s) =EF ac C (s). Then there existsĎ C âav C (s)such thatout C (s,Ď C ) =X. LetÎ=Ď AG âav AG (s)|Ď C âĎ AG . By the GCI-condition ofGCGFand Fact 3.3, X=out C (s,Ď C ) = [ out AG (s,Ď AG )|Ď AG âÎ. Consider the family â=out D (s,Ď AG | D )|Ď AG âÎ. Z. Chen, F. Ju & T. Ă gotnes77 For eachĎ AG âÎ, we haveout AG (s,Ď AG )̸=/0 andout AG (s,Ď AG )âout D (s,Ď AG | D ), henceĎ AG | D â av D (s)and thereforeout D (s,Ď AG | D )âEF ac D (s) =N ac D (s). ThusââN ac D (s). It remains to show thatX= S â. (â)LetuâX. Thenuâout AG (s,Ď AG )for someĎ AG âÎ, henceuâout D (s,Ď AG | D )and thus uâ S â. (â)Letuâ S â. Thenuâout D (s,Ď AG | D )for someĎ AG âÎ. By the GCI-condition ofGCGF, there existsÎť AG âJA AG such thatĎ AG | D âÎť AG anduâout AG (s,Îť AG ). SinceĎ C âĎ AG | D âÎť AG andÎť AG is available, we haveÎť AG âÎ. Hence uâ [ out AG (s,Ď AG )|Ď AG âÎ=X. This completes the proof. Theorem 4.8(Actual enoughness theorem).AssumeAG=a,b. LetXâES. EveryAC-representative actual neighborhoodX-frameAC-represents some general concurrent gameX-frame. The proof is somewhat involved; we refer to [5] for an illustrative example. Proof. Analysis of the task.LetNF ac = (ST,N ac C |CâAG)be anAC-representative actual neighborhood X-frame. We aim to construct a general concurrent gameX-frame GCGF= (ST,AC,av C |CâAG,out C |CâAG) such thatGCGFisAC-represented byNF ac . All conditions defining general concurrent gameX-frames are statewise: for each source states, they involve only the availability setsav C (s)and the outcome mapsout C (s,¡), and do not relate these information to those at a distinct source statet. Consequently, the required availability and outcome information can be constructed independently at each state. The resulting local constructions can then be combined by using pairwise disjoint, state-tagged action sets and taking their union as the global action set. Therefore, it suffices to proceed as follows: for eachsâST, starting from the local neighborhood structure N=N ac C (s)|CâAG, we construct a local structure G= AC s ,av C (s)|CâAG,out C (s,¡)|CâAG satisfying the following conditions. 1.Gis a local component (called alocal game) of a general concurrent game frame: (a)AC s is a set of actions. (b) For every CâAG,av C (s)âJA C . (c) For every CâAGand everyĎ C âJA C ,out C (s,Ď C )âST. 78Representation Theorems for Actual Powers (d) For every CâAG: av C (s) =Ď C âJA C |out C (s,Ď C )̸=/0. (e) For every CâAGand everyĎ C âJA C , the actionĎ C satisfies the GCI-condition ats: out C (s,Ď C ) = [ out AG (s,Ď AG )|Ď AG âav AG (s)andĎ C âĎ AG . 2.GisAC-represented byN, i.e., for every CâAG, out C (s,Ď C )|Ď C âav C (s)=N ac C (s). 3.Ghas the properties corresponding toX. FixsâST. In the sequel, to simplify notation, we drop the explicit mention ofs. More precisely: ⢠We write N ac C for N ac C (s). ⢠We writeACforAC s . ⢠We writeav C forav C (s). ⢠We writeout C (Ď C )forout C (s,Ď C ). The trivial case.Assume N ac /0 =/0. By Fact 4.4, we have N ac C =/0 for every CâAG. Define a game G= (AC,av C |CâAG,out C |CâAG)as follows: ⢠LetACbe any nonempty set (e.g., a singleton). ⢠For every CâAG, letav C =/0. ⢠For every CâAGand everyĎ C âJA C , letout C (Ď C ) =/0. It is straightforward to verify thatGsatisfies the requirements in the analysis above. Assume now that N ac /0 ̸=/0. Construction of a local game.By Fact 4.4, none of N ac a , N ac b , and N ac AG is empty. Assume N ac a =X i |iâI,N ac b =Y j |jâJ,N ac AG =Z k |kâK, whereI,J,Kare index sets. InitializeG= (AC,av C |CâAG,out C |CâAG)by settingAC=/0 and leaving allav C andout C empty. We will add actions, availability, and outcomes step by step untilGsatisfies conditions 1â3. Before the construction, we fix some terminology and conventions, and also give some quick preview of what we are going to do next: ⢠Byindividual powerswe mean powers ofaor ofb. ⢠Actions inACwill have the formÎą nâXâZ andβ nâYâZ , wherenâ1,2,3,XâN ac a ,YâN ac b , and ZâN ac AG satisfyZâXandZâY. We regard the indexnas indicating thelevel(three groups). Joint actions ofAGwill have the form(Îą nâXâZ ,β mâYâZ Ⲡ) AllÎą nâXâZ will be available actions ofa, and allβ nâYâZ will be available actions ofb. We will stipulate out a (Îą nâXâZ ) =Xandout b (β nâYâZ ) =Y. Z. Chen, F. Ju & T. Ă gotnes79 We say thatÎą nâXâZ is anameofX, and thatβ nâYâZ is a name ofY. Available joint actions ofAGwill be introduced gradually. Not every such pair must be available, since independence need not hold. Whenever we declare(Îą nâXâZ ,β mâYâZ Ⲡ)to be available, we will simultaneously specify its outcome setout AG (Îą nâXâZ ,β mâYâZ Ⲡ) =Z Ⲡ. In that case we say that the joint action is a name ofZ Ⲡ. ⢠For any available actionÎąofa, saying that wemakeÎąsatisfy the GCI-conditionmeans that we ensure out a (Îą) = [ out AG (Îą,β) | βis available forband(Îą,β)is available forAG . The same interpretation applies to any available actionβofb. ⢠SupposeÎąis an available action ofaandβis an available action ofb. Saying that wepairÎąand βmeans that we make(Îą,β)an available action ofAGand specify its outcome set. ⢠LetÎąbe an available action ofaandβan available action ofb. Declaring(Îą,β)to be an available joint action with outcomeZis calledsafe(forÎąandβ) if Zâout a (Îą)âŠout b (β). In that case, adding this pair cannot destroy the GCI-condition forÎąor forβ: if either action already satisfies its GCI-condition before the addition, it still satisfies it afterwards. ⢠Any joint action not explicitly declared available will be treated as unavailable, with outcome /0. The construction consists of three steps. Step 1: introducing names for individual powers.For everyXâN ac a , everyZâN ac AG withZâX, and everynâ1,2,3, letÎą nâXâZ be an available action ofasuch thatout a (Îą nâXâZ ) =X. For everyYâN ac b , everyZâN ac AG withZâY, and everynâ1,2,3, letβ nâYâZ be an available action ofbsuch thatout b (β nâYâZ ) =Y. The reason that we need three levels of individual actions will be given later. Step 2: enforcing the GCI-condition for names of individual powers.For eachXâN ac a define â X =ZâN ac AG |ZâX, and for eachYâN ac b defineâ Y =ZâN ac AG |ZâY. Note that by Fact 4.6, S â X =X for each XâN ac a and S â Y =Y for each YâN ac b . 1.Make all Group 1 names ofasatisfy the GCI-condition.Pick an available actionÎą 1âXâZ ofa. For everyZ Ⲡââ X , choose someYâN ac b such thatZ ⲠâY, and declare(Îą 1âXâZ ,β 2âYâZ Ⲡ)to be an available action ofAGwith out AG (Îą 1âXâZ ,β 2âYâZ Ⲡ) =Z Ⲡ. Note that such a Y exists for every Z Ⲡââ X , by actual power inclusion inN. Note that for every Z Ⲡââ X ,β 2âYâZ Ⲡis a Group 2 action of b. After this, every Z Ⲡââ X has a name extendingÎą 1âXâZ , andÎą 1âXâZ satisfies the GCI-condition.Repeat this procedure for any remaining Group 1 action ofanot yet satisfying the GCI-condition. 2.Make all Group 1 names ofbsatisfy the GCI-condition.Proceed analogously for Group 1 actions ofbnot yet satisfying the GCI-condition.Here we only pair such actions of b with Group 2 actions of a. 80Representation Theorems for Actual Powers 3.Make all Group 2 names ofasatisfy the GCI-condition.Proceed analogously.Here we only pair such actions of a with Group 3 actions of b. Note that the pairing is safe. 4.Make all Group 2 names ofbsatisfy the GCI-condition.Proceed analogously.Here we only pair such actions of b with Group 3 actions of a. Note that the pairing is safe. 5.Make all Group 3 names ofasatisfy the GCI-condition.Proceed analogously.Note that at this point, no Group 1 action of b has been paired with a Group 3 action of a. Here we only pair Group 3 actions of a with Group 1 actions of b. Note that the pairing is safe. 6.Make all Group 3 names ofbsatisfy the GCI-condition.Proceed analogously.Note that at this point, no Group 1 action of a has been paired with a Group 3 action of b. Here we only pair Group 3 actions of b with Group 1 actions of a. Note that the pairing is safe. We now explain why three levels of individual actions are used. The idea behind Step 2 is to make the names of individual powers satisfy the GCI-condition one level at a time. For a nameÎąof an individual power, this means ensuring that its outcome set is exactly the union of the outcome sets of its available joint extensions. To achieve this for names at one level, we add joint extensions using names of the other agent at the next level: Group 1 names are handled using Group 2 names, and Group 2 names are handled using Group 3 names. If this procedure were continued linearly, it would seem to require a further level to handle Group 3 names. The point of the three-level construction is that the process closes cyclically. When Group 3 names are treated, the corresponding Group 1 names of the other agent are already available and already satisfy their own GCI-condition, and they have not yet been paired with the Group 3 names currently under consideration. We can therefore pair Group 3 names with Group 1 names. These new pairings are safe, so they do not destroy the GCI-condition already achieved for the Group 1 names. Thus no fourth level is needed. Step 3: pair names of individual powers whenever possible.Pick any available actionsÎą nâXâZ Ⲡof aandβ mâYâZ Ⲡofb(at arbitrary levelsn,mâ1,2,3) such that: ⢠They have not been paired yet, and ⢠There existsZâN ac AG withZâout a (Îą nâXâZ Ⲡ)âŠout b (β mâYâZ Ⲡ). Choose such aZ, and declare(Îą nâXâZ Ⲡ,β mâYâZ Ⲡ)to be an available action ofAGwith out AG (Îą nâXâZ Ⲡ,β mâYâZ Ⲡ) =Z. Repeat for all remaining pairs satisfying the conditions above. Final local game.Finally, defineG= (AC,av C |CâAG,out C |CâAG)as follows: ⢠LetACbe the set of all actions specified at Step 1. ⢠Letav /0 =/0andout /0 (/0) = S N ac AG . ⢠Letav a ,out a be as specified above; similarly forav b ,out b ; and letav AG ,out AG be as specified above. We verify the ODA-condition and GCI-condition forG. Z. Chen, F. Ju & T. Ă gotnes81 ⢠For the ODA-condition, first consider the nontrivial case. Every individual action declared avail- able in Step 1 has an outcomeXâN ac a orYâN ac b , and every grand-coalition action declared available in Steps 2 and 3 has an outcomeZâN ac AG . All these outcome sets are nonempty by liveness. Moreover, out /0 (/0) = [ N ac AG ̸=/0, so /0âav /0 . Conversely, every action or joint action not explicitly declared available is assigned the empty outcome. Hence, for every CâAG, av C =Ď C âJA C |out C (Ď C )̸=/0. In the trivial case, all availability sets and outcome sets are empty, so the same equality holds. ⢠For the GCI-condition, the case C=AGis immediate, since a grand-coalition action has only itself as a grand-coalition extension. Now letÎą nâXâZ âav a . In Step 2, extensions of this action are introduced whose outcome sets cover every member of â X =Z ⲠâN ac AG |Z ⲠâX. Since S â X =Xby Fact 4.6, the union of the outcomes of these extensions isout a (Îą nâXâZ ) = X. Every extension added in Step 3 is safe, and therefore has its outcome contained inX; such extensions do not change this union. The argument for available actions ofbis symmetric. If an individual action is unavailable, no available grand-coalition action extends it, and both sides of the GCI equality are empty. Finally, consider C=/0. Every available grand-coalition action has an outcome in N ac AG . Conversely, everyZâN ac AG occurs as the outcome of some available grand-coalition action: by actual power inclusion, chooseXâN ac a withZâX; Step 2 assigns outcomeZto an extension ofÎą 1âXâZ . Consequently, [ Ď AG âJA AG out AG (Ď AG ) = [ N ac AG =out /0 (/0). Thus the GCI-condition holds for every coalition. HenceGsatisfies the defining conditions of a local general concurrent game frame. HenceGis a game. We show thatGisAC-represented byN.It suffices to show that for every CâAG, out C (Ď C )|Ď C âav C =N ac C . The inclusion âââ is immediate from the construction. For C=/0, by the definition of the final local game, we have the following equalities:out /0 (Ď /0 )|Ď /0 âav /0 =out /0 (/0)= n [ N ac AG o =N ac /0 ,where the last equality follows from Fact 4.5. For C=aor C=b, the reverse inclusion is also immediate from Step 1. It remains to show the reverse inclusion for C=AG, i.e., that everyZâN ac AG has a name. LetZâN ac AG . By actual power inclusion,ZâXfor someXâN ac a , henceZââ X . Consider the actionÎą 1âXâZ introduced in Step 1. In Step 2 we choose someYâN ac b withZâYand declare (Îą 1âXâZ ,β 2âYâZ )to be an available action ofAGwithout AG (Îą 1âXâZ ,β 2âYâZ ) =Z. ThusZhas a name, as required. Therefore,GisAC-represented byN. 82Representation Theorems for Actual Powers We show thatGhas the properties corresponding toX. â˘Seriality.AssumeSâX. ThenNF ac isAC-serial, hence N ac C ̸=/0 for all CâAG. In particular, pick XâN ac a and chooseZâN ac AG withZâX. ThenÎą 1âXâZ is available fora, soav a ̸=/0. Similarly, av b ̸=/0. Also, since N ac AG ̸=/0, there existsĎ AG âav AG without AG (Ď AG )âN ac AG , henceav AG ̸=/0. Finally,av /0 =/0by definition. Thereforeav C ̸=/0 for all CâAG. â˘Independence.AssumeIâX. ThenNF ac isAC-independent. Let C,DâAGwith CâŠD=/0, and letĎ C âav C andĎ D âav D . We show thatĎ C âŞĎ D âav CâŞD . If C=/0 or D=/0, the claim is immediate. Otherwise, sinceAG=a,b, both C and D are singletons; without loss of generality let C=aand D=b. WriteĎ a =ÎąandĎ b =β, and let out a (Îą) =Xandout b (β) =Y. ByAC-independence ofNF ac , there existsZâN ac AG such thatZâXâŠY. If(Îą,β)was already declared available in Step 2, then(Îą,β)âav AG . Otherwise, the existence of such aZshows that the unpaired actionsÎąandβsatisfy the criterion of Step 3. Hence Step 3 declares(Îą,β)available and assigns it some outcomeZ ⲠâN ac AG withZ ⲠâXâŠY. Thus, in either case,Ď a âŞĎ b = (Îą,β)âav AG =av CâŞD .ThereforeGsatisfies independence. â˘Determinism.AssumeDâX. ThenNF ac isAC-deterministic, so everyZâN ac AG is a singleton. By construction, for everyĎ AG âav AG we haveout AG (Ď AG )âN ac AG , henceout AG (Ď AG )is a singleton. RemarkThe conditions used above remain necessary for arbitrary finite agent sets, but they cease to be sufficient once three agents are present. Actual power inclusion and actual power decomposition con- strain powers only along inclusions of coalitions. With three agents, however, incomparable coalitions may overlap. For example, the restrictions of a full joint action toa,banda,cmust agree on their commona-component; consequently, their outcome sets must both be contained in the outcome set in- duced by the same action ofa. The conditions used here do not ensure that the witnesses along these two inclusion chains can be chosen compatibly. This obstruction does not arise with two agents, since no two incomparable proper nonempty coalitions have a nonempty intersection. Thus, a general finite-agent representation theorem requires additional coherence conditions for the actual powers of overlapping coalitions. A concrete three-agent counterexample is given in the full paper [5]. 5 Concluding remarks Concurrent game frames are the most widely used semantic frames for logics of strategic reasoning. Li and Ju [8, 9] argued that standard concurrent game frames rely on three assumptions that may be overly strong, namely seriality, independence of agents, and determinism. They therefore proposed eight classes of general concurrent game frames, distinguished by which of these three properties are satisfied. In this work, under the assumption that there are two agents, we showed that with respect to actual powers, the eight classes of general concurrent game frames are represented by eight corresponding classes of actual neighborhood frames. This generalizes the result in [3], which proves a partial representation theorem, for singleton coalitions only and not for the empty or grand coalitions, for the most standard case. The preceding remark identifies the obstruction to extending the enoughness direction beyond two agents. A natural next step is to formulate appropriate general finite-agent coherence conditions and seek a genuine general finite-agent representation theorem for actual powers. Z. Chen, F. Ju & T. Ă gotnes83 Acknowledgments We thank the three anonymous reviewers of the 17th International Symposium on Games, Automata, Logics, and Formal Verification for their valuable comments and constructive suggestions. Fengkui Ju was supported by âthe Fundamental Research Funds for the Central Universitiesâ in China (No. 1253200057). Thomas Ă gotnes was supported by Major Project of National Social Science Founda- tion of China (Grant No. 24&ZD227). References [1] Thomas Ă gotnes & Natasha Alechina (2019):Coalition logic with individual, distributed and common knowledge.Journal of Logic and Computation29(7), p. 1041â1069, doi:10.1093/logcom/exv085. [2] Rajeev Alur, Thomas A. Henzinger & Orna Kupferman (2002):Alternating-Time Temporal Logic. Journal of the ACM49(5), p. 672â713, doi:10.1145/585265.585270. [3] Johan van Benthem, Nick Bezhanishvili & Sebastian Enqvist (2019):A New Game Equivalence, its Logic and Algebra.Journal of Philosophical Logic48(4), p. 649â684, doi:10.1007/s10992- 018-9489-7. [4] Johan van Benthem, Nick Bezhanishvili, Sebastian Enqvist & Junhua Yu (2017):In- stantial Neighbourhood Logic.Reviews of Symbolic Logic10(1),p. 116â144, doi:10.1017/S1755020316000447. [5] Zixuan Chen, Fengkui Ju & Thomas Ă gotnes (2026):Representation theorems for actual and alpha powers over two-agent general concurrent game frames, doi:10.48550/arXiv.2603.04160. arXiv:2603.04160. [6] Valentin Goranko & Sebastian Enqvist (2018):Socially friendly and group protecting coalition logics. In:Proceedings of the 17th International Conference on Autonomous Agents and MultiA- gent Systems (AAMAS 2018), International Foundation for Autonomous Agents and Multiagent Systems, p. 372â380, doi:10.5555/3237383.3237442. Available athttps://dl.acm.org/doi/ abs/10.5555/3237383.3237442. [7] Valentin Goranko, Wojciech Jamroga & Paolo Turrini (2013):Strategic Games and Truly Playable Effectivity Functions.Journal of Autonomous Agents and Multi-Agent Systems26(2), p. 288â 314, doi:10.1007/s10458-012-9192-y. [8] Yinfeng Li & Fengkui Ju (2025):A minimal coalition logic.Journal of Logic and Computation 35(8), p. exaf059, doi:10.1093/logcom/exaf059. [9] Yinfeng Li & Fengkui Ju (2026):Completeness of coalition logics with seriality, independence of agents, or determinism.Journal of Logic, Language and Information, doi:10.1007/s10849-026- 09457-z. [10] HervĂŠ Moulin & Bezalel Peleg (1982):Cores of effectivity functions and implementation theory. Journal of Mathematical Economics10(1), p. 115â145, doi:10.1016/0304-4068(82)90009-X. [11] Marc Pauly (2002):A Modal Logic for Coalitional Power in Games.Journal of Logic and Compu- tation12(1), p. 149â166, doi:10.1093/logcom/12.1.149.