Representation theorems for actual and alpha powers over two-agent general concurrent game frames

Abstract

One of the most well-known connections between modal logic and games is Pauly's representation theorem: that the induced powers of individuals and coalitions in a concurrent game frame correspond, in a precise sense, to a certain class of neighborhood models. The precise sense here is what is called \emph{alpha effectivity} (or \emph{alpha 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 monotonic, and, as pointed out by \cite{benthem_new_2019}, 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 \emph{actual powers} (called \emph{basic powers} in \cite{benthem_new_2019}): 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 \cite{li_minimal_2025, li_completeness_2026} 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 of \emph{general} concurrent game frames. In this paper, assuming two agents, we prove that for actual powers, the eight classes of general concurrent game frames are representable by eight corresponding classes of neighborhood frames. Building on this result, we show that for alpha powers, the same eight classes of general concurrent game frames are likewise representable by eight corresponding classes of neighborhood frames. This generalizes a result in \cite{benthem_new_2019}. We also show that the two-agent actual characterization does not extend to arbitrary finite agent sets.