Fifth meeting of the Formal Methods Reading Group

Chapter 3 was concluded by me and Dr. Venkatesh began discussing the concept of concurrency in Chapter 4. My notes of the part of my lecture are here as FMRG-5. Dr. Venkatesh will also put up his notes soon at the wiki of http://enhanceedu.iiit.ac.in. You may send mail to choppell@gmail.com for the login name and password that are necessary to access the wiki.

Fourth Meeting of the Formal Methods Reading Group

The fourth set of notes is up as FMRG-4. In this we study automata for which there is no start state specified and all states are considered to be accepting states. This is defined as a set together with a collection of choice maps on the set. We define the notion of a strong simulation as a choice map that carries a transition between states to a transition between sets of states. Other ideas of Milner are expressed in similar terms. Would like to know from the readers if this makes it easier to understand Milner's ideas.

Third Meeting of the Formal Methods Reading Group

The third meeting took place on 3rd March. Most of the time was spent discussing the example of the faulty vending machine given by Milner as motivation for the notion of bisimilarity. It became clear that the example needs to be discussed more fully than in the earlier meeting. Accordingly the set of notes were written up. They are available here as FMRG-3. Lesson 3 is in the form of a story: "The Case of the Faulty Vending Machine - An Allegory for Software Engineers".