Communication and Concurrency (VS1) (U02943)

? Credit Points : 10 ? SCQF Level : 10 ? Acronym : INF-4-COC-V

The course provides an introduction to the Calculus of Communicating Systems (CCS) giving the theoretical foundation , examples of practical applications and logics for describing important properties. The course focuses on a mathematical model of the behaviour of concurrent systems which treats crucial notions like deadlock and non-determinism, and which reflects the modular construction of systems. The course also focuses on specifying safety and liveness properties of such systems. The approach is a mixture of operational semantics, algebra and logic. It applies alike to hardware and software. Although CCS is one of several alternative approaches, the aim is to treat it in depth rather than to make superficial comparisons with others.

Entry Requirements

? This course is only available to part year visiting students.

? This course is a variant of the following course : U01953

? Pre-requisites : Successful completion of Year 3 of an Informatics Single or Combined Honours Degree, or equivalent by permission of the School. There are no formal prerequisites although the Language Semantics & Implementation course is particularly relevant. The course requires a reasonable mathematical ability. This course is only available to part-year visiting students who are only in Edinburgh for Semester 1.

Subject Areas

Home subject area

Computational Systems Biology, (School of Informatics, Schedule O)

Other subject areas

Theoretical Computer Science, (School of Informatics, Schedule O)

Delivery Information

? Normal year taken : 4th year

? Delivery Period : Semester 1 (Blocks 1-2)

? Contact Teaching Time : 2 hour(s) per week for 10 weeks

All of the following classes

Type	Day	Start	End	Area
Lecture	Monday	14:00	14:50	Central
Lecture	Thursday	14:00	14:50	Central

Summary of Intended Learning Outcomes

The goal of this course is to develop basic competence in using a process calculus for modelling systems and in understanding properties of systems as described in temporal logic. After completing the course successfully students should be able to:
- Analyse computation, particularly concurrent systems in the process calculus CCS. The analysis consists of modelling situations by abstracting away from details and recording their fundamentals in a small computationally and mathematically appropriate formalism and then doing the same for their specifications. Finally one understands how to use all this to increase systems reliability.
- Define behaviour of a system as a transition graph.
- Understand when two systems are behaviourally equivalent. as defined by the notion of bisimulation equivalence.
- Verify that two systems are equivalent or prove that they are not.
- Specify temporal properties of systems in the branching time logic CTL.
- Understand the meaning of temporal formulas.
- Show that a system has, or fails to have, a temporal property.
- Use tools for systems verification.
- Be able to assimilate knowledge about different formalisms and tools and put them to practical use. Understanding how to apply mathematical and logical ideas in systems and other computational contexts.