Seven kinds of equivalent models for generalized coalition logics

TL;DR

The paper shows that for every one of Li and Ju's eight coalition logics grounded in grand-coalition-first action models, the same valid formulas are established by six alternative model classes: single-coalition-first action models, single-coalition-first actual neighborhood models, clear grand-coalition-first action models, clear single-coalition-first actual neighborhood models, tree-like grand-coalition-first action models, and tree-like single-coalition-first actual neighborhood models. It develops precise representation theorems (z- and α-representability) between action-based and neighborhood-based formalisms, and extends these results to structured variants like clear and tree-like models, including unravellings that preserve truth. The work unifies eight logics under a common semantic umbrella, showing that the same coalitional powers can be captured across six complementary semantic frameworks, with implications for modeling and reasoning about coordination and strategic ability. It also outlines pathways for future research, notably integrating richer languages such as ATL and STIT, and refining the distinctions between action quantification and outcome determinism in coalition reasoning.

Abstract

Coalition Logic is an important logic in logical research on strategic reasoning. In two recent papers, Li and Ju argued that generally, concurrent game models, models of Coalition Logic, have three too strong assumptions: seriality, independence of agents, and determinism. They presented eight coalition logics based on eight classes of general concurrent game models, determined by which of the three assumptions are met. In this paper, we show that each of the eight sets of valid formulas of the eight logics is determined by six other kinds of models, that is, single-coalition-first action models, single-coalition-first actual neighborhood models, clear grand-coalition-first action models, clear single-coalition-first actual neighborhood models, tree-like grand-coalition-first action models, and tree-like single-coalition-first actual neighborhood models.

Figures (4)

• Figure 1: This figure is used to show that in grand-coalition-first action models, the set of outcome states of a joint action might not contain the intersection of the sets of outcome states of the joint action's parts.
• Figure 2: This figure indicates two grand-coalition-first action models for Example \ref{['example:not compositional']}.
• Figure 3: This figure indicates a grand-coalition-first action model for the situation of Example \ref{['example:two']}. Here: $c_f$ and $c_b$, respectively, express the front door is closed and the back door is closed; $(\mathtt{open}\text{-}\mathtt{f}, \mathtt{skip})$ represents a joint action where Adam closes the front door and Bob does nothing, and so on. It can be checked that in this model, the set of outcomes of a joint action is the intersection of the sets of outcomes of individual actions of the joint action. For example: (1) $\mathsf{out}_\mathtt{AG} (s_1, (\mathtt{skip}, \mathtt{skip})) = \mathsf{out}_a (s_1, \mathtt{skip}) \cap \mathsf{out}_b (s_1, \mathtt{skip}) = \{s_1,s_2\} \cap \{s_1,s_3\} = \{s_1\}$; (2) $\mathsf{out}_\mathtt{AG} (s_2, (\mathtt{skip},\mathtt{close}\text{-}\mathtt{b})) = \mathsf{out}_a (s_2, \mathtt{skip}) \cap \mathsf{out}_b (s_2, \mathtt{close}\text{-}\mathtt{b}) = \{s_1,s_2\} \cap \{s_1\} = \{s_1\}$; (3) $\mathsf{out}_{\{a,b\}} (s_3, (\mathtt{close}\text{-}\mathtt{f}, \mathtt{skip})) = \mathsf{out}_a (s_3, \mathtt{close}\text{-}\mathtt{f}) \cap \mathsf{out}_b (s_3, \mathtt{skip}) = \{s_1\} \cap \{s_1,s_3\} = \{s_1\}$.
• Figure 4: This figure indicates a grand-coalition-first action model for the situation of Example \ref{['example:two processes']}. It can be checked that in this model, the set of outcomes of a joint action is the intersection of the sets of outcomes of individual actions of the joint action. For example: (1) $\mathsf{out}_\mathtt{AG} (s_1, (\mathtt{skip}, \mathtt{skip})) = \mathsf{out}_{a}(s_1, \mathtt{skip}) \cap \mathsf{out}_{b}(s_1, \mathtt{skip}) = \{s_1\} \cap \{s_1\} = \{s_1\}$; (2) $\mathsf{out}_\mathtt{AG} (s_2, (\mathtt{skip}, \mathtt{y:=1})) = \mathsf{out}_{a}(s_2, \mathtt{skip}) \cap \mathsf{out}_{b}(s_2, \mathtt{y:=1}) = \{s_1, s_2\} \cap \{s_1\} = \{s_1\}$; (3) $\mathsf{out}_\mathtt{AG} (s_4, (\mathtt{x:=1}, \mathtt{y:=1})) = \mathsf{out}_{a}(s_4, \mathtt{x:=1}) \cap \mathsf{out}_{b}(s_4, \mathtt{y:=1}) = \{s_1,s_2\} \cap \{s_1,s_3\} = \{s_1\}$.

Theorems & Definitions (73)

• Definition 1: The language $\Phi$
• Definition 2: Action models
• Definition 3: Action semantics
• Definition 4: Actual neighborhood models
• Definition 5: Alpha neighborhood models
• Definition 6: Neighborhood semantics
• Definition 7: Actual effectivity functions and alpha effectivity functions of action models
• Definition 8: Action models $z$-representable by actual neighborhood models and $\alpha$-representable by alpha neighborhood models
• Theorem 1: Representability implies equivalence
• Definition 9: Grand-coalition-first action models