Skip to main content »

Trinity College Dublin

Dublin University Crest Department of Computer Science > Reactive Systems 2010 Lecture Progress Trinity College Crest
 Reactive Systems Home
 Reading List
 Lecture Material
 Worksheets
 Lecture Progress
 Assignments
 Verification Tools
 

Reactive Systems - 2010:
Lecture Progress

Here I will keep a brief record of the topics discussed in each lecture, as the course proceeds.
For reference below you can see how the course went the last time I gave it, in Autumn 2008.

  • Week 18: January 18th

    Lecture 1 : Admin. Gave introduction to the course

    Lecture 2: Thurs 15.00 - 17.00. Labelled transition systems. Communicating processes. An informal introduction. Chapter 2 of textbook.

  • Week 2: January 25:

    Lecture 1 : Wed 16.00 - 17.00 The language CCS: an informal introduction. Chapter 2 of textbook.

    Tutorial: Thurs 15.00 - 16.00. Worksheet 1, defining labelled Transition systems from English descriptions. We did not get to consider Question 4.

    Lecture 2: Thurs 16.00 - 17.00. The semantics of CCS processes. Using the rules in Table 2.2 of the textbook.

  • Week 3: February 1:

    Lecture 1 : Wed 16.00 - 17.00: An example of how to generate an LTS from a CCS description.

    Tutorial: Thurs 15.00 - 16.00. Worksheet 2. CCs formally. Generating LTSs from CCS descriptions using the formal semantics.

    Lecture 2: Thurs 16.00 - 17.00. More on CCS descriptions and LTSs. Specifications versus implementations. Intrduction to behavioural equivalences.

  • Week 4: February 8:

    Lecture 1 : Wed 16.00 - 17.00: Behavioural equivalences. Beginning Chapter three of textbook. Trace equivalence. Strong bisimulation equivalence

    Lecture 2: Thurs 15.00 - 16.00. Value-passing CCS. Section 2.2.3 of textbook.

    Tutorial: Thurs 16.00 - 17.00. Worksheet 3.

  • Week 5: February 15:

    Lecture 1 : Wed 16.00 - 17.00: Using games to characterise strong bisimulation equivalence

    Tutorial: Thurs 15.00 - 16.00. How to use the CWB

    Lecture 2: Thurs 16.00 - 17.00. Milners workshop

  • Week 6: February 22:

    Lecture 1 : Wed 16.00 - 17.00: Weak bisimulation equivalence

    Tutorial: Thurs 15.00 - 16.00. Deciding strong bisimulation equivalence using games

    Lecture 2: Thurs 16.00 - 17.00. Understanding weak bisimulation equivalence.

  • Week 7: March 1:

    Study week. No lectures.

  • Week 8: March 8:

    Lecture 1 : Wed 16.00 - 17.00: Hennessy-Milner Logic. Sections 5.1 and 5.2 of textbook.

    Tutorial: Thurs 15.00 - 16.00. Deciding weak bisimulation equivalence using games. Worksheet 4

    Lecture 2: Thurs 16.00 - 17.00. Weak Hennessy-Milner Logic and its relation with weak bisimulation equivalence.

  • Week 9: March 15:

    Lecture 1 : Wed 16.00 - 17.00: St patricks Day. No lecture.

    Lecture 2: Thurs 15.00 - 16.00. Cancelled

    Tutorial: Thurs 16.00 - 17.00. Cancelled

  • Week 10: March 22:

    Lecture 1 : Wed 16.00 - 17.00: No students

    Lecture : Thurs 15.00 - 17.00. The alternating bit protocol (Vasileios Koutavas)

  • Week 11: March 29:

    Lecture 1 : Wed 16.00 - 17.00:

    Tutorial: Thurs 15.00 - 16.00.

    Lecture 2: Thurs 15.00 - 17.00.

  • Week 12: April 05:

    Lecture 1 : Wed 16.00 - 17.00.

    Lecture 2: Thurs 15.00 - 17.00. Recursive HML formulae (Edsko deVries)

  • Extra: April 21st: Two hour revision (Edsko DeVries)


    Reactive Systems course Autumn 2008:

    • Week 1: October 6th:

      Tutorial 1 : (Monday) No show

      Lecture 1: (Thursday) Labelled Transition Systems. How to use them to descibe reactive systems

    • Week 2: October 13th:

      Tutorial 2: (Monday) We did first half of worksheet1.

      Lecture 2: (Thursday) The language CCS
      Covered the syntax and semantics of CCS. Including the use of the SOS rules in Table 2.2 of the textbook for defining the actions of a process.
      All material taken from Section 2.1 and Section 2.2 of the textbook.

    • Week 3: October 20th:

      Tutorial 2: (Monday) : Working through worksheet2.

      Lecture 3: (Thursday) Translating CCS expressions into LTSs; some examples
      Behavioural equivalences: Sections 3.1 and 3.2 of textbook.
      Trace equivalence.
      Why trace equivalence is not adequate.

    • Week 4: October 27th:

      Tutorial: (Monday) Bank holiday

      Lecture 4: (Thursday) We went through worksheet on how to use the CWB.
      Then talked about strong bisimulations, and strong bisimulation equivalence. Section 3.3 of textbook.

    • Week 5: November 3rd:

      Tutorial: (Monday) Worksheet 3

      Lecture 5: (Thursday) Value-passing CCS, Section 2.2.3 of textbook
      How to show processes are not equivalent using games, Section 3.5 of textbook,
      Weak bisimulations, Section 3.4 of textbook.

    • Week 6: November 10th:

      Tutorial: (Monday) Finished worksheet3, started worksheet4

      Lecture 6: (Thursday)
      Finished Topic 4. Including properties of weak bisimulation equivalence.
      Discussed the example protocol in Table 3.1 of textbook.
      Started Topic 5.

    • Week 7: November 17th:

      Tutorial: (Monday) 15.00 - 16.00
      More on Worksheet4.

      Lecture 7: (Thursday) 16.00 - 18.00
      Hennessy-Milner logic. Sections 5.1 and 5.2 of textbook.

    • Week 8: November 24th:

      Tutorial: (Monday) 14.00 - 15.0. Some questions from Worksheet5
      Lecture 8.1: (Monday) 15.00 - 16.00. Tarkski's fixpoint theorem. An overview of Sections 4.1 and 4.2 of textbook.

      Lecture 8.2 : (Thursday) 16.00 - 18.00: The alternating bit protocol.
      Modal formulae with maximal and minimal fixpoints. Sections 6.1 and 6.2 of textbook.

    • Week 9: December 1st:

      Tutorial: (Monday) 14.00 - 16.00: Worksheet6. Questions 1 to 4 were tackled.
      Discussion of how to formulate interesting properties such as deadlock, livelock, and eventually.

    THE END

Email  WebAdmin @ cs.tcd.ie