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).

CodeCOMPGL02
YearMSc
PrerequisitesN/A
Term1
Taught ByRobin Hirsch (50%)
Fabio Zanasi (50%)
AimsTransition 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.
Learning Outcomes

TBC

Content

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.

Assessment

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.

Resources

Reading list available via the UCL Library catalogue.