Verifying Coalitions in 3-Party Systems

Multiplayer games are played by a set of agents, where, at each round, all players give their moves, and the combination of their moves defines the successor states for the game. In such games, the players pursue certain goals with their moves and in that pursuit, they can form coalitions to fulfill a common objective. In this paper, we adopt this model of multiplayer coalition games in the context of 3-party systems, consisting of a module, its environment, and a controller. The winning objective of our game is given as a specification in linear temporal logic and the module and controller together attempt to satisfy the specification for all possible strategies of the environment. In this paper, we analyze the problem for various degrees of observability of the module-controller pair, and provide quantified Boolean formula-based methods for investigating the existence of a winning coalition strategy. The coalition strategy can only be fulfilled on carefully implementing both the module and the controller such that they can cooperate. We also consider the problem where the implementations of the module and the controller are available and we present a dynamic simulation-based approach for verifying whether these implementations conform to the coalition requirements. In case, they do not, we provide algorithms for designing the winning strategy for an intelligent environment to drive the coalition to a refutation.