Logic, Games & Computation:
'the story behind the scenery'

Lecturer: Johan van Benthem & guest speakers
Autumn 2006, Master of Logic Seminar, Amsterdam

Sunday26 November: FINAL SCHEDULE

Homework  The deadline for all homeworks is Monday December 4 -- 'this is it', and on that date, you can give me all assignments that you have not handed in yet. The last homework is that on epistemic temporal logic by Eric Pacuit (Week 11, see below).

Workshops  These are working sessions where new topics and open problems are presented which you can use for a final paper. You can work together with other students on a topic if you want to. This replaces the original paper assignment for your final requirement. However, if you have an individual paper topic already, then it would also be fine to do that, and skip the workshop. The deadline for both variants is Friday December 15.

23 November, Workshop 1:

We discussed two topics in some technical detail:

(a) Frame correspondence arguments for DEL axioms. The first task would be to define a suitable general setting that makes the best sense of the frame correspondence arguments in my paper 'Dynamic Logic of Belief Revision'. This requires some formal setting up of families of epistemic (plausibility) frames and transitions between them, plus maybe abstract functions or relations between world across frames. Then you could sharpen up some correspondence arguments. E.g., we found during our session that, to fully capture eliminative update, we needed the reduction axiom for knowledge, but also one for an existential modality, plus a basic equivalence <!P>T iff P. A further desideratum: analyze the reduction axioms for knowledge in full DEL, and find a correspondence proof showing to which extent this forces us to adopt product update. Finally, all this led to a more general mathematical question: what happens to existing modal correspondence theory when we consider modal languages with dynamic modalities referring to changing models? For instance, the axioms that we analyzed all have a simple 'Sahlqvist form', but what is the proper generalization?

(b) Topological models for DEL. We discussed the basics of topological semantics for modal and epistemic languages, whose details (including bisimulation, and all that) you can find explained in several papers on my homepage under Research. Topological models add new, non-graph-based structures that can represent information, and hence they can also model information flow in new ways. Concrete question: Generalize product update MxE over topological static models M and topological event models E. You need to generalize the formulation of the basic reduction axiom for knowledge. The generalization should reduce to standard product update on relational models (which correspond to special 'Alexandroff topologies'), and it should validate the generalized reduction axiom. My prediction is that you will need something close to standard 'topological product spaces', the ones you find in basic results in topology like Tychonoff's Theorem.

There are further topics along these lines.

E.g., the representation theorem for DEL models inside branching temporal universes presented in class by Eric Pacuit also has a 'correspondence' flavour, describing what conditions on temporal universes are enforced by what DEL axioms. One obvious question is how this result and its proof can be extended to a temporal logic representation theorem for epistemic plausibility models allowing for both epistemic update and belief revision. You would need to think about translations from DEL and its belief versions into ETL and its belief versions. Moreover, conceptually, you will encounter the fact that 'belief' in a temporal setting has two distinct aspects: beliefs about the world based on observation of events so far, and belief based on prior expectations about what still has to happen in the future. These may require different formal modeling.

29 November, Workshop 2
Wednesday 11:15 - 13 hours, usual place Diamantslijperij)

The second workshop will be led by our Ph.D. students who presented in class in October and November, and they will provide materials on topics and open problems in research right now.

Theme: "From Constraints to Preferences and Back: the General Picture"

