FI:IA040 Modal and Temporal Logics for - Course Information
IA040 Modal and Temporal Logics for Processes
Faculty of InformaticsAutumn 2005
- 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 12:00–13:50 B411
- Prerequisites
- ! I040 Modal and Temporal Logics for Processes
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
- there are 6 fields of study the course is directly associated with, display
- 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 2005, recent)
- Permalink: https://is.muni.cz/course/fi/autumn2005/IA040