FI:IA040 Modal and Temporal Logics for - Course Information
IA040 Modal and Temporal Logics for Processes
Faculty of InformaticsAutumn 2002
- Extent and Intensity
- 0/2. 2 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: z (credit).
- 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 15:00–16:50 B411
- Prerequisites
- ! I040 Modal and Temporal Logics for Processes
Recommended: I010 Communication and Parallelism - Course Enrolment Limitations
- The course is only offered to the students of the study fields 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 (in Czech)
- Cílem předmětu je získat základní přehled o temporálních logikách, které jsou používány při verifikaci souběžných systémů. Důraz je v oblasti porovnání jejich vyjadřovací síly a rozhodnutelnosti.
- Syllabus
- Modal logics: propositional modal logic, modal mu-calculus.
- Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
- Real-Time logics.
- Verification of sequential processes (Hoare logic).
- Classification of properties, liveness, safety, local and global properties.
- Model checking.
- Literature
- 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
- Language of instruction
- Czech
- Further Comments
- The course is taught annually.
- Enrolment Statistics (Autumn 2002, recent)
- Permalink: https://is.muni.cz/course/fi/autumn2002/IA040