Fundamentals of Concurrent Systems
Knowledge Representation and Reasoning)
Here is a brief
to the module.
Basics of concurrency (including interprocess communication)
and a formal approach to modelling the behaviour of concurrent programs
(including specification and verification).
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).
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
Other applications of modal/temporal logic (multi-agent systems, knowledge representation) - depending on student interest
By compulsory homework (0%) and written examination (100%).
Previous exam papers (some questions are no longer relevant
because of change in the syllabus):
Reading material include the lecture notes (to be distributed during the term),
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)
Motivation - the use of logic in computer science.
Logical approach to program specification and verification.
Mathematical background (naive set theory and induction).
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.
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").
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.
More propositional logic.
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.
Basics of concurrency.
Execution of concurrent (multithreaded or parallel) programs;
interprocess communication (IPC) tools
(semaphores, software solutions)
Basics of linear propositional temporal logic.
Modelling program execution.
Labelled transition systems.
Temporal logic and transition systems.
Temporal logic as a specification language and reasoning mechanism
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.
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.
Verification by rules.
Using inductive arguments showing invariance properties, assertion strengthening.
Homework: Exercise 7.4, Exercise 7.5(2), Exercise 7.6(2).
Basics of modal logic.
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.
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.
Modelling knowledge in multi-agent systems,
common and distributed knowledge,
the muddy children puzzle.
More epistemic logic.
Temporal epistemic logic.