Epistemic programs are programs for jointly updating all the agents' states of knowledge (or "belief") in a distributed system. They can be intuitively understood as computing the effect of exchanges of information ("communication") between agents. Such programs are recursively built from basic epistemic actions (e.g. public broadcasting, or various more "opaque" forms of communication), using standard program constructors. I introduce a (complete and decidable) Hoare logic for epistemic programs, which can be used to reason about informational changes, and in particular to prove the partial correctness of communication strategies with respect to given epistemic goals (and given epistemic preconditions). I apply this to some well-known epistemic games and puzzles. Finally, I present an extension of the Hoare logic to a much more expressive dynamic logic of epistemic programs, which turns out to be undecidable, although still useful in some contexts.

The claim that IF logic is the classical logic is grounded in the idea that, once one has adopted a game semantics, this liberalisation is very natural, corresponding to the shift from perfect to imperfect information games. But one could as well use Henkin quantifiers to give a recursive semantic for independence, so that the question cannot be settled on the level of pure expressivity, and arguments are likely to boil down to the fact that IF approach is more natural, elegant, or intuitive. We would like to give some precise content to this feeling. Namely, we will discuss three points : the claim of generality, the idea that IF gives a true analysis of independence, the links between truth-seeking and truth-establishing games. We will make thus some technical points about the use of slash, links with modal logic, and connections with classical proof theory.

This talk is about epistemic effects of actions such as public announcements (e.g., X shows his cards to everybody), private communication (e.g., X shows his cards to Y without Z noticing anything), semi-private communication (e.g., X shows his cards to Y in Z's presence; Z cannot see which cards are shown). Baltag, Moss and Solecki have proposed a convincing framework for reasoning about such "epistemic actions".

We will discuss a natural deduction calculus for reasoning about epistemic actions, based on hybrid logic. Hybrid logic is an extension of modal logic with nominals. These are special proposition letters that are true at exactly one world. Hybrid logic offers various advantages over orthodox modal logic, including nice proof systems.

Extended abstract

It is an old problem of Henkin, Monk, and Tarski to find a `simple intrinsic characterisation' of the `representable' algebras of relations.

Games have been found useful in constructing representations of relation algebras The ideas go back to Lyndon's work in the 1950s, but the presentation can arguably be made more transparent by using games. First-order axioms characterising representability can be extracted from the process; but I claim that the games themselves form a simple, intrinsic characterisation of representability. This claim is strengthened by the fact that one may go on to use games to analyse relation algebras in some detail, and prove many hierarchy results.

An extension of the WHILE-language is developed for programming game-theoretic mechanisms involving multiple agents. Examples of such mechanisms include auctions, voting procedures, and negotiation protocols. A structured operational semantics is provided in terms of extensive games of almost perfect information. Hoare-style partial correctness assertions are proposed to reason about the correctness of these mechanisms, where correctness is interpreted as the existence of a subgame perfect equilibrium. Using an extensional approach to pre- and postconditions, we show that an extension of Hoare's original calculus is sound and complete for reasoning about subgame perfect equilibria in game-theoretic mechanisms.

Thanks to Hintikka's slash notation, informational independence can be imported into various logics and especially into dynamic languages. A natural interpretation of the resulting IF dynamic logics is then provided by usual evaluation games. We will consider two IF extensions of dynamic logics:

1. Van Benthem's Epistemic Action Logic;
2. Groenendijk and Stokhof's Dynamic Predicate Logic.

The aims of my talk are:

1. to define a language IFML[k] for IF modal logic interpreted in terms of k accessibility relations;
2. to provide a game-theoretical interpretation to it, where the independence-indicator essentially becomes a device for forming 'information sets' on which the relevant player's winning strategies need be uniform;
3. to compare the expressive power of IFML[k] with that of the corresponding basic modallogic ML[k].

Results are obtained already with one accessibility relation, k := 1. We show that for arbitrary unary modal structures, IFML is strictly more expressive than ML. On the other hand, over unary modal structures with arbitrary linear frames, the expressive powers of IFML and ML indeed coincide. The same holds even for the corresponding temporal logics (with operators capable of speaking both of the accessibility relation and its converse), provided that there be operators available in the respective languages that can speak of immediate successors and immediate predecessors.

When a question arises as to the translatability of IF modal logic to first-order logic, the answer is that not only can the language IFML[k] considered here be translated to IF first-order logic, but in fact it can be translated to its traditional, perfect-information fragment, i.e. to FO.