Aring; gotnes

AAMAS Conference 2012 Conference Paper

Epistemic Coalition Logic: Completeness and Complexity

• Thomas
• Aring; gotnes
• Natasha Alechina

Coalition logic is currently one of the most popular logics for multi-agent systems. While logics combining coalitional and epistemic operators have received considerable attention, completeness results for epistemic extensions of coalition logic have so far been missing. In this paper we provide several such results and proofs. We prove completeness for epistemic coalition logic with common knowledge, with distributed knowledge, and with both common and distributed knowledge, respectively. Furthermore, we completely characterise the complexity of the satisfiability problem for each of the three logics.

AAMAS Conference 2011 Conference Paper

Scientia Potentia Est

• Thomas
• Aring; gotnes
• Wiebe van der Hoek
• Michael Wooldridge

In epistemic logic, Kripke structures are used to model the distribution of information in a multi-agent system. In this paper, we present an approach to quantifying how much information each particular agent in a system has, or how important the agent is, with respect to some fact represented as a goal formula. It is typically the case that the goal formula is distributed knowledge in the system, but that no individual agent alone knows it. It might be that several different groups of agents can get to know the goal formula together by combining their individual knowledge. By using power indices developed in voting theory, such as the Banzhaf index, we get a measure of how important an agent is in such groups. We analyse the properties of this notion of information-based power in detail, and characterise the corresponding class of voting games. Although we mainly focus on distributed knowledge, we also look at variants of this analysis using other notions of group knowledge. An advantage of our framework is that power indices and other power properties can be expressed in standard epistemic logic. This allows, e. g. , standard model checkers to be used to quantitatively analyse the distribution of information in a given Kripke structure.

AAMAS Conference 2010 Conference Paper

Optimal Social Laws

• Thomas
• Aring; gotnes
• Michael Wooldridge

Social laws have proved to be a powerful and theoretically elegantframework for coordination in multi-agent systems. Most existingmodels of social laws assume that a designer is attempting to produce a set of constraints on agent behaviour which will ensure thatsome single overall desirable objective is achieved. However, thisrepresents a gross simplification of the typical situation, where adesigner may have multiple (possibly conflicting) objectives, withdifferent priorities. Moreover, social laws, as well as bringing benefits, also have implementation costs: imposing a social law oftencannot be done at zero cost. We present a model of social lawsthat reflects this reality: it takes into account both the fact that thedesigner of a social law may have multiple differently valued objectives, and that the implementation of a social law is not cost-neutral. In this setting, designing a social law becomes an optimisation problem, in which a designer must take into account boththe benefits and costs of a social law. We investigate the issue ofrepresenting a designer's objectives, characterise the complexity ofthe optimal social law design problem, and consider possible constraints that lead to reductions in computational complexity. Wethen show how the problem of designing an optimal social law canbe formulated as an integer linear program.

IJCAI Conference 2007 Conference Paper

• Thomas
• Aring; gotnes
• Wiebe van der Hoek
• Michael Wooldridge

We add a limited but useful form of quantification to Coalition Logic, a popular formalism for reasoning about cooperation in game-like multi-agent systems. The basic constructs of Quantified Coalition Logic (QCL) allow us to express properties as "there exists a coalition C satisfying property P such that C can achieve Phi". We give an axiomatization of QCL, and show that while it is no more expressive than Coalition Logic, it is exponentially more succinct. The time complexity of QCL model checking for symbolic and explicit state representations is shown to be no worse than that of Coalition Logic. We illustrate the formalism by showing how to succinctly specify such social choice mechanisms as majority voting, which in Coalition Logic require specifications that are exponentially long in the number of agents.

IJCAI Conference 2007 Conference Paper

• Thomas
• Aring; gotnes
• Wiebe van der Hoek
• Juan A. Rodr
• iacute; guez-Aguilar
• Carles Sierra
• Michael Wooldridge

We introduce Normative Temporal Logic (NTL), a logic for reasoning about normative systems. NTL is a generalisation of the well-known branching-time temporal logic CTL, in which the path quantifiers A ("on all paths. .. ") and E ("on some path") are replaced by the indexed deontic operators O n and P n, where for example "O n Phi" means "Phi is obligatory in the context of normative system n". After defining the logic, we give a sound and complete axiomatisation, and discuss the logic's relationship to standard deontic logics. We present a symbolic representation language for models and normative systems, and identify four different model checking problems, corresponding to whether or not a model is represented symbolically or explicitly, and whether or not we are given an interpretation for the normative systems named in formulae to be checked. We show that the complexity of model checking varies from P-complete up to ExpTime-hard for these variations.