INTERACTIVE LOGIC:Games and Social Software 7th Augustus de Morgan Workshop King's College London November 4-7, 2005 |
Ludolf Bakhuizen,
XVIIth century |

We consider the following questions: What kind of logic has a natural semantics in multi-player (rather than 2-player) games? How can we express branching quantifiers, and other partial-information constructs, with a properly compositional syntax and semantics? We develop a logic in answer to these questions, with a formal semantics based on multiple concurrent strategies, formalized as closure operators on Kahn-Plotkin concrete domains. Partial information constraints are formalized as co-closure operators.

The rationalizability concept was introduced in (Bernheim 84) and (Pearson 84) to assess what can be inferred by rational players in a non-cooperative game in presence of common knowledge. However, this notion can be defined in a number ways that differ in seemingly unimportant minor details. We shed light on these differences, explain their impact, and clarify for which games these notions coincide. Also we apply the same analysis to clarify the differences and similarities between various ways iterated elimination of strictly dominanated strategies was defined in the literature.

My work in this area focuses on the formalization of multi-agent systems in modal logic with particular emphasis on concurrency, independence, collaboration, and coordination issues. In the talk I present a class of operators (quantificational modal operators [1]) that combine modality with quantification and that can capture all these aspects (to different degrees) without need for introducing other operators in the language. Differently from [1], this work focuses on semantics. The idea is that, varying the interpretation provided in [1], one can capture different types of agents in the very same language. I provide a first classification of the possible interpretations and show how to model a few scenarios. A major motivation for this work is the comparison of multi-agent systems. The variety of modal languages used today often hide the common aspects of the modeled systems. I believe one can overcome this problem by using new operators developed explicitly for MAS. The quantificational modalities I present are a first step in this direction since they provide a fixed framework where it is possible to compare (direcly) a relatively large class of multi-agent systems.

- [1] Quantificational modal logic with sequential Kripke semantics. Borgo, S. JANCL Vol.15 No.2/2005, pp. 137-188

I shall discuss recent work, by myself and others, on the application
of Independence-Friendly Logic, as developed by Hintikka and Sandu, to
modal and temporal logics. In particular, I will consider the notion
of independence-friendly modal *mu*-calculus.

(with Amanda Friedenberg)

