FI:IA040 Logics for Processes - Course Information

IA040 Modal and Temporal Logics for Processes

Extent and Intensity

2/0. 2 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).

Teacher(s)

prof. RNDr. Luboš Brim, CSc. (lecturer)

Guaranteed by

prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.

Timetable

Thu 16:00–17:50 B011

Prerequisites

Recommended: IV010 Communication and Parallelism

Course Enrolment Limitations

The course is also offered to the students of the fields other than those the course is directly associated with.

fields of study / plans the course is directly associated with

• Applied Informatics (programme FI, N-AP)
• Information Technology Security (programme FI, N-IN)
• Bioinformatics (programme FI, N-AP)
• Information Systems (programme FI, N-IN)
• Informatics (programme FI, M-IN)
• Informatics (programme FI, N-IN)
• Mathematical Informatics (programme FI, B-IN)
• Parallel and Distributed Systems (programme FI, N-IN)
• Computer Graphics (programme FI, N-IN)
• Computer Networks and Communication (programme FI, N-IN)
• Computer Systems (programme FI, N-IN)
• Embedded Systems (eng.) (programme FI, N-IN)
• Theoretical Informatics (programme FI, N-IN)
• Upper Secondary School Teacher Training in Informatics (programme FI, M-SS)
• Upper Secondary School Teacher Training in Informatics (programme FI, M-TV)
• Upper Secondary School Teacher Training in Informatics (programme FI, N-SS) (2)
• Artificial Intelligence and Natural Language Processing (programme FI, N-IN)
• Image Processing (programme FI, N-AP)

Course objectives

The goal is acquire basic knowledge about tempral logics as used for the verification of reactive systems. The emphasis is on comparison of expressive power and decidability.

Syllabus

• Modal logics: propositional modal logic, modal mu-calculus.
• Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
• Real-Time logics.
• Classification of properties, liveness, safety, local and global properties.
• Model checking, applications.

Literature

• GRUMBERG, Orna, Doron A. PELED and E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
• MANNA, Zohar and A. PNUELI. Temporal verification of reactive systems : safety. New York: Springer, 1995, xviii, 512. ISBN 0387944591. info
• Handbook of logic in computer science. Edited by Samson Abramsky - Dov M. Gabbay - Thomas S. E. Maibaum. Oxford: The Clarendon Press, 1992, 571 s. ISBN 0198537611. info

Assessment methods (in Czech)

Zkouška je písemná a ústní. V případě zadání průběžných testů během semestru, mají tyto podíl nejvýše 30% na závěrečném hodnocení. Pomocné materiály nejsou povoleny.

Language of instruction

Czech

Further Comments

The course is taught annually.

Teacher's information

http://www.fimuni.cz/usr/brim/IA040

• Enrolment Statistics (Autumn 2007, recent)
  
• Permalink: https://is.muni.cz/course/fi/autumn2007/IA040