I040 Modal and Temporal Logics for Processes

Faculty of Informatics
Spring 2002
Extent and Intensity
0/2. 2 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium), 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 13:00–14:50 B411
Prerequisites
Recommended: I010 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
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.
The course is also listed under the following terms Spring 1996, Spring 1997, Spring 1998, Spring 1999, Spring 2000, Spring 2001.
  • Enrolment Statistics (recent)
  • Permalink: https://is.muni.cz/course/fi/spring2002/I040