COMP3151/9154 Homework 1

Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

COMP3151/9154

Homework (Week 1) (corrected)

Due: 9:00 am Mon 5 June 2023

Submission: 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 a few pages. See the course Moodle page for the submission location. Late submissions will not be accepted. Solutions to this homework will be discussed in the tutorial immediately following the due date, and your participation mark will depend on your ability to present your answer if called upon in the tutorial.

1. Dining Cryptographers: If we denote the variables of the protocol by (for i = 0, 1, 2) the boolean variables ci for cryptographer i’s coin toss, pi for whether or not cryptographer i paid, then cryptographer i’s public announcement ai is pi ⊕ ci ⊕ ci−1 mod 3

We showed the correctness of the Dining Cryptographers protocol in lec-tures, by demonstrating that a0 ⊕ a1 ⊕ a2 = p0 ⊕ p1 ⊕ p2. 1 Noting that at most one of the pi is equal to 1, this expression expresses whether or not one of the cryptographers paid for the dinner.

Note that cryptographer i sees only the following variables:

pi , ci , c(i−1 mod 3), a0, a1, a2.

Consider a scenario where cryptographer 0 paid — call this the “real world”. Consider cryptographer 2. Show the security of the protocol, by demonstrating that at the end of the protocol, cryptographer 2 cannot deduce from their observations whether cryptographer 0 paid or whether cryptographer 1 paid. That is, there exist two scenarios (in which at most one of the cryptographers paid) in which cryptographer 2’s variables have exactly the same values as in the real world, but in which p0 = 1 in one scenario and p1 = 1 in the other.

2. Safety and Liveness: Let s be a state, and let s ω denote the behaviour ssssssssssss . . . (i.e. infinitely many repetitions of s.)

Give an example of a set A such that s ω ∈ A, but s ω /∈ A.

3. Alpern and Schneider’s theorem: Alpern and Schneider’s theorem states that any property P is the intersection of a safety property PS and a liveness property PL. In the following, state concretely what these properties are. (Don’t just restate the theorem, give expressions for these sets that are as simple as possible!)

(a) What are PS, PL when P is a safety property?

(b) What are PS, PL when P is a liveness property?

(c) Let Σ = {a, b}. That is, we assume there are only two states, a and b. Consider the property P = {σ|σ contains exactly one b}. What are PS and PL?

(d) Is the empty property ∅ a liveness property? Is it a safety property? Explain.

4. Temporal Logic

Define suitable predicate symbols and give LTL formalisations for the following properties (assume that there is one state per day):

(a) Once the dragon is slain, the princess will live happily ever after.

(b) The dragon will never be slain, and the princess will live happily until she becomes sad.

(c) The dragon will be slain at least twice.

(d) The dragon will be slain at most once.

(e) On any day that the dragon is slain, the princess will be sad, but she will eventually become happy again.

5. Prove the following logical statements:

□ ⃝ φ ⇔ ⃝□φ

ϕ U ψ

⇔ ψ ∨ (ϕ ∧ ⃝(ϕ U ψ))

♢♢φ ⇔ ♢φ

It may help to use these semantic definitions for □ and ♢ (derivable from the definition in terms of U):

σ |= ♢φ iff ∃i ≥ 0. (σ|i |= φ)

σ |= □φ iff ∀i ≥ 0. (σ|i |= φ)

You may use previously proven identities (both in this question and in lectures) to prove new ones.

Note that two temporal logic formulas ϕ and ψ are logically equivalent, written φ ⇔ ψ, iff for all behaviours σ it holds that:

σ |= φ if and only if σ |= ψ

General remark: For any proofs you submit: feel free to use any well known laws about propositional logic, predicate logic or set theory without proof (e.g., the de Morgan laws).