6752 18s1 guest lectures

for everything else about this course go to Rob's page for the course.

Notes/Slides for week 5

Homework for week 5

due at 10am on April 9th. Submit as usual. You can email questions about homework to Kai. They should then be listed and answered on the Q&A page.

Exercise 1

  1. Research the dining philosophers problem.
  2. Model 5 dining philosophers as an abstract machine. Make it as simple as possible. Ignore forks for now. All we care about is that philosophers alternate between thinking and eating, and that there's a restriction in place that prevents philosophers from eating when either of their immediate neighbours is already eating. (This machine should not have more than 32 states.)
  3. Argue informally that your first model is accurate, show that it has only infinite derivations, and that individual philosophers could starve.
  4. Refine your model to one with forks that are picked up individually. Do not prescribe an order in which forks are picked up. Preserve who's eating/thinking.
  5. Show that this second model has deadlock potential (maximal finite sequences that aren't derivations).
  6. Use the notion of simulation\({}^*\) introduced in the Monday lecture and prove that your second model simulates the first while preserving who is eating and who is thinking. Draw conclusions about what is not necessarily preserved by simulation\({}^*\).
  7. Improve your model to prevent deadlocks (and show that the improved model has this property)
  8. Prove that your third model simulates the second one, this time also preserving who has which fork(s).

Exercise 2

Suppose we add sequential composition \(E\mathbin{;}E\) to the syntax of CSP as it is presented in Rob's notes. Give SOS rules in GSOS format for the new operator. For instance, we'd want that \(a\to{\rm\small STOP} \mathbin{;} b\to{\rm\small STOP}\) is equivalent to \(a\to b\to{\rm\small STOP}\).

Exercise 3 (challenge)

Let the set \(\mathcal{A}\) of communications be finite. Does the addition of a sequential composition operator increase the expressive power of CSP?
Potential hint or obfuscation: one could attempt to answer this question in the positive by showing that: Alternatively, give a CSP expression strictly within the language as described in Rob's note (i.e., without "\(;\)") that has the language \(M\) as finite traces.

Solutions

are here.

Notes/Slides for week 6

Monday: state machines for concurrency

Tuesday: security and process algebra

Homework for week 6

due at 10am on April 16th. Submit as usual.
  1. Give an example of TSS that is in GSOS format except for failing the requirement that all variables occurring in the source of a rule must be different. Show that bisimulation fails to be a congruence for this TSS.
  2. Suppose our propositions are \(\{a,b,c\}\). Give an LTL formula for each of the following requirements.
    1. \(a\) and \(b\) are never true at the same time
    2. every \(a\) is followed by a \(b\) (which is short for: whenever \(a\) is true there is a later time where \(b\) is true)
    3. no \(b\) occurs without an \(a\) having occurred already
    4. every \(a\) is followed either by a \(b\) or a \(c\). Whether this response is followed by another \(a\) depends on what the response is: if the response is \(b\) then there will be another \(a\) but if it's a \(c\) then we've seen the last \(a\).
  3. omitted to compensate for the relatively laborious week 5 homework set

Maintained by: Kai Engelhardt
Last modified: Sun Apr 15 13:55:43 AEST 2018