FI:IA040 Logics for Processes - Course Information
IA040 Modal and Temporal Logics for Processes
Faculty of InformaticsAutumn 2011
- 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 14:00–15:50 G123
- 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 (eng.) (programme FI, D-IN4)
- Informatics (programme FI, D-IN4)
- 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 and Technologies (eng.) (programme FI, D-IN4)
- Computer Systems and Technologies (programme FI, D-IN4)
- Computer Systems (programme FI, N-IN)
- Embedded Systems (eng.) (programme FI, N-IN)
- Embedded Systems (programme FI, N-IN)
- Service Science, Management and Engineering (eng.) (programme FI, N-AP)
- Service Science, Management and Engineering (programme FI, N-AP)
- Social Informatics (programme FI, B-AP)
- 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 aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics. - Syllabus
- Modal logics: propositional modal logic, modal mu-calculus.
- Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
- 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
- Teaching methods
- seminar, homeworks, reading
- Assessment methods
- Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
- Language of instruction
- Czech
- Further Comments
- Study Materials
The course is taught annually. - Teacher's information
- http://www.fimuni.cz/usr/brim/IA040
- Enrolment Statistics (Autumn 2011, recent)
- Permalink: https://is.muni.cz/course/fi/autumn2011/IA040