Concurrency - week 6

Exercise class (October 3 - 6)

1. Regular safety properties: [B&K] Exercise 4.1
2. Product of TS and NFA: [B&K] Exercise 4.5
3. Show that each of the following properties (about some mutual exclution algorithm for two processes) is -regular:
   • Process 1 will eventually enter its critical region
   • Process 1 will enter its critical region infinitely often
   • Process 1 will, if waiting, eventually enter its critical region
   • Each of the two processes will eventually enter its critical region
   [ Hint ] Then show that each of the four properties can also be expressed formally using LTL.
4. Model checking with a regular safety property: [B&K] Exercise 4.6
5. Model checking with an -regular property: Go through the example on slide 41 and step-by-step explain how the model checking algorithm works.
6. From -regular expression to NBA: [B&K] Exercise 4.11 [ Hint ]
7. Equivalence of NBAs and -regular expressions: Go through the proof of Theorem 4.32 in [B&K] pp. 178-182. (You may skip the second part, i.e. Lemma 4.39.)
8. Give an example of a linear-time property that is not -regular. Also, give an example of an -regular property that cannot be expressed using LTL. [ Hint ] (Argue informally, or - if you are ambitious - prove that your examples are correct.)

Hand-in #6

In the last few weeks, we have studied a range of classes of properties of transition systems:

• linear-time properties
• safety properties
• liveness properties
• progress properties
• LTL-expressible properties
• regular safety properties
• invariant properties
• -regular properties
• persistence properties

In this final hand-in exercise, your task is to summarize the known relationships between these classes. Which classes are contained within which other classes? (You should briefly explain why, in each case.) Also, give examples of properties that distinguish the different classes (that is, belong to one class but not another). [ Hint ]