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.

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.

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.

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.

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.

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⁰₂ set is Sigma⁰₂).

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⁰₃ set is Sigma⁰₃. A second level Borel function f has a countable decomposition if there is a Pi⁰₂ 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.

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₂). IFML, as defined by us, will bear to IF₂ exactly the same relation as basic modal logic bears to FO₂, 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.

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⁰₂ (and beyond), but not for Sigma⁰₃ sets.