Game Semantics has over the past decade become a highly developed approach to the semantics of programming languages, type theories and logics. The emphasis is on structural aspects of the semantics, which involves games in extensive form, and which allows many subtle logical and computational features to be captured in a very precise fashion, leading to full abstraction and full completeness results. Recently, algorithmic forms of these semantics have been developed which provide a basis for software model-checking. For the most part, Game-semantical analyses involve finite plays over infinite game trees. Infinite plays arise naturally in the semantics of untyped calculi. For various typed calculi, the fact that certain infinite plays cannot arise becomes a semantic means of expressing and proving Normalization (the fact that well-typed programs terminate).
We investigate path-forming games of infinite duration among several players with objectives given as omega-regular languages. Two-player purely competitive variants of such games are well studied within the computer science community, their algorithmic foundations being established mainly by the theory of alternating automata.
In a multi-player setting, however, cooperative aspects play a crucial role. Towards capturing these aspects, we study the structure of strategy sets under mild rationality assumptions (parasitising and dominance) and propose strategy synthesis procedures for restricted classes of games.
An aggregated form game is an alternative, coarser description of a game where players' preferences are specified in a statistical way. In this article I characterize equilibria of aggregated form games in terms of compositions. A composition describes aggregated behavior and tells us how many players of which type play what. Kalai (2002a,b) has shown that equilibria of extensive form incomplete information games are approximately extensively robust and ex-post Nash and therefore are Nash-equilibria of the corresponding normal form game if the game is large and players' preferences are semi-anonymous. Therefore, the present characterization result is the more relevant since it applies to the latter more complicated but more general and realistic class of large games. The nature of the result is illustrated by a non-existence example of a migration equilibrium.
Hintikka's independence-friendly (IF) logic is a formulation of branching quantifiers, so that a quantification may be declared to be made without knowledge of the values of previous quantified variables. In this talk, I will give an overview of some work in the last couple of years, some with Kreutzer, about the application of this idea to modal and temporal logics, and in particular the combination of IF logic with fixpoint logic, when the associated (infinite) semantic game becomes a parity game of imperfect information.
The theory of strong dominance in games is well understood, but that of admissibility (weak dominance) much less so. Yet admissibility gives much sharper predictions in many games of applied interest. This paper gives epistemic foundations for admissibility concepts.
Specifically, we develop an epistemic structure for games, in which rational players choose admissible (not weakly dominated) strategies. With this definition of rationality, we formulate the condition of rationality and mth-order assumption of rationality (RmAR). Rationality and common assumption of rationality (RCAR) then means RmAR for all m.
Note that even if a game is finite (i.e., has finite strategy sets), an associated epistemic structure may be infinite. In particular, a complete structure, which is one that contains all possible types that are implied by the structure, is necessarily infinite. In this sense, even a finite game, when described epistemically, may well be an infinite structure.
We prove three results on admissibility in games:
The impossibility result appears to indicate a limit on players' ability to reason about all possibilities in a game. Admissibility asks a player to take all states into consideration. RCAR asks players to assume "RmAR for the other players" for all m. Completeness asks players to consider all types. Evidently, not all of this is possible.
This work is located at the intersection of automata theory in computer science, semigroup and omega-semigroup theory in algebra, and game theory in descriptive set theory. There is a bridge between automata theory in computer science and semigroup theory in algebra. In fact, in case of finite words, there is a correspondance between automaton and finite semigroup. This property can be generalized to infinite words where Büchi automaton corresponds to a Wilke algebra, which is actually equivalent to a finite omega-semigroup. We focus on omega-semigroups and define a reduction relation on subsets of these omega-semigroups by the help of an infinite two players game. We show that using Borel determinacy and a conveniant topology on omega-semigroups, the "SG-hierarchy" defined by this game yields interesting results. In particular, Wadge hierarchy and Wagner hierarchy become special cases of this hierarchy. We also show that important algebraic and set theoretical notions can then be expressed in a very natural game theoretical way.
Game Theoretical Semantics (GTS) for first order predicate logic can be regarded as "an explication" in game terms, "of our own pre-theoretical ideas about quantifiers and truth" (Hintikka, BSL 8(3) 2002).
Semantical games for first order logic are finite two-player games, and like the majority of games that are used for the semantics of logical calculi, they are of perfect information. But Hintikka's extension of first order logic named IF-logic, gives rise to semantical games of imperfect information. This gives results in a larger expressive power and some surprising properties.
We will give a general introduction to Game Theoretical Semantics and IF-logic, and explore some infinitary aspects and generalizations.
We extend results of Fraenkel for determining the value of the combinatorial game on a graph to the asymmetric case, in which the infinite walk is a win for one of the players. We find a labelling procedure on the (finite) graph to achieve this, and show that it is finitary. We then give an algorithm to compute this labelling in time linear in the number of edges.
The topological complexity of sets of reals recognized by finite automata was studied in 1979 by Wagner. The resulting Wagner hierarchy turned out to be precisely the Wadge hierarchy restricted to sets of infinite words accepted by deterministic finite automata (DA) with Muller acceptance conditions (acceptance or rejection depends on the set of control states that are visisted infinitely often during the run of the machine).
Naturally, the Wadge game theoretical point of view induces a way of defining very simple set theoretical operations to construct the whole hierarchy with, on the basis of the empty set. And only a slight improvement of this hierarchy is needed to describe the one defined by PushDown Automata instead of automata. But this is no more true when one goes from the deterministic world to the non deterministic one. A huge gap separates the hierarchy induced by sets of infinite words accepted by non deterministic finite automata and the one related to non deterministic finite PushDown automata. In particular, the former is located inside the Boolean closure of Sigma02 sets, while the latter, as shown by O. Finkel, climbs along all Borel levels of finite ranks, also up to Sigma0omega, and even beyond all Borel levels.
As a nice and easy example of how a thorough functorial approach of the Wadge hierarchy leads to intriguing results about sets of reals defined by simple machines, we concentrate on a notion of sets of infinite words slightly weaker than the one of sets accepted by non deterministic PushDown automata: the omega power of finite context-free language. That is a set of reals of the form Vomega, where V is a set of finite words accepted by a non deterministic PushDown automaton. Using a "Backspace" operation that arises very naturally when studying the Wadge hierarchy of Borel sets, we construct such a set and show that it is both Borel and stricly above Delta0omega.
Dialogue games, as developped in the 1960s by K. Lorenz and P. Lorenzen, provide a semantics for a great variety of logical systems. For first order predicate logic, e.g., a dialogue semantics can be specified, which is equivalent to classical (model-theoretical) semantics. In contrast to the latter the dialogue semantics is "anti-realist", since it does not presuppose that every (especially logically prime) proposition is true or false, but only that it is justifiable or not justifiable. In the dialogue game played by a proponent and an opponent, the question whether a logically complex proposition asserted by the proponent is justifiable or not can be reduced stepwise to the question, whether certain logically prime propositions contained in the complex one are justifiable or not. On the basis of this reduction a procedure can be specified, which analyses for an arbitrary given formula of first order predicate logic all possible constellations concerning the question whether the contained prime propositions can be justified or not and whether in all these constellations the dialogue game can be won by the proponent. Thus the procedure yields a decision whether the given formula is logically valid or not. In the talk this procedure will be presented and the obvious question will be discussed, how this kind of decision is to be assessed with regard to the decision problem in general and its well-known negative solution for first order predicate logic by A. Church.
The procedures of Searching of solutions for problems, in A I, can be carry out, in many ocassions, with knowledge of the Domain, and in another situations, without knowledge of the same. This last procedure is usually named Heuristic Search. In such methods the matricial technics reveals essential, also in all related with Infinite Games. Their intoduction can give us an easy and effective way in the search of solution. Our paper explain how the matrix theory appear in A I, and therefore, on Infinite Games.
Forcing is a method to extend models of Set Theory in order to get independence or at least consistency results. (Originally it was invented by Paul Cohen in the early 1960's to prove the independence of the Continuum Hypothesis from the axioms of Set Theory.) For some forcing notions it is shown how infinite games, and in particular winning strategies, can be used to predict combinatorial properties of the extended model.
Determinacy axioms state the existence of winning strategies for infinite two player games played on the natural numbers.
We show that a base theory enriched by a certain scheme of determinacy axioms is proof-theoretically equivalent to Pi12-comprehension.
A classical problem in algebraic logic is to axiomatise classes of representable algebras. Taking the example of the representable Tarskian relation algebras, I will discuss how games can help with axiomatisation problems, and how they throw light on representability itself.
I plan to survey recent progress in the study of several types of evolutionary dynamics (replicator dynamics, best response dynamics, Brown-von Neumann-Nash dynamics) for infinite games, in particular games with a continuous strategy set.
When several, alternative theories fit the data, Ockham's razor enjoins us to choose the simplest. But how could such a policy possibly help us find the truth? For Ockham's razor is a fixed bias toward simplicity, and a fixed bias of any kind can no more indicate truth than a broken thermometer stuck on a particular reading can indicate temperature. Standard responses either beg the question by assuming that the world is probably simple or change the subject by substituting some feature of simple theories for truth.
I resolve this traditional puzzle by modelling scientific problems as infinite truth-finding games in which the scientist wins if she eventually converges to the right answer to a given, empirical question. Convergence to the truth allows for arbitrarily many "scientific revolutions" or retractions of earlier opinons prior to convergence to the right answer. I argue that, in a well-defined sense, Ockham's razor is the unique scientific strategy that minimizes retractions en route to the truth. Thus, Ockham's razor helps us find the truth in a strong and unique sense, but it doesn't indicate the truth since arbitrarily severe retractions may still await a retraction-minimizing scientist in the future. The argument involves a general (topological) definition of theoretical simplicity that I will state and motivate. Time permitting, I will sketch how these ideas apply to curve fitting, Goodman's "new riddle of induction", statistical testing, causal inference, and statistical model selection.
The talk is self-contained and is aimed at a general philosophical and scientific audience. Animated diagrams illustrate the novel concepts involved.
Let A be an algebra, not necessary finite, consider the set FA of all finite subalgebras of A which is a partially ordered set with an order A1 < A2 if A2 is a subalgebra of A1 This allows to consider games on A, and similarly cores of the games or, equivalently, finitely-additive measures, as elements of projective limits. On this way we obtain decomposition theorems for cores of the form of commuting diagrams of some canonical isomorphisms (analogues of Möbius inversion).
Here is an example of an easy choice. When you visit a restaurant, would you prefer to have an entree selected from the menu by a lottery, or would you prefer to choose your dinner for yourself? While most individuals would have no hesitation identifying the opportunity to choose for oneself as preferable, most theories of rational decision are incapable of even posing the question.
In this paper I will explain how, within one influential system of analyzing decisions under uncertainty, we may represent decision problems themselves as events which stand in relations of relative preference to other events. Given a preference relation among events, a choice function can be constructed for a domain including decision problems. Infinite decision problems create a novel feature. While the extended choice function does support revealed preference, the resulting preference order is no longer isomorphic to the real numbers, when decisions among infinitely many options are included in the domain. An open question is whether revealed preference is unique given an arbitrary choice function over a domain containing infinite decisions.
In a concluding section, choice function representations of decision problems are compared to matrix representations. Translation between the formalisms is shown to be constructively definable, but not trivial.
In this talk we present the relationship between the mu-calculus, automata and games. The model checking and the satisfiability problem of the mu-calculus can be translated into problems for alternating tree automata. In this context parity games play an important role. They are played to find out which transition systems are accepted or rejected by a given alternating tree automaton.
We survey some of the results on stability of Nash equilibrium and of equilibrium selection in dynamic evolutionary models with and without mutations/trembles. We first consider the issue of stability of Nash equilibrium and then explore how the introduction of a small amount of mutation, in terms of players making mistakes or experimenting, helps the underlying system to converge to recurrent classes that are stochastically stable. By drawing on some of our recent work, we show how the standard results in these areas are affected when each player's type space is sufficiently rich - that is, when players are identified by (learning) rules that choose actions conditional on past histories.
The Wagner hierarchy of regular omega-languages has perfect properties with respect to Wadge reducibility and its effective versions. We try to develop a similar theory for regular star-free (RSF) omega-languages. We show that Wadge degrees of RSF omega-languages are the same as those of regular omega-languages. A (hopefully) suitable effectivization of the Wadge reducibility for RSF omega-languages is proposed. The relationship to the Brzozowski hierarchy of RSF omega-languages is described.
Some of the earliest examples of infinite games appear in topology. In this talk we will give a brief survey of selected topological games that have played an important role in characterizing various topological properties.
Many authors have pointed out serious shortcomings in the formalism of contemporary economic theory. In this brief paper we introduce a methodology to overcome some of them. We will begin by showing that the computability of choice functions as well as the existence of economic equilibria and of states of the world may not be ensured in general if the assumed set theory is ZFC. We claim that a switch to an alternative set theory may help to get rid of some of these negative results. While this procedure seems a facile form to solve analytical problems, we think that it may have a legitimate importance for economic theory. In fact, alternative set-theoretical frameworks convey different intuitions about how agents behave when solving problems. One of these intuitions is that agents are able to play an infinite game of internal deliberation, for which they always have a winning strategy. An appropriate axiomatization of this idea is by means the Axiom of Determinacy (AD). Since this axiom is incompatible with other set-theoretic postulates (in particular the Axiom of Choice) we need to give an entire axiomatic structure for our reformed economic theory. We postulate that AFA- + AD + DC is the adequate set-theoretical universe for economic theory, where AFA- is ZF without AC and Regularity replaced by Barwise's Anti-Foundation Axiom, while DC is the axiom of Dependent Choices.
Motivated by a question of Iliadis, we extend Scheepers' prototypes of topological diagonalizations to the case that the types of covers in the sequence to be diagonalized can vary. The most well known example of such a property which cannot be expressed by Scheeper's prototypes is the Galvin-Miller strong gamma-property. Whereas this property is strictly stronger than the the Gerlits-Nagy gamma property, the corresponding strong notions for the Menger, Hurewicz, Rothberger, Gerlits-Nagy (*), Arkhangel'skii and Sakai properties are equivalent to the original ones.
We give new game theoretic characterizations for most of these properties, and answer Iliadis' Question.
We define a new Ehrenfeucht-Fraïsse game. The new feature of this ordinal-ranked infinitary game is that the second player is allowed to give partial answers as long as she completes them later. Since the game ends after a finite number of moves, she may not have to complete all partial moves. This game gives rise to a new infinitary language with the Craig Interpolation Theorem and a Lindström-type model theoretic characterization.
This paper contributes a "structural" perspective on game forms by studying concept lattices of general coalitional game forms (CGFs). Some basic properties of concept lattices of CGFs and of the desirability relations they induce on the latter through a natural rank function are considered. The use of the concept-latticial size, length and width as basic complexity measures of the underlying game correspondence is also presented by means of several examples. In that connection, "structurally" infinite game forms are introduced. A direct extension of the concept lattice construct to extensive and strategic game forms when viewed as Chu spaces is also outlined.
There is a long and respectable tradition in theoretical computer science linking automata theory and logic. Two key results in this area are Rabin's decidability theorem of the monadic second order logic of n-ary trees, and the expressive completeness result by Janin and Walukiewizc stating that the modal mu-calculus corresponds to the bisimulation invariant fragment of second order logic.
Infinite games form the backbone of the connection between automata and logic. The standard situation is that the acceptance games associated with a certain kind of automaton, is of the same kind as the evaluation game associated with a formula of the corresponding logic. Quite often the games involved are infinite two-player graph game with a winning condition on infinite matches that is expressed via a parity function. Properties of such games are crucially involved in the proofs of the pivotal results in the area. As an example, the History Free Determinacy of infinite parity graph games, plays a key role in the proof of the Complementation Lemma for various classes of automata.
In the talk we argue that it is worthwhile to study the connections between fixed point logics and automata from the perspective of coalgebra. We will outline how the triangle logic-automata-games can be parametrized by a set functor. In particular, for any standard set functor F we define the notion of an F-automaton, a device operating on pointed F-coalgebras. This enables, for instance, a uniform treatment of automata operating on infinite words, trees, or graphs, but also allows generalizations to other structures. We discuss the criterion under which such an automaton accepts or rejects a pointed coalgebra, which is formulated in terms of an infinite two-player graph game.
Time permitting we also introduce a language of coalgebraic fixed point logic for F-coalgebras, and discuss the mutual transformations between F-automata and formulas of this language. A number of applications of this connection will be discussed, for instance on uniform interpolation.
Herzberger (Toronto) has established an approach to adding a truth predicate to a language that has been called "revision-theoretic" by Gupta and Belnap (Pittsburg). The latter have generalised on this idea to form a theory of "quasi-inductive definitions".
The Herzbergerian part of this theory has been defined and used independently by Kreutzer (Aachen) in order to separate out Partial from Inflationary Fixed Point logics on infinite structures.
We show how such quasi-inductive definitions can be performed if we assume Determinacy for Gale-Stewart infinite games of perfect information with Sigma03 payoff sets.
sigma-ideals defined in the Cantor space (or in the Baire space) associated to certain games between two players have been investigated by many authors (here I limit myself to mentioning only some: Mycielski, Roslanowski, Bartoszynski and Scheepers).
My contribution deals with the so-called (alpha,beta)-games, defined in the real line, introduced by the number-theorist Wolfgang Schmidt in 1966. Precisely, my aim is that of presenting the descriptive set-theoretical properties of the sigma-ideal consisting of the "absolutely losing" (in Schmidt's sense) subsets of R. In particular, my intention is to stress the analogies (and the differences, as well) between such an ideal and the classical ones taken from Real Analysis.
For instance, Schmidt's ideal turns out to be orthogonal to the sigma-ideal made up of the sets being both meager and null in the sense of Lebesgue. Moreover, Schmidt's ideal (better: a suitable slight variant of it) turns out to be Borel-generated.
Some consequences of the two facts above are then discussed, among which the existence of very pathological sets a la Mahlo-Luzin-Sierpinski, i.e., constructed by combining transfinite recursions and the assumption of CH.
Finally, I add some related open problems: they all appear to rely on infinitary combinatorics.