Social Laws in Alternating Time

Abstract

Since it was first proposed by Moses, Shoham, and Tennenholtz, the social laws paradigm has proved to be one of the most compelling approaches to the offline coordination of multiagent systems. In this paper, we make three key contributions to the theory and practice of social laws in multiagent systems. First, we show that the Alternating-time Temporal Logic of Alur, Henzinger, and Kupferman provides an elegant and powerful framework within which to express and understand social laws for multiagent systems. Second, we show that the effectiveness, feasibility, and synthesis problems for social laws may naturally be framed as atl model checking problems, and that as a consequence, existing atl model checkers may be applied to these problems. We illustrate the concepts and techniques developed by means of a running example.

(joint with with Wiebe van der Hoek and Mark Roberts)