COMPGL02 - Modal Logic and Transition Systems
This database contains the 2017-18 versions of syllabuses. Syllabuses from the 2016-17 session are available here.
Note: Whilst every effort is made to keep the syllabus and assessment records correct, the precise details must be checked with the lecturer(s).
|Taught By||Robin Hirsch (50%)|
Fabio Zanasi (50%)
|Aims||Transition systems are a simple, yet pervasive mathematical structure adapted to the description of discrete computing devices and processes. This course introduces various formal methods of reasoning about transition systems. The focus is on modal logic, an extension of classical logic with operators, which serves as a specification language for system properties and their verification. We will explore connections of modal logic with relational algebra, game theory, proof theory and automata, as well as its computational complexity and expressiveness. The second part of the course will focus on extensions of modal logic with fixed-point operators, which are essential to capture time-based properties of systems.|
The syllabus consists of the following parts
Part I: Modal Logic
- Modal logic, dynamic logic: Syntax and semantics
- Completeness, Deduction, Complexity
- Behavioural equivalences on transition systems (traces, bisimulation)
- Algebras of relations
- Verification games
- Games and representations
Part II: Modal Fixpoint Logic
- Basic fixpoint theory; fixpoint properties of transition systems (safety, liveness…)
- Modal fixpoint logics: LTL, CTL, CTL*, the modal μ-calculus
- Algebraic semantics and game semantics
- Automata characterisations: Büchi and alternating automata.
- Automata-based model checking
Method of Instruction
2 hours of lectures and 2 hours of practicals/classes per week.
The course has the following assessment components:
- Coursework (20%)
- Written examination (2 hours, 80%)
To pass this course, students must:
- Obtain an overall pass mark of 50% for all sections combined.
Reading list available via the UCL Library catalogue.