- Research the dining philosophers problem.
- 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.)
- Argue informally that your first model is accurate, show that it has only infinite derivations, and that individual philosophers could starve.
- 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.
- Show that this second model has deadlock potential (maximal finite sequences that aren't derivations).
- 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\({}^*\).
- Improve your model to prevent deadlocks (and show that the improved model has this property)
- Prove that your third model simulates the second one, this time also preserving who has which fork(s).

- with "\(;\)" it is possible to give a process \(E\) such that the finite traces of \(E\) form a non-regular language, e.g., \(M = \{~\mathtt{a}^n\mathtt{b}^n~|~n\in\mathbb{N}~\}\). (This is the easy bit.)
- without "\(;\)" it is possible to give an inductive translation \(t\) from CSP expressions to \(\epsilon\)-NFAs (or right-linear grammars) such that the translation preserves the set of finite traces, i.e., the set of finite traces of a CSP expression \(E\) is equal to the (regular) language \(L(t(E))\). (This could be harder.)

- slides on LTL borrowed from COMP3151 (see lecture03a.pdf and lecture04a.pdf)
- Harel's Statecharts in the Making: A Personal Account, yakindu statechart tools; example code
- Promela/spin: spinroot.com; example code
- Lamport's Temporal Logic of Actions: TLA; example code

- J. A. Goguen and J. Meseguer Security policies and security models. S&P 1982
- P. Y. A. Ryan, S. A. Schneider Process Algebra and Non-Interference Journal of Computer Security 9(1/2): 75-103 (2001). (That link goes to an earlier version I believe)
- G. Smith Recent developments in quantitative information flow (invited tutorial). LICS 2015

- 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.
- Suppose our propositions are \(\{a,b,c\}\). Give an LTL formula for each of the following requirements.
- \(a\) and \(b\) are never true at the same time
- every \(a\) is followed by a \(b\) (which is short for: whenever \(a\) is true there is a later time where \(b\) is true)
- no \(b\) occurs without an \(a\) having occurred already
- 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\).

- 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