Topic

No. of hours

Lecture

Tutorial/Practical

Multi-agent systems. Modal logic, Kripke models, epistemic logic.

3

3

-

Temporal logic, linear vs. branching time, synchronous vs. asynchronous product.

3

3

-

Standard non-symbolic algorithms. Model generators for partial order reductions (interleaved interpreted systems).

3

3

-

Partial order reduction methods, introduction to symbolic model checking. Logics for real time.

6

6

-

Strategic logics, ATL. Basic model checking algorithm for ATL.

3

3

-

Imperfect information scenarios. Demo (MCMAS).

3

3

-

Model checking complexity for explicit models, example complexity proofs.

3

3

-

Complexity revisited higher-order representations.

3

3

-

Timed automata, detailed region graphs, timed CTLK.

3

3

-

Standard non-symbolic model checking, complexity results.

6

6

-

BDD-based and SAT-based approaches to model checking, bounded and unbounded model checking for CTLK, unbounded model checking for ATL.

6

6