To fully understand the lessons, students should be familiar with the following topics:

• basic terms of formal language theory: an alphabet, a word, a (formal) language, etc.
• languages over infinite words and Büchi automata - see Section 9.1 of [CGP99] or Chapter 5 of [Pel01]
• Linear Temporal Logic (LTL) - see Chapter 3 of [CGP99] or Chapter 5 of [Pel01]
• automata-based LTL Model Checking - see Chapter 9 of [CGP99] or Chapter 6 of [Pel01]
• pushdown processes - will be recalled in the course

It is also assumed that studentds have some knowledge of the folloing topics (as they are definitely parts of the verification area). However, we will not elaborate on these topics in the course:

• symbolic model checking - briefly explained in the course IV113 Introduction to Validation and Verification and in a more detailed way in Chapter 6 of [CGP99]
• bisimulation equivalence and equivalence checking - explained in the course IA006 Selected Topics on Automata Theory and in Chapter 8 of  [Pel01]

Where:

• [CGP99] stands for the book E. M. Clarke, O. Grumberg, and D. A. Peled: Model Checking, MIT Press, 1999 (available in FI library), and 
• [Pel01] stands for the book D. A. Peled: Software Reliability Methods, Springer, 2001 (available in FI library).

Examination:

• oral exam
• no intrasemestral tests, no written exams, no mandatory homeworks