Correlations arise naturally in non-cooperative games, e.g., in the equivalence between undominated and optimal strategies in games with more than two players. But the non-cooperative assumption is that players do not coordinate their strategy choices, so where do these correlations come from? In coin tossing, correlated assessments are usually understood as reflecting the observer's ignorance of a hidden variable, viz., the coin's parameter or bias. We take a similar view of correlation in games. The hidden variables are the players' characteristics that aren't already described in the matrix or tree, viz., their types (beliefs about the game, beliefs about other players' beliefs, etc.). A player may then consider other players' strategies to be correlated, if he considers their types to be correlated. We analyze this hidden-variable view of game-theoretic correlation.

Type space and canonical homeomorphism related to it are the fundamental tools of epistemic game theory. First introduced by Harsanyi (1967/68), later formally developed by Mertens and Zamir (1985), and Brandenburger and Dekel (1993). I propose alternative, but equivalent, construction of a type. Instead of the Kolmogorov Extension Theorem used by Brandenburger and Dekel (1993) I base my approach on the Ionescu-Tulcea Theorem. Instead of using probabilities defined on product spaces, I exploit the notion of transition probability. The second level of Ann's type consists of a belief over Bob's strategy space and a family of functions which assign probabilities to Bob's belief for a given strategy of his. Ann picks Bob's strategy and ponders which Bob's beliefs are likely to support this choice. This alternative approach not only provides new interpretation of a type but also allows us to make weaker topological assumptions - instead of Polish spaces we require only separability. I also show that if we restrict construction of Brandenburger and Dekel (1993) to disintegrable measures then the two approaches are equivalent.

We study two-player games of infinite duration that are played on finite or infinite game graphs. A winning strategy for such a game is called positional if it only depends on the current position in a play, and not on its history. A game is positionally determined, if from each position, one of the two players has a positional winning strategy.

The theory of such games is well studied for winning conditions that are defined by logical formulae or automata-theoretic conditions in terms of a mapping that assigns to each position a priority from a finite set C. Specifically, in Muller games the winner of a play is determined by the set of those priorities that have been seen infinitely often, and in parity games the least (or greatest) priority occurring infinitely often determines the winner. It it is well-known, that parity games are positionally determined whereas Muller games are determined via finite-memory strategies.

After an introduction into the theory of determinacy and positional determinacy of infinite games, we will extend this theory to the case of games with infinitely many priorities. Such games arise in several application areas, for instance in pushdown games with winning conditions depending on stack contents.

For parity games there are several generalisations to the case of infinitely many priorities. While max-parity games over omega or min-parity games over larger ordinals than omega require strategies with infinite memory, we can prove that parity games with priorities in omega are positionally determined. Indeed, it turns out that the parity condition over omega is the only infinitary Muller condition that guarantees positional determinacy on all game graphs.

The discrepancy between (min-)parity games and max-parity games has an intersting application to an old problem posed by Jonathan Swift.

A theorem in formal semantics states that
if a language *L* has a grammar determining its sentences and
their constituents, then any valuation *v* of the sentences of
*L*
(for example as true or false) induces an essentially unique
fully abstract and compositional valuation of the constituents,
which in turn determines *v*. This applies in particular when
the valuation *v* is given in terms of games. In some cases
involving games of imperfect information, the induced
valuation on constituents is known but not entirely intuitive.
The talk will aim to gain some intuition by applying the
semantic theorem to the games themselves, taking subgames as
constituents. The resulting notions make good sense even
when there is no language involved. If time allows, the talk
will also sketch a very different and more linguistic approach
to the relevant intuitions, using an idea of Väänänen.

(with Jeff Paris)

We characterize "rational choice" in the context of two agents who, in the absence of communication, intend to conform to each other's expected behaviour.

In the short talk I will try to deliver ideas mostly related to Hyland--Schalk abstract game semantics and newly introduced by Japaridze formalism of computability logic. The aim of the talk is to convince the audience that logic can be used not only as a tool for computing static truth values of formulae, but also for modelling interactive processes such as dynamic (parallel) computation of streams. I exploit the idea that it is possible to represent computation of streams within the abstract game semantics, and so this type of computation could be dealt with by means of the underlying fragments of linear logic. For the case of computability logic, I establish its coalgebraic semantics, and thus I show that computability logic also models streams.

(with Allard Tamminga)

We present a generalization of Horty's stit-based deontic logic, which enables us to give formal interpretation of what an agent ought to do in the interest of a certain group of agents. This allows us to study group phenomena in deontic settings. We can represent different deontic notions such as egoism (when the interest group consists of only the agent himself), altruism (when the agent is not a member of the interest group), nihilism (when the interest group is empty), and utilitarianism (when the interest group consists of all agents) in the same formal system. We can interpret the logic in game-theoretical settings and provide characterising axioms for strategic games (where the outcome is determined by the actions of the agents), constant sum games (where the sum of the payoffs of all agent is the same regardless of the actions), and provide a general characterization which tells us when the interests of different groups coincide. By applying the logic to the Prisoner's Dilemma we gain formal insight into the different common sense intuitions that people have about this well-known problem. In short, we present a multi-agent deontic logic.

Belnap, N., M. Perloff, and M. Xu (2001). Facing the Future, Agents and Choices in Our Indeterminist World. New York: Oxford University Press.

Horty, J. F. (2001). Agency and Deontic Logic. New York: Oxford University Press.

Osborne, M. and A. Rubinstein (1994). A Course in Game Theory. Cambridge, Massachusetts: MIT Press.

van Benthem, J. (1984). Correspondence theory. In D. Gabbay and F. Guenther (eds.), Handbook of Philosophical Logic, Volume II (pp. 167-247). Dordrecht: D. Reidel Publishing Company.

We propose in this talk DIAL, a framework for inter-agents dialogue, which formalize a collective decision-making process to compose divergent interests and perspectives. This framework bounds a dialectics system in which argumentative agents play and arbitrate to reach an agreement. For this purpose, we propose an argumentation-based reasoning to manage the conflicts between arguments having different strengths for different agents. Moreover, we propose a model of argumentative agents which justify the hypothesis to which they commit and take into account the commitments of their interlocutors according to their reputations. In the scope of our dialectics system, a third agent is responsible of the final decision outcome which is taken by resolving the conflict between two players according to their competences and the advanced arguments.

Social software begins by pointing out that there is a close analogy between computer software and social procedures. For example, just as registers in a computer are continually updated as a program is executed, the information of each agent changes as a social procedure is executed. We present a logic of knowledge and communication and discuss to what extent it can be used to reason about social procedures.

One fundamental insight behind social software is that ideas from Computer Science are useful in understanding social algorithms. The relevant fields of Computer Science are Logic of Programs and Analysis of Algorithms. Logic of Knowledge, which overlaps Philosophy, Computer Science and Economics is also very important.

A second fact is that detailed analysis is more useful than utility maximization - which carries the danger of turning into income maximization at the individual level, or GNP maximization at the national level. These can then become distractions from addressing actual needs.

A detailed analysis of what people want and what they need will become easier if we look at particular algorithms which people perform to fulfill particular needs, and how society can provide the infrastructure which enables people to carry out such algorithms. Supermarkets, hospitals, transportation networks, libraries, are all societal responses to PARTICULAR human needs and enable people to carry out algorithms which address these needs.

Game theory may give us some insights into WHY people want to do something (they want to maximize payoffs), but Computer Science addresses the issue of structure, i.e. an answer to the question of HOW.

After describing some foundational results and insights, we will briefly describe some recent developments at the City University of New York, namely Knowledge Based Obligation, Adjusted Winner (extending the work of Brams and Taylor) and perhaps some other work if time permits.

Backward induction is one of the oldest ideas in game theory. Whereas the algorithm is very simple, various examples in the literature have shown that choosing according to backward induction is not a simple consequence of (common belief in) rationality. The problem is the following: If a player observes that an opponent is not choosing according to backward induction, then it is not clear that this player should reason in accordance with backward induction in the game that lies ahead, and as such, it is not clear that this player should choose according to backward induction himself. In order to arrive at backward induction, one therefore needs to make explicit assumptions about how players revise their beliefs upon observing unexpected moves by opponents.

In this presentation, I will discuss the differences and similarities between various epistemic foundations for backward induction that have been proposed in the literature. Each of these foundations puts different restrictions on the players' belief revision procedures, but they eventually lead to the same strategy choices for all players, namely the backward induction choices. In order to better recognize the differences and similarities between the foundations, we incorporate all foundations into a unique epistemic base model.

There are two seemingly unrelated paradoxes in social choice theory. These are the Ostrogorski paradox and the doctrinal paradox. They arise when, in a group, each individual consistently makes a judgment (in the form of yes or no) over specific propositions, and the collective outcome is in some respect inconsistent. The result is inconsistent as regards the adopted voting rule in the Ostrogorski paradox, and it is logically inconsistent in the case of the doctrinal paradox. In this paper I will argue that, despite of the differences, these two problems share a similar structure. My conclusion will be twofold: on the one hand, the similarities among the paradoxes support the claim that these problems should be tackled using the same aggregation procedure; on the other hand, applying the same procedure to these paradoxes will help clarifying the strength and weakness of the aggregation method itself when applied to this kind of aggregation problems. In a previous work I have shown that the doctrinal paradox dissolves when we apply an operator defined in artificial intelligence to merge knowledge bases. In this paper I will apply the same merging operator to the Ostrogorski paradox and show that we can avoid this paradoxical result as well.

(with Edward Hermann Haeusler and Mario R. F. Benevides)

Games are abstract models of decision-making in which decision-makers(players) interact in a shared environment to accomplish their goals. Several models have been proposed to analyze a wide variety of applications in many disciplines such as mathematics, computer science and even political and social sciences among others.

In this talk we show how to use a logic based on first-order CTL, called Game Analysis Logic (GAL), in order to reason about games in which a model of GAL is a game and a formula of GAL is an analysis. In this way, we model and analyze some standard games and solution concepts of Game Theory. Precisely, we specify Strategic Games and Coalition Games as models of GAL as well as their standard solution concepts, Nash Equilibrium and Core, respectively, by means of GAL formulas. We may also take into account other variations of games and solution concepts using this approach. A model-checking algorithm for GAL is used to achieve automatic verification.

Game theory is mainly concerned with finding rational solutions in game
models. However, coming up with a good and manageable representation of
the game is also an important task for agents with limited capacities. How
much information is needed to make a "good enough" decision? To which
extend can an agent ignore details of a decision problem? Different
answers to these questions will result in different *deliberative
strategies*, a concept that as been proposed in action theory by
Michael
Bratman. In this talk, I will present a preliminary framework to formalize
this concept. I will try to characterize which transformations of
extensive games result in models that limited agent can manage, but upon
which they can still reach a rational solution.

In an interactive multi-agent system agents communicate and as a result their information changes. A particular case of such a system is the setting of a security protocol, where principals should reach authentication by message passing through an unsafe channel. I will show how the algebraic axiomatization of the logic of information flow, which is a previous joint work of mine with Baltag and Coecke, can be used to reason about authentication in such protocols. The reasoning is based on the encoding of suspicions of principals, as well as the dynamic, compositional and non-deterministic character of the algebra of actions, i.e., Quantales.

It is well known that the Wadge game characterizes the set of continuous functions, in the sense that a function is continuous if and only if there is a strategy for Player II in the Wadge game that induces it.

It was shown by Alessandro Andretta in 2003 that
the set of first level Borel functions is
characterized in the same way by the backtrack game.
(A function is first level Borel if the preimage of
every
**Sigma**^{0}_{2}
set is
**Sigma**^{0}_{2}).

We present the multitape game, which is a
generalization of the Wadge and backtrack games.
We show that the multitape game characterizes the
set of second level Borel functions that have
a countable decomposition. (A function is second
level Borel if the preimage of every
**Sigma**^{0}_{3} set is
**Sigma**^{0}_{3}.
A second level Borel
function *f* has a countable decomposition if there
is a
**Pi**^{0}_{2}
partition such that the restriction of *f* to the sets in the
partition is first level Borel.)

It is a recurrent observation in Combinatorial Game Theory (CGT) that one-player games ("puzzles") have NP-complete complexity. That is, deciding whether an instance of a puzzle is in fact solvable is NP-complete. Furthermore, the complexity of two-player games is typically PSPACE-hard. These observations strongly suggest that alternation of players increases complexity.

This raises the question what the computational influence is of other game properties. For instance, what about imperfect information? In my presentation, I will make a case study of Scotland Yard, Ravensburger's well-known multi-player board game. I treat Scotland Yard as a two-player graph game, in which Mr. X only reveals his whereabouts during designated rounds, whereas the positions of the cops are commonly known throughout the game.

Surprisingly enough, I observe that any Scotland Yard game can be turned into a game of perfect information in a computationally efficient manner. In line with the aforementioned observations in CGT we observe that Scotland Yard has PSPACE-complete complexity. Moreover, we observe that in a certain sense imperfect information makes the decision problem easier, rather than harder.

Time permitting, I will relate my findings to CGT's restriction on games of perfect information.

(with Merlijn Sevenster)

Generalizing basic modal logic by dissociating the relations of logical dependency and syntactic subordinatedness gives rise to so-called Independence-friendly (IF) modal logics. Bradfield [1,2] has worked in the framework of transition systems with concurrency, making use of concurrency in giving meaning to independence, whereas Tulenheimo [4,5] has formulated and studied an IF modal logic, evaluated on usual Kripke structures, in which independence is implemented solely by the requirement of uniformity imposed on Verifier's winning strategies in evaluation games. Formulating Independence-friendly modal logic calls for answers to many questions: (i) How to logically model independence? (ii) To which types of operators independence may pertain? (iii) Is the logic related to other logics (such as IF first-order logic and basic modal logic), and the tools used (e.g. game theory of imperfect information) in the expected way?

We propose a novel way of formulating IF modal logic (IFML). We take
stance to
three parameters which all potentially admit of variation: formulation of
basic
modal logic, translation of modal logic into first-order logic (FO), and
an
IF-ing procedure yielding from FO a version of IF first-order logic. We
introduce the 2-variable fragment of IF first-order logic
(IF_{2}). IFML, as
defined by us, will bear to IF_{2} exactly the same relation as
basic modal
logic
bears to FO_{2}, the 2-variable fragment of FO. We propose a novel
way of
formulating the semantics of IFML, which is "far more" compositional than
are
the usual game-theoretically defined semantics of various IF logics; yet
we
need not make use of the combinatorially monstrous framework of trump
semantics
developed by Hodges [3]. We conclude by mentioning some metatheoretical
results
concerning IFML.

- [1] Bradfield, J. (2000). "Independence: Logics and concurrency," LNCS 1862.
- [2] Bradfield, J. & S. Fröschle (2002). "Independence-friendly modal logic and true concurrency" in Nordic J. of Computing 9(2), 102-17.
- [3] Hodges, W. (1997). "Compositional semantics for a language of imperfect information," Logic J. of the IGPL 5(4), 539-63.
- [4] Hyttinen, T. & T. Tulenheimo (2005). "Decidability of IF modal logic of perfect recall" in Schmidt & al. (eds.): Advances in Modal Logic, vol. 5, King's College Publications, London, 111-31.
- [5] Tulenheimo, T. (2003). "On IF modal logic and its expressive power" in Balbiani & al. (eds.): Advances in Modal Logic, vol. 4, King's College Publications, London, 475-98.

It is well-known that if sentences involving partially ordered quantifiers, as in Independence Friendly Logic, are given the game-theoretical interpretation, all except the first order ones are non-determined in some structures. How far afield do we have to go to find those structures? We show that the most commonly occurring mathematical structures serve as examples of structures where commonly quoted sentences, such as those expressing infinity, non-well-foundedness, or completeness, are non-determined.

According to standard truth-conditional semantics, the meaning of almost any type of expression is thought
of as a function from one domain to another. As standardly construed, however, this resulting meaning space
is immense, and the vast majority of the possible meanings are typically not expressed by simple natural
language constructions. One task of semantic theory is to *describe* which meanings are typically
expressed in such simple terms (the search for `semantic universals'), and which are not. Another task is to
*explain* this division. In this talk I will use Signaling Games, as introduced by David Lewis (1969),
but now seen from an evolutionary point of view, to motivate some semantic universals, and to characterize
the circumstances under which expressions of a certain type will emerge.

(with Mark Roberts and Michael Wooldridge)

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 talk, we start off with briefly introducing Social Laws and then show how Alternating-time Temporal Logic (ATL) of Alur, Henzinger, and Kupferman provides an elegant and powerful framework within which to express and understand social laws for multiagent systems. Then, 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. Third, we show that the complexity of the feasibility problem in our framework is no more complex in the general case than that of the corresponding problem in the Shoham-Tennenholtz framework (it is NP-complete. We illustrate the concepts and techniques developed by means of a running example.

It time allows, we then give some hints about such a system for reasoning about social laws can be extended to reason about knowledge, and how one might constrain the agents' actions by explicitly allowing or forbidding specific strategies.

Model checking techniques for communication protocols usually are phrased in terms of processes, basically labelled arcs in a labelled transition system. We propose to lift checking for such protocols to a more abstract level by analysing the protocols as composite communicative actions, with a communicative actions viewed as a mapping on an appropriate class of epistemic models. As an example, we will give an epistemic analysis and check of Chaum's well-known dining cryptographers protocol, and compare this with the more traditional process analysis.

Belnap and Gupta have given a formal theory of circular
definitions using so-called "revision-theoretic semantics".
Whilst this theory produces predictes whose extensions are of high
complexity in second order number theory, we look at how Herzberger's
simplified theory of truth produces what Burgess called "Arithmetical
Quasi-Inductive (AQI) Definitions". This notion coincides with various
others in the literature of computer science and math. logic. We show
that
AQI Definitions produce strategies for infinite games of perfect
information with payoff sets in *Sigma*^{0}_{2} (and
beyond), but
not for *Sigma*^{0}_{3} sets.

We give an overview of a prototype implementation of a multi-agent deontic action language written in Haskell (a functional programming language). The program allows one to simulate the interactive behavior of two or more agents which execute actions that are deontically specified. Deontic logic is the logic of obligation, permission, and prohibition (Carmo and Jones (2001)); agents use deontic notions to guide behavior. Dynamic deontic logics (Khosla and Maibaum (1987) and Meyer (1988)) introduce deontic operators on (simple or complex) actions (Harel et. al. (2000)), where the basic idea is that the operators modify the postconditions of an action by introducing a violation or fulfillment flag into the the postconditions of the action. In the simplest example, where an agent is prohibited from executing an action, if the agent does execute the action, then the agent incurs a violation in the postcondition.

In the implementation, actions are functions from precondition states-of-affairs (SOAs) to postcondition states-of-affairs. Agents execute actions in a SOA. Deontic operators modify actions by introducing violation and fulfillment flags into the postconditions of actions; the operators can apply to simple or complex (e.g. sequence and choice) actions. A contract state is a list of deontically specified actions in a SOA. Actions are executed by agents with respect to a contract state. A history component of the SOA records the 'results' of the executions of actions. The postconditions of an action can also modify the contract state, allowing an account of 'Contrary-to-Duty Obligations'. Agents are able to 'choose' among the executable actions in a SOA against a criteria of desirable results; that is, if an agent is obligated with respect to one available action and prohibited with respect to another, the agent can 'choose' to execute the obligated action.

The implementation supports multi-agents and interaction. Given agents 'Bill' and 'Jill', the contract can specify that 'Bill' is obligated to execute action A and 'Jill' is prohibited from executing action A. There are two sorts of 'interaction' among the agents. First, we have relative execution: for example, 'Bill' may choose to execute action A, and so fulfill his obligation, only if 'Jill' has already violated the prohibition on action A. The other sort of interaction is relative to 'thematic' roles: we can express Hohfeldian Jural Relations of 'right' and 'privilege', among others, where we specify the agents with respect to the benefactor or malefactor. The implementation can also express notions of power and roles in an organization. The program provides a way to simulate interactive agentive behavior with respect to laws.