Homework (Week 1) Term 2, 2020 Announcements Course Outline Course Schedule Glossary Maths Resources Moodle - BB Collab Piazza Forum Assignment 0 Spec TeX Guide Web Submission Assignment 1 Spec TeX Guide Web Submission Assignment 2 Spec Web Submission Java Resources Monitors Video Multithreading Video Semaphores Video Volatile Video Web Tutorials Week 1 Homework Monday Board Recording Slides Condensed Slides Thursday Code Slides Condensed Slides Week 2 Homework Thursday Slides Condensed Slides Week 3 Homework Monday Brownies Promela Samples Slides Condensed Slides Thursday Code Slides Condensed Slides Week 4 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 5 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 7 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 8 Homework Monday Slides Thursday Slides Week 9 Homework Monday Slides Thursday Slides Week 10 Notes Homework (Week 1) Table of Contents 1. Dining Cryptographers 2. Safety and Liveness 2.1. Characterisation 2.2. Topological Interpretation 2.3. Bonus Question 3. Temporal Logic 3.1. Examples 3.2. Proof Submission: Due on Thursday, 11th of June, 6pm Sydney Time. Please submit using the CSE Give System either online or via this command on a CSE terminal: give cs3151 hw1 hw1.pdf
Please put all your answers in one PDF file called hw1.pdf. Use of LaTeX is encouraged but not required. Please make your answers as concise as possible. This homework should not be more than two pages, and preferably no more than one. 1 Dining Cryptographers Assume the setting described in the first lecture for the problem of the Dining Cryptographers. Now assume payment of (a) pre-dinner drinks and (b) the dinner itself is organised separately. Can the 3 coin flips for (a) be re-used for (b)? No, because confidentiality is violated. As an example, suppose the NSA paid for the drinks in the first round, and one of them paid in the second round. Whichever of them changes their answer from the first to the second round paid in the second round, which is observable to the other philosophers. 2 Safety and Liveness 2.1 Characterisation Are the following properties safety or liveness? Once process \(p\) has executed statement 5 then process \(q\) must execute statement 17 again. Once process \(p\) has executed statement 5 then process \(q\) cannot execute statement 17 again. Process \(q\) cannot execute statement 17 again unless process \(p\) executes statement 5 first. Process \(p\) has to execute statement 5 before \(q\) can execute statement 17 again. If you require that \(q\) must execute immediately, safety, otherwise liveness. Safety. Safety. Safety. 2.2 Topological Interpretation Is the empty property (\(\emptyset\)): a safety property? a liveness property? Prove or disprove. Recall that safety properties are limit closed (i.e. \(\overline{S} = S\)) and liveness properties are dense (\(\overline{S} = \Sigma^\omega\)). Note that \(\overline{\emptyset} = \emptyset\). Therefore it is a safety property, and not a liveness property. Is the universal property (\(\Sigma^\omega\)): a safety property? a liveness property? Prove or disprove. Recall that safety properties are limit closed (i.e. \(\overline{S} = S\)) and liveness properties are dense (\(\overline{S} = \Sigma^\omega\)). Note that \(\overline{\Sigma^\omega} = \Sigma^\omega\). Therefore it is the only property that is both a safety property and a liveness property. 2.3 Bonus Question This question is not for marks, but for a meaningless brownie point which will earn you a place in the Concurrency Hall of Champions Assuming there are at least two distinct states \(a\) and \(b\), prove that any property \(P\) is the intersection of two liveness properties. Hint: It is helpful to note that the union of a dense set and any set is itself dense. Let \(A\) and \(B\) be the properties defined as: \[A = \{\ wa^\omega\ |\ w \in \Sigma^\ast\ \}\] \[B = \{\ wb^\omega\ |\ w \in \Sigma^\ast\ \}\] Observe that \(\overline{A}\) and \(\overline{B}\) are both \(\Sigma^\omega\), and are therefore liveness properties. And, as all behaviours in \(A\) end in \(a^\omega\) and all behaviours in \(B\) end in \(b^\omega\), \(A \cap B = \emptyset\). Because the union of a dense set and another set is dense (as \(\overline{A} \subseteq \overline{A}\)), we know that our arbitrary property \(P\) union \(A\) is a liveness property (resp. \(B\)). Then we show: \begin{array}{lclr} P & = & (P \cup A) \cap (P \cup B) \\ & = & (P \cap (P \cup B)) \cup (A \cap (P \cup B)) & \text{distrib} \\ & = & P \cup (A \cap (P \cup B)) & \text{absorb} \\ & = & P \cup (A \cap P) \cup (A \cap B) & \text{distrib} \\ & = & P \cup (A \cap P) \cup \emptyset & \text{from above} \\ & = & P \cup (A \cap P) & \text{identity} \\ & = & P & \text{absorb} \\ \end{array} Therefore, any property \(P\) is the intersection of the two liveness properties \(P \cup A\) and \(P \cup B\). 3 Temporal Logic 3.1 Examples Define suitable predicate symbols and give LTL formalisations for the following properties: Once the dragon was slain, the princess lived happily ever after. If she returns before midnight, all will be well. If might happen again, but not after that. It will not happen again. It will never happen. The contestant was beaten repeatedly until he gave up. If at first you don't succeed, try, try again. Remain seated until the exam comes to a complete halt. Solutions may vary, but mine were: \(\neg\text{slain}\ \mathcal{U}\ (\text{slain}\land\Box\text{happy})\) \((\text{before0}\land\text{before0}\ \mathcal{U}\ \neg\text{before0}) \land \Box(\text{return}\land\text{before0}\Rightarrow\text{well})\) \(\Box(\text{happen} \Rightarrow \bigcirc\Box\neg\text{happen})\) \(\bigcirc\Box\neg\text{happen}\) (circle optional) \(\Box\neg\text{happen}\) \(\text{beaten}\ \mathcal{U}\ \text{gaveUp}\) \(\text{fail} \Rightarrow \bigcirc (\text{try}\land(\text{fail}\Rightarrow\bigcirc\text{try}))\) \(\text{sit}\ \mathcal{U}\ \text{examOver}\) 3.2 Proof Prove the following logical identities: \begin{array}{rcl} \Box\Box \varphi & \Leftrightarrow & \Box \varphi \\ \Diamond\Diamond \varphi & \Leftrightarrow & \Diamond \varphi \\ \Diamond\Box\Diamond\varphi & \Leftrightarrow & \Box\Diamond\varphi \\ \Box\Diamond\Box\varphi & \Leftrightarrow & \Diamond\Box\varphi \\ \end{array} It may help to use these semantic definitions for \(\Box\) and \(\Diamond\) (derivable from the definition in terms of \(\mathcal{U}\)): \begin{array}{rcl} \sigma \models \Diamond\varphi & \text{iff} & \exists i \geq 0.\ (\sigma|_i \models \varphi) \\ \sigma \models \Box\varphi & \text{iff} & \forall i \geq 0.\ (\sigma|_i \models \varphi) \end{array} You may (and are encouraged) to use previously proven identities (both in this question and in lectures) to prove new ones. \begin{array}{lcl} \sigma \models \Box\Box\varphi &\Leftrightarrow & \forall i.\ \sigma|_i \models \Box\varphi \\ & \Leftrightarrow & \forall i.\ \forall j.\ \sigma|_i|_j \models \varphi \\ & \Leftrightarrow & \forall i.\ \forall j.\ \sigma|_{i+j} \models \varphi \\ & \Leftrightarrow & \forall k.\ \sigma|_k \models \varphi \\ & \Leftrightarrow & \sigma \models \Box \varphi \\ \end{array} The next is proved as a consequence of the first. \begin{array}{lcl} \Diamond\Diamond\varphi & \Leftrightarrow & \Diamond\Diamond\neg\neg\varphi\\ & \Leftrightarrow & \Diamond\neg\Box\neg\varphi\\ & \Leftrightarrow & \neg\Box\Box\neg\varphi\\ & \Leftrightarrow & \neg\Box\neg\varphi\\ & \Leftrightarrow & \neg\neg\Diamond\varphi\\ & \Leftrightarrow & \Diamond\varphi \end{array} We prove each direction of the next one separately: \begin{array}{lcl} \sigma \models \Diamond\Box\Diamond\varphi & \Leftrightarrow & \exists i.\ \forall j.\ \exists k.\ \sigma|_{i+j+k} \models \varphi \\ & \Rightarrow & \forall j.\ \exists \ell.\ \sigma_{i+\ell} \models \varphi \\ & \Leftrightarrow & \sigma \models \Box\Diamond\varphi\\ \sigma \models \Box\Diamond\varphi & \Rightarrow & \exists i.\ \sigma|_i \models \Box\Diamond\varphi \\ & \Leftrightarrow & \sigma \models \Diamond\Box\Diamond\varphi \end{array} And this is proved as a consequence: \begin{array}{lcl} \Box\Diamond\Box\varphi & \Leftrightarrow & \Box\Diamond\Box\neg\neg\varphi\\ & \Leftrightarrow & \Box\Diamond\neg\Diamond\neg\varphi\\ & \Leftrightarrow & \Box\neg\Box\Diamond\neg\varphi\\ & \Leftrightarrow & \neg\Diamond\Box\Diamond\neg\varphi\\ & \Leftrightarrow & \neg\Box\Diamond\neg\varphi\\ & \Leftrightarrow & \neg\Box\neg\Box\varphi\\ & \Leftrightarrow & \neg\neg\Diamond\Box\varphi\\ & \Leftrightarrow & \Diamond\Box\varphi\\ \end{array} 2020-08-06 Thu 03:32 Announcements RSS
