I040 Modal and Temporal Logics for Processes

Faculty of Informatics
Spring 2000
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.
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 taught: every week.
The course is also listed under the following terms Spring 1996, Spring 1997, Spring 1998, Spring 1999, Spring 2001, Spring 2002.
  • Enrolment Statistics (Spring 2000, recent)
  • Permalink: https://is.muni.cz/course/fi/spring2000/I040