Teaching‎ > ‎

ESSLLI 2019: Quantifying over Information Change

Taught together with Hans van Ditmarsch

This is the external website for the ESSLLI 2019 course "Quantifying over Information Change". For now, this page contains a summary of the material that will be treated in the course and a list of references. The slides for the course have not been finalized yet, but will be posted here before ESSLLI starts.

Course abstract
In dynamic epistemic logics a modality that is interpreted as a model transformer represents information change. Examples are public announcement logic, action model logic, and arrow update logic. Such logics can be expanded with operators describing quantification over information change to represent, for example, 'there is an announcement after which formula phi is true' (where phi is some postcondition in the resulting structure), or 'there is an action model after which phi is true'. Over the past 10 to 15 years several such logics have been proposed. They are indispensable in describing epistemic planning problems. We will present various such logics in depth, and also sketch some general themes around update logics involving expressivity, axiomatization, decidability, quantifying over world/relation/factual change, and related logics such as sabotage logic.

Students taking this course are expected to know modal logic and to have at least some familiarity with dynamic epistemic logic.

Tentative course outline
Note that this is only a tentative outline. Expect the final outline to deviate at least somewhat from this one.
  • Day 1: Public announcement logic, action model logic, factual change and arrow update logic. Expressivity, update expressivity, decidability, axiomatization.
  • Day 2: Arbitrary public announcement logic (APAL), group announcement logic (GAL), and coalition announcement logic (CAL). Focus on expressivity results and axiomatizations. Mention of undecidability results. Further variations: fully arbitrary APAL, boolean APAL, positive APAL.
  • Day 3: Arbitrary arrow update logic, arbitrary action model logic, arbitrary arrow update model logic. Synthesis of action models and arrow update models.
  • Day 4: Refinement modal logic and refinement epistemic logic.
  • Day 5: (i) Undecidability of arbitrary arrow update logic and (ii) windup, including presentation on other issues such as: quantifying over public and private factual change, quantification in contingency logics, sabotage logic, (highly expressive) model transformers.
The following slides will be used. Please keep in mind that we will probably keep improving the slides until the day of the lecture. So the final slides may differ slightly from the ones listed below.
These exercises are completely optional; they serve only a food for thought for students who want to dive a bit deeper into the material.

Detailed description of the course
Epistemic logic, the logic of knowledge, can be used to describe the information state of one or more agents, and the knowledge that the agents possess in that situation. Basic epistemic logic by itself cannot, however, represent information change. So it cannot be used to reason about situations where agents learn new things, or forget things they already knew. Dynamic epistemic logic (DEL) is an extension of epistemic logic that does allow us to represent information change.

In DEL, information change is represented by so-called updates. An update is of the form <E>, where E is some kind of event that changes what information the agents possess. A formula <E>phi then means “after the event E has happened, phi will be true”. There are many different kinds of updates, representing different kinds of information changing events. The simplest type of update is the public announcement (Plaza, 1989, Baltag et al., 1998). A public announcement is of the form <psi>, and indicates that all agents are made aware of the truth of psi in a public fashion, for example by an announcement when all of them are present. As a simple example, suppose that a teacher announces to their class that the test will be on Friday. After such an announcement, it will be common knowledge between the teacher and the class that the test is indeed on Friday. In DEL, this can be represented as <p>Cp, where p is an atomic proposition meaning “the test is on Friday”.

Public announcements can only represent relatively simple events, in order to represent more complex events we can use different types of updates, such as action model logic (Baltag et al., 1998) or arrow update logic (Kooi & Renne, 2011). Arrow updates, like public announcements, represent events that are essentially public. Action models are a generalization of public announcements to events that are non-public. Similarly, arrow updates can be generalized to arrow update models (Kooi & Renne, 2011, Van Ditmarsch et al., 2018) that allow for non-public events.

One particular strand of further development in DEL is towards quantification over updates. Dynamic epistemic logic allows us to reason about the effects of a particular event that is specified in advance. Using quantified updates, we can reason about the effect of every possible update. A root of such investigations is Fine's work on propositional quantification (1970), and later work on bisimulation quantifiers (French, 2006). The first dynamic epistemic logic to explicitly use a quantified update was APAL: arbitrary public announcement logic (2008). The language op APAL contains an operator <>phi standing for 'there is psi such that after public announcement of psi, phi (is true)', subject to certain conditions on psi to avoid a circular definition. Such a logic is useful for analyzing knowability (if phi is true, is there an update after which the agent knows that phi?), and also in epistemic planning (given epistemic goal phi, is there an update/program realizing phi?). A number of variations of this logic have appeared since, with quantification over certain subsets of all public announcements. A well-established version is one where <G>phi stands for 'there are psi_1, ..., psi_n (one for each agent in G) such that after simultaneous public announcement by the agents in G of psi_1, ..., psi_n, phi (is true)'. This logic formalizes certain notions of agency and ability (Agotnes et al., 2010). Another version, with relations to game logics, has a similar operator but then expressing that the agents in G can realize phi no matter what the agents not in G do to prevent it (by simultaneous announcements).

