Preferences in game logics

We introduce a Game Logic with Preferences (GLP), which makes it possible to reason about how information or assumptions about the preferences of other players can be used by agents in order to realize their own preferences. GLP can be applied to the analysis of social protocols such as voting or fair division problems; we illustrate this use of GLP with a number of worked examples. We then prove that the model checking problem for GLP is tractable, and describe an implemented model checker for the logic - by using the model checker, it is possible to automate the analysis and verification of social protocols.