Homework (Week 1) Term 2, 2021 Announcements Course Outline Course Schedule Ed Forum Glossary Maths Resources Moodle - Lecture Recordings 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 Thursday Slides Condensed Thursday Slides Wednesday Slides Condensed Wednesday Slides Week 2 Homework Thursday Code Thursday Notes Thursday Slides Condensed Thursday Slides Wednesday Code Week 3 Homework Promela Code Thursday Code Thursday Slides Condensed Thursday Slides Wednesday Slides Condensed Wednesday Slides Week 4 Homework Thursday Code Thursday Slides Condensed Thursday Slides Wednesday Code and Notes Wednesday Slides Condensed Wednesday Slides Week 5 Homework Thursday Slides Condensed Thursday Slides Wednesday Code and Notes Wednesday Slides Condensed Wednesday Slides Week 7 Homework Thursday Notes Thursday Slides Condensed Thursday Slides Wednesday Notes Wednesday Slides Condensed Wednesday Slides Week 8 Homework Thursday Slides Condensed Thursday Slides Wednesday Code Wednesday Slides Condensed Wednesday Slides Week 9 Homework Thursday Notes Thursday Slides Wednesday Notes Wednesday Slides Condensed Wednesday Slides Week 10 Old Exams Thursday Slides Wednesday Notes Wednesday Slides Old Exam Papers final05s2 final06s2 final07s2 final08s2 final09s2 final10s2 final11s2 final13s2 final14s2 final17s2 Homework (Week 1) Table of Contents 1. Circularity (1 mark) 2. Dining Cryptographers (2 marks) 3. Safety and Liveness (5 marks) 3.1. Characterisation 3.2. Topological Interpretation 3.3. Bonus Question 4. Temporal Logic (5 marks) 4.1. Examples 4.2. Proof Submission: Due on Thursday, 10th of June, 4pm 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 Circularity (1 mark) What is the answer to this question? Hint: You will find the answer to this question on Ed. If you can't access Ed yet, see the Announcements page for instructions. 2 Dining Cryptographers (2 marks) Assume the setting described in the first lecture for the problem of the Dining Cryptographers. Suppose there are four cryptographers. At the end, how do we know if the NSA paid or not? Is confidentiality preserved? 3 Safety and Liveness (5 marks) 3.1 Characterisation Suppose someone has written down a property \(P\), but obnoxiously, they won't tell you what it is. However, you know that it is either a safety property or a liveness property. Furthermore, suppose that after you show them the first 1000 states of a behaviour \(\sigma\), they exclaim one of the following: \(\sigma\) satisfies \(P\)! \(\sigma\) violates \(P\)! It's too early to say whether \(\sigma\) satisfies \(P\) or not! For each of the above exclamations, do we learn what kind of property \(P\) is? Why? Bonus question (not for marks): if we drop the assumption that \(P\) is either a safety property or a liveness property, then what do we learn? 3.2 Topological Interpretation Let \(\Sigma = \{a,b\}\). That is, we assume there are only two states, \(a\) and \(b\). Consider the property \(P = \{\sigma | \sigma \mbox{ contains exactly one } b\}\). Use Alpern and Schneider's theorem to decompose \(P\) into a safety property \(P_S\) and a liveness property \(P_L\). Simplify them; that is, don't just say \(P_L = \Sigma^\omega \backslash (\overline{P} \backslash P)\) but give something that explains what \(P_L\) is. Assume \(P\) is a safety property. Prove that \(\Sigma^\omega \backslash (\overline{P} \backslash P) = \Sigma^\omega\) using the algebraic laws of set operations. Is the empty property \(\emptyset\) a liveness property? Is it a safety property? Prove or disprove. 3.3 Bonus Question This question is not for marks, but for a meaningless brownie point 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. 4 Temporal Logic (5 marks) 4.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. The dragon was never slain, but the princess lived happily until she didn't. The dragon was slain at least twice. The dragon was slain at most once. Whenever the dragon was slain, the princess did not live happily. 4.2 Proof Prove the following logical statements: \begin{array}{rcl} \Box\Box \varphi & \Leftrightarrow & \Box \varphi \\ \Diamond\Diamond \varphi & \Leftrightarrow & \Diamond \varphi \\ \Box \varphi & \Rightarrow & \Diamond \varphi \\ \Diamond\Box \varphi & \Rightarrow & \Box\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 use previously proven identities (both in this question and in lectures) to prove new ones. Note that two temporal logic formulas \(\phi\) and \(\psi\) are logically equivalent, written \(\varphi \Leftrightarrow \psi\), iff for all behaviours \(\sigma\) it holds that: \[ \sigma \models \varphi \mbox{ if and only if } \sigma \models \psi \] 2021-08-05 tor 15:45 Announcements RSS
