IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2021
Extent and Intensity
2/0. 2 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
Taught in person.
Teacher(s)
prof. RNDr. Luboš Brim, CSc. (lecturer)
Guaranteed by
prof. RNDr. Luboš Brim, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Supplier department: Department of Computer Science – Faculty of Informatics
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 57 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Learning outcomes
By the end of the semester, students should be able: • to understand and apply definitions of the logics and logical systems presented in the course, the ideas of the proofs; • to understand the differences in the logics, and their capabilities and limitations; • to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
lecture, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
The course is taught annually.
The course is taught: every week.
Teacher's information
https://www.fi.muni.cz/usr/brim/home/#teaching
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, 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.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2020
Extent and Intensity
2/0. 2 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
Taught online.
Teacher(s)
prof. RNDr. Luboš Brim, CSc. (lecturer)
Guaranteed by
prof. RNDr. Luboš Brim, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Tue 10:00–11:50 B411
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 57 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Learning outcomes
By the end of the semester, students should be able: • to understand and apply definitions of the logics and logical systems presented in the course, the ideas of the proofs; • to understand the differences in the logics, and their capabilities and limitations; • to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
lecture, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
The course is taught once in two years.
Teacher's information
https://www.fi.muni.cz/usr/brim/home/#teaching
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, 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 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2019
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. Luboš Brim, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Wed 14:00–15:50 B410
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 57 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Learning outcomes
By the end of the semester, students should be able: • to understand and apply definitions of the logics and logical systems presented in the course, the ideas of the proofs; • to understand the differences in the logics, and their capabilities and limitations; • to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
seminar, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/usr/brim/ia040.html
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, Autumn 2008, Autumn 2009, Autumn 2010, Autumn 2011, Autumn 2012, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2020, Autumn 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2018
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.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Tue 12:00–13:50 B411
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 28 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Learning outcomes
By the end of the semester, students should be able: • to understand and apply definitions of the logics and logical systems presented in the course, the ideas of the proofs; • to understand the differences in the logics, and their capabilities and limitations; • to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
seminar, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/usr/brim/ia040.html
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, Autumn 2008, Autumn 2009, Autumn 2010, Autumn 2011, Autumn 2012, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2019, Autumn 2020, Autumn 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2017
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.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Tue 12:00–13:50 B411
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 28 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Learning outcomes
By the end of the semester, students should be able: • to understand and apply definitions of the logics and logical systems presented in the course, the ideas of the proofs; • to understand the differences in the logics, and their capabilities and limitations; • to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
seminar, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/usr/brim/ia040.html
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, Autumn 2008, Autumn 2009, Autumn 2010, Autumn 2011, Autumn 2012, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2018, Autumn 2019, Autumn 2020, Autumn 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2016
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.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Tue 10:00–11:50 B410
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 28 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
seminar, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/usr/brim/ia040.html
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, Autumn 2008, Autumn 2009, Autumn 2010, Autumn 2011, Autumn 2012, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Autumn 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2015
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.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Thu 12:00–13:50 B410
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 28 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
seminar, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/usr/brim/ia040.html
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, Autumn 2008, Autumn 2009, Autumn 2010, Autumn 2011, Autumn 2012, Autumn 2013, Autumn 2014, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Autumn 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2014
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.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Wed 12:00–13:50 B410
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 27 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
seminar, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/usr/brim/ia040.html
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, Autumn 2008, Autumn 2009, Autumn 2010, Autumn 2011, Autumn 2012, Autumn 2013, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Autumn 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2013
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.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Thu 14:00–15:50 B411
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 27 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
seminar, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fimuni.cz/usr/brim/ia040.html
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, Autumn 2008, Autumn 2009, Autumn 2010, Autumn 2011, Autumn 2012, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Autumn 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2012
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.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Thu 14:00–15:50 B411
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 27 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
seminar, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
Study Materials
The course is taught annually.
Teacher's information
http://www.fimuni.cz/usr/brim/ia040.html
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, Autumn 2008, Autumn 2009, Autumn 2010, Autumn 2011, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Autumn 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2011
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 14:00–15:50 G123
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 27 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
seminar, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
Study Materials
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 2007, Autumn 2008, Autumn 2009, Autumn 2010, Autumn 2012, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Autumn 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2010
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 13:00–14:50 B410
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 26 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
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
Teaching methods
lectures, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
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 2007, Autumn 2008, Autumn 2009, Autumn 2011, Autumn 2012, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Autumn 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2009
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 10:00–11: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 26 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
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
Teaching methods
lectures, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
Study Materials
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 2007, Autumn 2008, Autumn 2010, Autumn 2011, Autumn 2012, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2017, Autumn 2018, Autumn 2019, Autumn 2020, Autumn 2021.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2008
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 13:00–14:50 B410
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 aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analyzis and verification of computer systems.
By the end of the semestr, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
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
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
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 2007, 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.

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.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2006
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 B204
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
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2007, 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.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 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
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2006, Autumn 2007, 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.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2004
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 14:00–15:50 B410
Prerequisites
! I040 Modal and Temporal Logics for Processes
Recommended: IV010 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
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 2005, Autumn 2006, Autumn 2007, 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.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2003
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
Wed 10:00–11:50 B411
Prerequisites
! I040 Modal and Temporal Logics for Processes
Recommended: IV010 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
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.
  • 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 2004, Autumn 2005, Autumn 2006, Autumn 2007, 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.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 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.