We are going to study the connections between constraint- based preferences, as presented earlier by Fenrong Liu, and "possible world"-based preferences, as presented by Olivier Roy and Patrick Girard.
A very suggestive parallel can be drawn between the two approaches. The essence of what Fenrong presented is to propose various ways (there's 3 in the paper) to construct a preference relation over objects (i.e. c > c') from the a defined binary relation between predicates, that she calls constraints. It's a "top-down" procedure. For example, given two constraints C and C' such that C >> C' : c > c' iff |= C(c) or ((C (c) iff C(c')) and C'(c). The "possible-world"-based preferences approach goes the other way around. There, various procedures (the number depends on the properties of >) are proposed
to construct a preference relation between predicate (or formulas) from the defined binary relation between objects/worlds. It's a "bottom-up" procedure. One example: P Pref P' iff forall x,y if P(x) and P'(y) then x > y. Mathematically, the two approaches appear to be highly comparable. Just look at formulas P, P' and constraint C, C' abstractly, as predicates, and at world as objects. In this workshop, we are going to investigate aspects of this connection, through the following questions:

Is one of the top-down procedures "transformation-equivalent" to one of the bottom-ups? By "transformation equivalence" we will mean: take an ordering on predicate >>, transfer it to an ordering between worlds > using a given top-down procedure, then can we find a bottom-up procedure in preference logic that would lift back > to a new >>' such that C >> C' iff C >>' C'? The same question aries mutatis mutandis from a defined > back to >'.

Two of the top-down procedures presented in Fenrong's lecture involved beliefs of the agents. How can we translate these requirements in preference logic?

If time permits, we will also look at the connection between the completeness results obtained in Fenrong's work, and the ones for preference logic.

========================================

Aim of the Seminar

This seminar is about dynamic logics that describe events where information flows. Our special focus will be games, which form a natural interface with modern logic, which is broadening year by year. You will learn about some current topics, basic techniques, and ongoing research. About half of our presentations will be by guest speakers active in the area.

Time and Place

Please note: we have kept the Wednesday slot 11 - 13 hours, in the 'Diamantslijperij', and for a fall-back, we also have Thursdays 18 - 20 hours, 'Euclides' building.

Schedule

September

6 Games in logic, and logic in games

Logical notions can be cast in the form of 'logic games', and this leads to significant links with game theory. But also more generally, the structure of arbitrary games can be analyzed by logical means. For this purpose, we need to develop 'game logics' that combine ideas from computation (dynamic logics) and philosophy (epistemic logics). Here is a general Introduction. Two useful chapters with background: Evaluation Games, Comparison Games.

13 + 14 Philosophy meets computer science: epistemic and dynamic logic

We have surveyed the main ideas from epistemic logic and dynamic logic (ßsee handout with points): language, models, truth definition, validities, correspondence, bisimulation and invariance, and complexity. A text containing the whole story in more detail is the chapter on modal logic in a semantic perspective by Blackburn & van Benthem in the forthcoming Handbook of Modal Logic.

20 From public annoucement to dynamic epistemic logic

Read the introduction to the logic PAL of public announcement in the paper 'One is a Lonely Number'. We covered: basic epistemic-dynamic language, models, reduction axioms, completeness, decidability, adding common knowledge, bisimulation invariance. Two still open questions were mentioned: describing the substitution-closed validities, characterizing the persistent formulas whose public announcement turns them into (common) knowledge. A brief introduction was given to product update with event models. You can read the definitions later on in the same paper.

27 A logic of communication and change Barteld Kooi

Read the definition of DEL in the paper 'A Logic of Communication and Change', and get a sense of completeness theorems and other results. Some recent further literature was mentioned in class.

October

4 Dynamics of belief change and revision

We took two hours on Wednesday, going through the following handout. I hope that the apple symbols, which of course stand for the Tree of Knowledge, come through this time.

Read the paper 'Dynamic Logic of Belief Revision', as far as you can get. Background on belief revision is not needed, but you may want to check any standard source on 'AGM theory' and 'Grove models' (Google should help). By now, you should see the same dynamic logic ideas returning!

Our next block of three classes works with essentially the same epistemic accessibility + plausibility models which were used this week. But now they serve as a basis for new developments at ILLC in static and dynamic preference logics, which are related to plausibility reasoning in several ways.

11 Preference logic and games Olivier Roy

18 Preference change: qualitative and quantitative Fenrong Liu

Here is special webpage for this presentation, including a homework question.

25 Belief Revision and (Ceteris Paribus) Preference Logic Patrick Girard

Here is a handout of this presentation.

November

1 Dynamic logics of game structure Johan van Benthem

This is based on two papers that you can download under Research on Logic & Games at my website. They are called 'Extensive Games as Process Models' and 'Games in Dynamic Epistemic Logic'. We mainly discussed two basic levels for studying games: bisimulation and modal logic, and power equivalence and modal 'forcing languages'. Both introduce fine-structure into game theory, and allow us to balance expressive power versus computational complexity in describing players, and game solutions.

8  Complexity and games Merlijn Sevenster

This lecture will mainly evolve around the following two questions: 1. How can one measure the complexity of a game? 2. What properties make games harder? We will discuss win-loss games, and their computational complexity, in terms of some complexity theory: P, NP, PSPACE, EXP, NEXP. Papadimitriou's Theorem: Games that meet the following conditions are in PSPACE: 1. any legal sequence of moves is polynomially bounded, 2. all successors of a position can be enumerated in PSPACE; if there are none, it can be decided in PSPACE to whom the position belongs. Logical games of increasing complexity SAT -- NP -- 1 player game, QBF -- PSPACE -- 2 player game, IFQBF -- NEXPTIME -- 2 player, impf. inf. game, IFQBF + Perfect Recall -- PSPACE. "PlayGames" Minesweeper, Sudoku, Battleships -- NP, Geography -- PSPACE, Checkers, Chess -- EXPTIME. The effect of impf. inf. is not well understood, but: SY -- PSPACE. Reflections on the complexity theory measure for games: Advantages, Disadvantages

References: (a) C.H. Papadimitriou, 1994, Computational complexity -- especially chapter 19, (b) L. J. Stockmeyer and A. R. Meyer, 1973, Word problems requiring exponential time, Proceedings of the 5th ACM Symposium on the Theory of Computing (STOC 73), 1-9 -- here PSPACE-completeness of QBF is established. (c) R.J. Nowakowski, 2002, More games of no chance, Cambridge University Press -- gives a nice overview and up-to-date papers on combinatorial game theory. Don't forget to check out the list of open problems! (d) M. Sevenster, 2006, Branches of imperfect information: logic, games, and computation -- especially section 3.6 and chapter 6.

15 Epistemic-temporal logic Eric Pacuit

See the paper The Tree of Knowledge in Action, presented at AiML Melbourne 2006..

23 (Thursday 18;00 - 20 hours!) Workshop 1: Belief revision, correspondence, and temporal representation

29  (Wednesday 11:15 - 13 hours!) Workshop 2: Preference logic and games

December

Date to be arranged: paper/workshop presentations.

Prerequisites

A working knowledge of modal logic, plus some general logical sophistication.


Homework Assignments

Weeks 1: A question on first-order evaluation games

Look up the paper 'An Essay on Sabotage and Obstruction', ILLC Research Report 2005. Explain the sabotage game with some new example, verify the given translation for Traveler's being able to win into the truth of some matching first-order formula, and show that evaluation games for first-order formulas are determined, with an upper bound of polynomial space for their solution complexity.

Week 2A: A question on modal-epistemic frame correspondence

Consider the epistemic-modal principle [a]K phi <--> K[a] phi. Determine which relational conditions on epistemic-modal frames correspond to validity of the two separate implications, and prove this. Discuss the connection with one particular reduction axiom (which one?) of the logic of public announcement. What does this express about agents' powers? The [a]K/K[a] equivalence is almost valid in DEL product update, but with an important modification: explain.

Week 2B: A question on bisimulation and invariance

State and prove the Adequacy Lemma for modal bisimulation games, which says that Duplicator has a winning strategy in the game over k rounds if the initial pointed models have the same modal theory up to operator depth k. Also state the equivalent version for Spoiler, and compare the two versions. Explain the difference between the usual 'E-sick' statement of the result, and the more constructive information that we discussed in class.

Week 3: A question about completeness for public announcement logic

Look up the completeness proof for epistemic logic with conditional common knowledge in the paper 'A Logic of Communication and Change'. Explain the overall structure, and supply the missing steps.

Week 4:  Question on DEL supplied by our guest speaker Barteld Kooi: assignment. You can hand this in either by email by next Monday morning (get it out of your system!), or as part of the second batch of homeworks end of October.

Week 5: Homework question for dynamic logic of belief revision:

Give a complete soundness argument for the reduction axioms given in the paper for the 'conservative' variant of lexicographic upgrade. Also, give the complete modal correspondence argument analyzing the axiom for knowledge of agents after public announcements (you will encounter some technical issues to be resolved, but they are not major). Bonus: Explain how the uniform update rule of Baltag & Smets covers all cases dealt with in class, as well as those in van Benthem & Liu.

Week 6: Here is the assignment by Olivier Roy

Week 7: Here is the assignment by Fenrong Liu.

Week 8: Here is the assignment by Patrick Girard.

Week 9: (a) Complete the details of the representation argument for players' powers in terms of games given in class. (b) Look up the axioms for Rohit Parikh's 'Dynamic Logic of Games', either in the old lecture notes "Logic and Games", or in the Pauly/Parikh survey paper (check via Google). Explain the intended formal semantics, and show how the modality differs from the standard ones in relational semantics. Then show that the axioms are sound. Explain also how the Parikh modality could be formulated inside standard propositional dynamic logic, at least within a given game. (c) Try to define the Backward Induction solution to a finite game with values for outcomes using a combination of modal logic of actions and the preference logics you have learnt about in October. You can either look up a solution in the literature, or think up one for yourself.

If you have questions about the formulation or content of these Exercises, do send email.

Week 10 (Merlijn Sevenster): Please check with sevenstr@science.uva.nl for any questions about the following assignment.

Select two non-starred questions or one starred question and submit your answer to the selected problems electronically to Merlijn Sevenster. Note that the starred questions are challenging -- it would most certainly be appreciated if you gave one of them a try.

A. In class we discussed the complexity measure provided by computational complexity theory. But many more are available on the market. Give a short overview of two other measures of complexity for games (with examples!).

B. Give a detailed account (using pseudo code) of Papadimitriou's algorithm solving any game meeting the conditions 1. and 2 mentioned in class.

C. Prove that DQBF is computable in EXPTIME.

(*) D. Prove NEXP-hardness for DQBF by reducing from TILING, see Problem 20.2.10 on pg. 501 of Papadimitriou (1994).

E. Prove the equivalence: QBF = Gamified QBF. That is, show that a QBF instance F holds iff Eloise has a winning strategy in G(F).

(*) F. Let DQBF+PR be the fragment of DQBF, such that every F gives rise to a game G(F) that has perfect recall. Show that for every DQBF+PR instance F, there is a QBF instance G such that F holds iff G holds.

G. Extend the ladder SAT - QBF - DQBF+PR - DQBF by another SAT-like problem, that can be associated with a game-theoretic property. Here you can start from either game theory or logic. What, you guess, would be the problem's computational complexity?

H. It is sometimes informally argued that NP-completeness is a necessary property for a game to be interesting (for instance pg. 476 of A.S. Fraenkel (2002) in R.J. Nowakowski (2002) and http://www.ics.uci.edu/~eppstein/cgt/hard.html). Please give your opinion on this proposition supported by three arguments.

References

C.H. Papadimitriou, 1994, ComputationalComplexity -- especially chapter 19.

L. J. Stockmeyer and A. R. Meyer, 1973, Word problems requiring exponential time, Proceedings 5th ACM Symposium on the Theory of Computing (STOC 73), 1-9 -- here PSPACE-completeness of QBF is established.

R.J. Nowakowski, 2002, More games of no chance, Cambridge University Press -- gives a nice overview and up-to-date papers on combinatorial game theory. Don't forget to check out the list of open problems!

M. Sevenster, 2006, Branches of imperfect information: logic, games, and computation -- especially section 3.6 and chapter 6.

Week 11 (Eric Pacuit):Check with epacuit@science.uva.nl if clarification is needed.

For the precise definition of the no miracles and perfect recall properties, refer to the paper
`The Tree of Knowledge in Action: Towards a Common Perspective'.

(1) The no learning and no forgetting property from the Halpern and Vardi paper are as follows:

(nf) for all histories H, H', n,n',k\ge 0, if H_n\sim_i H'_n' and k\le n, then there is a k'\le n'
such that $H_k\sim_i H'_k'

(nl) for all histories H, H', if H_n \sim_i H'_m, then for all k\ge n, there is a l\ge m such that
H_k\sim_i H_l

Answer the following questions:

a. What is the precise connection between the no miracles property and the no learning property? Are they equivalent? Does one imply the other?

b. What is the precise connection between the perfect recall property and the no forgetting property? Are they equivalent? Does one imply the other?

c. Find ETL formulas that are validated in frames with the (nf) and the (nl) properties respectively.

2. Let M be a Kripke structure and E an event model. Prove that Tree(M, E)= ((M x E) x E) x E x ...
has the perfect recall and uniform no miracles property.

3. Find an event model E and an initial model M such that in the generated tree Tree(M, E)= ((M x E) x E) x E x ..., the number of nodes at each moment continues to grow (that is for each t\ge 0, the number of finite histories of length t+1 is greater than the number of finite histories of length t). Are the structures at each stage ``really different'' or is there a momen after which all the models are epistemically bisimilar?

Course Materials

General material on update logics and dynamic logics of games can be found on the web page Logic, Games and Computation at Amsterdam . You can also check my own website under Research, and  under Teaching for some earlier seminars. We will post relevant documents later on a weekly basis.

Some background literature

Earlier course webpage: Logic and Games. Check the electronic lecture notes Logic in Games , which will be updated periodically. Here is the Introduction to the 'Logic in Games' seminar from 2002. Update for everybody: Farewell to Loneliness. Recent challenge papers: Open Problems in Logical Dynamics, and Open Problems in Logic and Games. Publication details and further references: check again my webpage under Research. My own philosophical views: Epistemic Logic and Epistemology.

Here are some links for specific topics, but these will be updated as we proceed:

Contact

Write to johan@science.uva.nl with comments or suggestions.