# 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.

- 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).