Quantification over updates other than public announcements is also possible. Arbitrary action model logic (Hales, 2013) and arbitrary arrow update logic (Van Ditmarsch et al, 2017) quantify over action models and arrow updates, respectively, as their names suggest. Most, but not all, of these quantified update logics are undecidable. Whether they are axiomatizable is currently an open question, although the slightly more powerful arbitrary arrow update logic with common knowledge has been shown to be unaxiomatizable (Kuijer, 2017). Additionally, even for the decision problems that are decidable, the computational complexity tends to be rather high.

Another related logic is Refinement modal logic (Bozelli et al., 2014), which has a modality representing quantification over updates, but does not have (deterministic/concrete) update modalities in the object language to quantify over. The refinement modality can be nicely mapped to combinations of relativization and bisimulation quantifiers, and therefore is a decidable (but highly complex) logic. The meaning of the refinement operator is hard to describe informally, so it is difficult to find real-life examples that are well represented using refinements. Still, its technical properties make it very useful in theoretical computer science, for issues such as synthesis and simulation.

A number of other logics exist that are conceptually similar to quantified update logics, but that operate very differently from a technical point of view. These logics have very expressive quantifiers over information change (the reason they are expressive is that they are state-based, not model-based), and include sabotage logic (Van Benthem, 2005) as well as various works by Areces and Fervari on relation-changing modalities. Yet further developments envisage update logics with quantification over purely factual change, both public and private, reminiscent of the original Fine (1970) publication on propositional quantification.

In this ESSLLI course, we will discuss all types of quantified information change. We will explain the applications of the different logics, but also their downsides with respect to computational complexity. Additionally, we will compare the logics to one another, with emphasis on their expressivity and update expressivity.

  • Thomas Ågotnes, Philippe Balbiani, Hans van Ditmarsch, Pablo Seban: Group announcement logic. Journal of Applied Logic 8: 62-81 (2010)
  • Philippe Balbiani, Alexandru Baltag, Hans van Ditmarsch, Andreas Herzig, Tomohiro Hoshi, Tiago De Lima: 'Knowable' as 'known after an announcement'. Rev. Symb. Logic 1: 305-334 (2008)
  • Alexandru Baltag, Lawrence S. Moss, Slawomir Solecki: The logic of public announcements, common knowledge, and private suspicions. TARK 1998: 43-56 (1998)
  • Johan van Benthem: An essay on sabotage and obstruction. Mech. Math. Reasoning: 268-276 (2005)
  • Laura Bozzelli, Hans van Ditmarsch, Tim French, James Hales, Sophie Pinchinat: Refinement modal logic. Inf. Comput. 239: 303-339 (2014)
  • Hans van Ditmarsch, Wiebe van der Hoek, Barteld Kooi, Louwe B. Kuijer: Arbitrary arrow update logic. Artif. Intell. 242: 80-106 (2017)
  • Hans van Ditmarsch, Wiebe van der Hoek, Barteld Kooi, Louwe B. Kuijer: Arrow Update Synthesis. Preprint on ArXiv (2018)
  • Kit Fine: Propositional quantifiers in modal logic. Theoria 36: 336-346 (1970)
  • Tim French: Bisimulation quantifiers for modal logics. University of Western Australia (2006)
  • James Hales: Arbitrary Action Model Logic and Action Model Synthesis. LICS 2013: 253-262 (2013)
  • Barteld Kooi, Bryan Renne: Arrow update logic. Rev. Symb. Logic 4: 536-559 (2011)
  • Barteld Kooi, Bryan Renne: Generalized arrow update logic. TARK 2011: 205-211 (2011)
  • Louwe B. Kuijer: Arbitrary Arrow Update Logic with Common Knowledge is neither RE nor co-RE. TARK 2017: 373-381 (2017)
  • Jan Plaza: Logics of public communications. Fourth international symposium on methodologies for intelligent systems: Poster session program: 201–216 (1989).