Dynamic Logic

Fall 2023, Faculty of Arts, Charles University (Tuesdays 13:20–14:50)

Course outline

The course introduces some of the frameworks that have been proposed to formalize reasoning about programs, focusing on Kleene algebra, propositional dynamic logic, and some temporal logics.

Syllabus and materials

• 1. Programs and their semantics
  
  1.1 A propositional logic of programs and its relational semantics (3.10.)
  1.2 Trace semantics and its equivalence to relational semantics (10.–17.10.)
  1.3 Hoare logic (24.10.)
• 2. Kleene algebra with tests
  
  2.1 Semirings and Kleene algebras (24.10.)
  2.2 Regular expressions, Kozen's Theorem (31.10.)
  2.3 Kleene algebra with tests (21.11.)
• 3. Finite automata
  
  3.1 Finite automata (21.11.)
  3.2 Bisimulation and determinization (5.12.)
  3.3 Kleene's Theorem (12.12.)
  3.4 Guarded automata (19.12.)
• 4. Modal logic
  
  4.1 Basic modal logic (19.12. and 9.1.)
  4.2 Propositional Dynamic Logic (9.1.)
  4.3 Temporal logics of programs

Announcements

• No lecture on 7.11. (Sports Day), replacement: 21.11. (15:00–16:30)
• No lecture on 14.11., replacement: 5.12. (15:00–16:30)
• No lecture on 2.1., replacement to be agreed on

Reading

Besides the lecture notes, I suggest the following (more suggestions later):

• D. Blackubrn, M. de Rijke, Y. Venema: Modal Logic. Cambridge University Press, 2001.
• M. Huth and M. Ryan: Logic in Computer Science. Cambridge University Press, 2004.
• D. Harel, D. Kozen, J. Tiuryn: Dynamic Logic. MIT Press, 2000.
• T. Kappé: Elements of Kleene Algebra. Course at ESSLI 2023.

A useful tool for proving/disproving equations:

• Prover 9/ Mace 4 (a more modern online implementation here).

Grading

Lecture attendance and an assignment (at the end of the lecture period).

Office hours

By appointment (email me).