Dr Szabolcs Mikulas / Teaching / Logic
Logic

Fundamentals of Concurrent Systems
(formerly Knowledge Representation and Reasoning)

Brief Introduction

Here is a brief introduction to the module.

Module Outline

Basics of concurrency (including interprocess communication) and a formal approach to modelling the behaviour of concurrent programs (including specification and verification).

Aims

In this module we will concentrate on concurrency (arising by the use of multithreaded programs or distributed computations). We will introduce a formal approach (labelled transition systems) for modelling concurrent programs and tools (modal and temporal logics) to reason about their behaviours. Applications include software engineering (formal specification and verification of concurrent programs) and distributed systems (reasoning about knowledge in multi-agent systems).

Syllabus

  • Concurrency mechanisms (semaphores, monitors, software solutions, message passing)
  • Modelling concurrent programs (labelled transition systems)
  • Basics of propositional logic (syntax, semantics, decidability)
  • Basics of modal and temporal logics (syntax, semantics)
  • Temporal logic as a specification language
  • Model checking for temporal logic
  • Verification using model checking
  • Rule-based verification
  • Other applications of modal/temporal logic (multi-agent systems, knowledge representation) - depending on student interest

Assessment

By compulsory homework (0%) and written examination (100%).
Previous exam papers (some questions are no longer relevant because of change in the syllabus): 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014.

Reading

Reading material include the lecture notes (to be distributed during the term), the textbook:
M. Huth nad M. Ryan, Logic in Computer Science, 2nd edition, Cambridge University Press, 2004, ISBN 0 521 54310 X
Additional readings will be recommended during the term.

Lectures (tentative program)

  • Week 1.
    Motivation - the use of logic in computer science. Logical approach to program specification and verification.
    Mathematical background (naive set theory and induction). Notes. Sets, operations on sets (union, intersection, complement, direct product, power set), cardinality (when two sets have the same number of elements).
    Homework: Exercise 1.1 (1) and Exercise 1.2 (2) from the notes.
  • Week 2.
    Mathematical background (ctd.). Relations as products of sets, functions; mathematical and structural induction (a powerful proof method by establishing a base case and then showing "inheritance").
    Propositional logic. Notes. Syntax: logical connectives (conjunction, disjunction, negation, implication) and well-formed formulas, parse tree, subformulas. Semantics: meaning/truth values of formulas, valuations, truth tables, satisfiability, validity, logical consequence.
    Homework: Exercise 1.5 (1) and Exercise 1.6 (1) from the notes.
  • Week 3.
    More propositional logic. Formalizing arguments. Semantic tableaux: a formal method for establishing satisfiability of formulas. Decidability: general procedures for determining which are the valid/satisfiable formulas.
    Homework: Exercise 2.5 from the notes and 1.4.7.(a) from the textbook.
  • Week 4.
    Basics of concurrency. Execution of concurrent (multithreaded or parallel) programs; interprocess communication (IPC) tools (semaphores, software solutions)
    Temporal logic. Notes. Basics of linear propositional temporal logic.
    Modelling program execution. Notes. Labelled transition systems.
  • Week 5.
    Temporal logic and transition systems. Notes. Temporal logic as a specification language and reasoning mechanism for verification.
    Model checking in temporal logic. Determining whether a formula is true in a model.
  • Week 6. Reading week.
  • Week 7. Lab session.
    Verification by model checking. Notes. Verifying properties of computations by checking whether the specification formula is true in the labelled transition system. NuSMV code for MUX-SEM.
  • Week 8. Lab session.
  • Week 9.
    Verification by rules. Notes. Using inductive arguments showing invariance properties, assertion strengthening.
    Homework: Exercise 7.4, Exercise 7.5(2), Exercise 7.6(2).
  • Week 10.
    Basics of modal logic. Notes. Different modes of truth (depending on time, location, belief, knowledge, etc.), modalities (boxes and diamonds), meanings of formulas by possible world semantics. Various flavours of ML (frame conditions).
    See Jan Jaspars' animations for logic.
  • Week 11.
    More on modal logic. Model checking (determining whether a formula is true in a given model), decidability (general procedure for determining which are the valid formulas).
    Basics of epistemic logic. Notes. Modelling knowledge in multi-agent systems, common and distributed knowledge, the muddy children puzzle. More epistemic logic. Temporal epistemic logic. -->