Dynamic logic - ALGV19008

• Title: Dynamic logic
• Guaranteed by: Department of Logic (21-KLOG)
• Faculty: Faculty of Arts
• Actual: from 2022
• Semester: winter
• Points: 4
• E-Credits: 4
• Examination process: winter s.:
• Hours per week, examination: winter s.:2/0, C [HT]
• Capacity: unlimited / unknown (unknown)
• Min. number of students: unlimited
• 4EU+: no
• Virtual mobility / capacity: no
• State of the course: taught
• Language: English
• Teaching methods: full-time
• Teaching methods: full-time
• Note: course can be enrolled in outside the study plan; enabled for web enrollment
• Guarantor: Mgr. Igor Sedlár
• Teacher(s): Mgr. Igor Sedlár

Annotation

Last update: Mgr. Šárka Stejskalová, Ph.D. (23.09.2021)

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

Literature

Last update: Mgr. Šárka Stejskalová, Ph.D. (23.09.2021)

[1] D. Harel, D. Kozen, and J. Tiuryn, Dynamic Logic. MIT Press, 2000.
[2] J. E. Hopcroft, R. Motwani, and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd Edition. Pearson Education, 2007.
[3] M. Huth and M. Ryan, Logic in Computer Science. Modelling and Reasoning about Systems, 2nd edition. Cambridge University Press, 2004.

Syllabus

Last update: Mgr. Šárka Stejskalová, Ph.D. (23.09.2021)

1. Modal logic
2. Operational semantics of programs and program verification
3. Finite automata and regular expressions
4. Propositional dynamic logic
5. Kleene algebra and Kleene algebra with tests
6. Temporal logics and model checking
7. Automata-theoretic techniques in logics of programs