The course is also listed under the following terms Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, 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.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2023

The course is not taught in Autumn 2023

Extent and Intensity
2/0. 2 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
Taught in person.
Teacher(s)
prof. RNDr. Luboš Brim, CSc. (lecturer)
Guaranteed by
prof. RNDr. Luboš Brim, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Supplier department: Department of Computer Science – Faculty of Informatics
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 58 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Learning outcomes
By the end of the semester, students should be able: • to understand and apply definitions of the logics and logical systems presented in the course, the ideas of the proofs; • to understand the differences in the logics, and their capabilities and limitations; • to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
lecture, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
The course is taught annually.
The course is taught: every week.
Teacher's information
https://www.fi.muni.cz/usr/brim/home/#teaching
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, 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.

IA040 Modal and Temporal Logics for Processes

Faculty of Informatics
Autumn 2022

The course is not taught in Autumn 2022

Extent and Intensity
2/0. 2 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
Taught in person.
Teacher(s)
prof. RNDr. Luboš Brim, CSc. (lecturer)
Guaranteed by
prof. RNDr. Luboš Brim, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Supplier department: Department of Computer Science – Faculty of Informatics
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 58 fields of study the course is directly associated with, display
Course objectives
The aim is to acquire basic knowledge and develop skills in the use of modal and temporal logics for specification, analysis and verification of computer systems.
By the end of the semester, students should be able:
to understand definitions of the logics and logical systems presented in the course, the ideas of the proofs;
to understand the differences in the logics, and their capabilities and limitations;
to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Learning outcomes
By the end of the semester, students should be able: • to understand and apply definitions of the logics and logical systems presented in the course, the ideas of the proofs; • to understand the differences in the logics, and their capabilities and limitations; • to understand the utility, potential and limitations of formal verification, in particular model checking, for linear-time and branching-time logics.
Syllabus
  • Modal logics: propositional modal logic, modal mu-calculus.
  • Temporal logics: propositional temporal logic, linear and branching time, temporal operators.
  • 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
Teaching methods
lecture, homeworks, reading
Assessment methods
Final exam is both written and oral. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
Language of instruction
Czech
Further Comments
Study Materials
The course is taught annually.
The course is taught: every week.
Teacher's information
https://www.fi.muni.cz/usr/brim/home/#teaching
The course is also listed under the following terms Autumn 2002, Autumn 2003, Autumn 2004, Autumn 2005, Autumn 2006, Autumn 2007, 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 (recent)