Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
[go: Go Back, main page]
Models of Concurrent Computation

Models of Concurrent Computation

This course runs on Tuesdays at 9--11 and 2-3 in room 145.

Course Material

CCS

  • Introduction to course
  • Introduction to CCS with accompanying lecture notes
  • Value-passing CCS
  • Modal Logic
  • The Concurrency Workbench
  • Strong Bisimulation
  • Weak Bisimulation

    Exercises associated with CCS will be posted here . There will be an assessed exercise sheet on CCS, hand-out date 31st October, submission date Friday 10th November.

    The Pi calculus

    Sergio Maffeis will be giving this half of the course. See https://www.doc.ic.ac.uk/~maffeis/teaching/

    Iain Phillips' previous course

    The slides for Iain Phillips former course on Models of Concurrent Computation can be found here.

    Recommended Books

    Communication and Concurrency, Robin Milner , Prentice Hall, 1989. This one is important.

    Modal and Temporal Properties of Processes, Colin Stirling, Springer, 2001. First chapter will be given out in the lectures.

    Communicating and Mobile Systems: the Pi calculus, Robin Milner, Cambridge University Press, 1999. Also worth reading.

    The Pi calculus: a Theory of Mobile Processes, Davide Sangiorgi and David Walker, Cambridge University Press, 2001. Only for enthusiasts!

    The Edinburgh Concurrency Workbench

    The Workbench is a tool for describing, exploring and automatically verifying systems modelled in CCS. It is a good idea to use this tool as an aid towards understanding the course. Knowledge of the tool will not be formally assesssed in this course. Documentation

  • An introductory workout (postscript-file), written by Joachim Parrow. It takes you step by step through the basic features of the Workbench.
  • Examples of systems modelled as CCS processes.
  • A file of macros that must be used for exercises about CTL-. Copy it into the directory from which you call the Workbench as filename.cwb, and after calling the Workbench type the command ``input "filename.cwb";''. CTL- is an specification language which will be introduced in the lectures.
  • A train crossing
    • Philippa Gardner, pg @ doc.ic.ac.uk