IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2007
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 16:00–17:50 B011
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
there are 19 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
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2008, Autumn 2009, Autumn 2010, Autumn 2011, Autumn 2012, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Autumn 2021.
  • Enrolment Statistics (Autumn 2007, recent)
  • Permalink: https://is.muni.cz/course/fi/autumn2007/IA040