Homework 1, Wednesday 2-3-2016

  1. A binary relation ~ on a set D is an equivalence relation if it is
    1. Give an example of an equivalence relation on the domain of all people.
    2. Give 2 examples of a relation on people that is not an equivalence relation because exactly one of the three requirements above fails. Which one?
    3. If ~ is an equivalence relation on D, and p is in D, then [p]~ denotes the set of all processes in D that are equivalent to p. Such a set is called an equivalence class. Show (formally, by means of a mathematical proof) that the collection of all equivalence classes form a partitioning of D. This means that every p in D belongs to one and only one equivalence class.
    [None of this has been treated in class; (c) is a test of prior mathematical exposure to the notion of a mathematical proof. If this is hard, it is a good warm-up for bits of mathematical proof yet to come.]
  2. Consider a vending machine that accept pieces of 20 cents, 50 cents and 1 dollar, and that can dispense chocolate and pretzels, each of which costs 1 dollar. Draw an LTS whose transaction are labelled with "20c", "50c" or "$\$$1", indicating the reception by the machine of a coin inserted by a user, and by the actions "chocolate" or "pretzel", indicating the opening of the glass door of the machine behind which chocolate or pretzels are stored. (We abstract from the closing of the door after extraction of the pretzel, which happens automatically, and the appearance of a new pretzel behind the glass door afterwards.) You may assume that the machine does not give change, and that it accepts any amount surplus money; alternatively you may assume that the opening for inserting coins will close after $1 or more has been inserted.
  3. Draw a process graph for the ACP expression a(bc+b(c+d)).
  4. Look at the definition given in the notes of the choice operator (+) of ACP in terms of LTSs. An alternative definition could be obtained by "identifying" the states IG and IH, i.e. by merging them together into one state. Is there any difference between this approach and the one of the notes? If so, illustrate this by means of examples, and tell which definition you prefer.
  5. Give a formal definition of the sequential composition operator of ACP (see notes), in the style of the notes.

Homework 2, Wednesday 9-3-2016

Due Monday 14 March at 4pm; if you can, please submit it by email to me.
  1. Let P be the process given by the recursive equation X = a.(b.X + c.X)
    and Q be the process (c+e).a. Assume an ACP communication function γ given by γ(a,c)=γ(c,a)=d.
    1. Draw a process graph representation of P and Q.
    2. Draw a process graph representation of P||Q.
    3. Draw a process graph representation of {a,c}(P||Q).
  2. Show, for labelled transition systems without termination predicate, that bisimulation equivalence is strictly finer than completed trace equivalence. This means that it makes strictly fewer identifications. This involves two things:
  3. Out of the following processes, which pairs are weak bisimulation equivalent? Show the bisimulation or informally describe why there isn't any.
    a.(b+τ.c)+τ.a.d a.(b+τ.c)+τ.a.d+a.b a.(b+τ.c)+τ.a.d+a.c a.(b+τ.c)+τ.a.d+a.d
    Also tell which pairs are weak completed trace equivalent, and why or why not. And which pairs are strong completed trace equivalent, and why or why not.
  4. Consider a process called "gatekeeper" that makes sure that of 2 other processes "1" and "2", at most one is in its critical section. Its action are "hear request of process i to enter critical section", or h(i) for short; "admit process i into critical section", or a(i); and "observe that process i exits the critical section", e(i). Here i can have the values 1 or 2. Keep in mind that each of the processes i may enter the critical section multiple times. The actions h(i), a(i) and e(i) all synchronise with corresponding actions h(i), a(i) and e(i) from the processes 1 and 2. The gatekeeper should be able to hear a request in any state, subject to the restriction that each process will request entry in the critical section only once, until it has entered and exited the critical section.
    1. Draw a process graph describing the correct behaviour of the gatekeeper.
    2. Express the behaviour of the gatekeeper by a system of recursive equations.
    You are not asked to specify the processes "1" and "2" themselves.

Homework 3, Wednesday 16-3-2016

Due Monday 21 March at 4pm; if you can, please submit it by email to Peter Höfner (peter.hoefner < at > nicta.com.au).
  1. Consider the vending machine discussed during the lecture:
    Ven = 50c.Venb + 20c.Venl
    Venb = big.collectb.Ven
    Venl = little.collectl.Ven
  2. Do the following properties hold? If yes, provide a proof, if no give a counter-example.
    1. Ven ⊨ [50c]([-{big}]false ∧<-{little,50c}>true)
    2. Ven ⊨ [50c,20c](<big>true ∧<little>true)
  3. Let Cl = tick.Cl and Cl2 = tick.tick.Cl2. Show that no modal formula distinguishes these clocks.
  4. Two modal formulas Φ and Ψ are equivalent if, for all processes E, E ⊨ Φ iff E ⊨ Ψ. Are the following pairs of formulas equivalent? (Proof/Counterexample)
    1. <tick>(Φ1Φ2),      <tick>Φ1∧<tick>Φ2
    2. [tick](Φ1Φ2),      [tick]Φ1∧[tick]Φ2
    3. <tick>(Φ1Φ2),      <tick>Φ1∨<tick>Φ2
    4. [tick](Φ1Φ2),      [tick]Φ1∨[tick]Φ2
  5. Consider the following transition system.

    The following atomic propositions are used: red, yellow, green, and black. The model is intended to describe a traffic light that is able to blink yellow. Determine for each of the following CTL formulas the set of states for which these formulas hold:
    1. AF yellow
    2. AG yellow
    3. AG(EF yellow)
    4. AF green
    5. EF green
    6. EG ¬green
    7. A (¬ black) Until (EF black)
    8. A (green) Until (A yellow Until red)

    This exercise is taken from Bayer/Katoen "Principles of Model Checking"

Wednesday 23-3-2016 to Thursday 7-4-2016 (by K. Engelhardt)

See this page.

Homework 6, Wednesday 13-4-2016

  1. Describe the relay race in CCS in a similar way that the class notes describe it in ACP.
  2. Give an example of a process that satisfies the HML formulas [a]⟨b⟩T and ⟨a⟩([b]⟨c⟩T) but does not satisfy [a]⟨b⟩⟨c⟩T.
  3. Show that weak completed trace equivalence is a congruence for the abstraction operator. This means that whenever P =WCT Q and I is any set of actions, it must be the case that τI(P) =WCT τI(Q).
  4. An equivalence ~ is a congruence for a language L if P ~ Q implies that C[P] ~ C[Q] for every context C[ ]. Here a context C[ ] is an L-expression with a hole in it, and C[P] is the result of plugging in P for the hole. The congruence closure ~L of ~ is defined by

    P ~L Q if and only if C[P] ~ C[Q] for any L-context C[ ].

    Prove that ~L is the coarsest congruence finer than ~.
  5. Sequencing is a binary operation defined on any process graphs; it starts with its second component as soon as its first component cannot do any further actions.
    Sequential composition, on the other hand, is defined on process graphs equipped with a state-labelling, where some states are marked with the symbol for successful termination, ✔. Here the second component starts only when the first one successfully terminates.
    1. Give a definition of sequencing as an operator on process graphs.
    2. Give an example that shows the difference between these two operators.
    3. Is (strong) partial trace equivalence a congruence for sequencing? Show why your answer is correct.
    4. Is completed trace equivalence a congruence for sequencing? Show why your answer is correct.
    5. Is weak bisimulation equivalence a congruence for sequencing? Show why your answer is correct.

Homework 7, Wednesday 20-4-2016

Due to ANZAC day there is no tutorial on April 25. Please try to submit the HW by email by Tuesday morning, so that I can correct it by Wednesday.
  1. Model the relay race in CSP.
  2. How would you translate the CSP expressions (ab) ⊓ c and (ab) ☐ c into CCS? Here I omitted trailing .0's.
  3. Consider the processes a.0 + b.0, τ.(a.0 + b.0), τ.a.0 + b.0, a.τ.0 + b.0 and τ.(a.0 + b.0) + a.0.
    1. Which of these processes are weak bisimulation equivalent to each other, and why (or why not)?
    2. Which of these processes are branching bisimulation equivalent to each other, and why (or why not)?
    3. Which of these processes are rooted weak bisimulation equivalent to each other, and why (or why not)?
    4. Which of these processes are rooted branching bisimulation equivalent to each other, and why (or why not)?
  4. Rooted Weak Bisimilarity =RWB is an explicit characterisation of =WBC, in the sense that there is a constructive method to show P =RWB Q and from that it follows that P =WBC Q. Can you find an explicit characterisation of the congruence closure of =WCT for the CCS +-operator only (so for the coarsest congruence for + that is contained in weak completed trace equivalence)?
  5. Prove that any weak bisimulation equivalence classes consists of at most two rooted weak bisimulation equivalence classes (one of which contains processes P that can do a τ-transition to a process that is weakly bisimilar with P). Is it exactly two, or can you find an example of a weak bisimulation equivalence class that contains only one rooted weak bisimulation equivalence class?

Homework 8, Wednesday 27-4-2016

  1. Use the partition refinement algorithm on the states of a.(a(a+aa)+aa)+aaa. Show the steps. With how many bisimulation equivalence classes do you end up?
  2. Draw the graph of τ.(τ.(a+τ)+τ.a)+τ.(τ(a+τ)+a). Colour the states, such that two states are branching bisimilar iff they have the same colour. Provide a branching bisimilar process graph with as few states as possible.
  3. Let Δ be the operator on processes that prepends a τ-loop at the beginning of its argument process. So a.Δb is a process with three states, one transition labelled a, one transition labelled b, and a τ-loop in the middle state.
    1. Give a structural operational semantics for this operator.
    2. Is this operator compositional for weak completed trace equivalence? Why, or why not?
    3. Is this operator compositional for strong bisimilarity? Why, or why not?
  4. Now I use the following names:
    normal progressfora.b.0
    fair divergencefora.Δb.0
    livelockfora.(b.0+ τ.Δ.0)
    deadlockfora.(b.0 + τ.0)
    These correspond with the four pictures drawn in class.

    Modify the definition of weak completed trace semantics in six different ways, namely such that

    1. deadlock = livelock and fair divergence = progress,
    2. fair divergence = progress, and livelock differs from deadlock and from progress,
    3. deadlock = livelock and fair divergence differs from livelock and from progress,
    4. livelock = fair divergence, different from deadlock and progress,
    5. deadlock = livelock = fair divergence, different from progress,
    6. all four phenomena are distinguished.
    In all cases deadlock should be distinguished from normal progress. Your notions of weak completed trace equivalence should all be strictly finer than partial trace equivalence, and strictly coarser than strong bisimilarity. Also, the definitions should be such that upon restricting attention to τ-free processes, they coincide with a known concept of strong completed trace equivalence. They should also be congruences for abstraction (τI); no need to prove this.
  5. Turn the processes graphs of the 3 processes a.b.Δ0, a.Δb.Δ0 and a.(b.Δ0+ τ.Δ.0) from edge-labelled transition systems into state-labelled transition systems (also known as Kripke structures) by labelling each state s by one of the atomic propositions ε, a or ab, indicating the sequence of visible actions on a path reaching s (from the initial state). Now find formulas in LTL or CTL that distinguish the first three of these processes, i.e. there should be formula that holds for "fair divergence" but not for "livelock"; etc.

Homework 9, Wednesday 4-5-2016

  1. In the paper available at http://www.cse.unsw.edu.au/~rvg/pub/spectrum1.ps.gz there are a number of pictures, called Counterexample 1, 2, 3, etc.
    A (bad) pdf of the paper is here.
    1. For each of counterexamples 2, 3, 4, 5, 8, 14, 15, provide a HML formula (if needed with infinite conjunctions) that holds for the left process, but not for the right one.
    2. If possible give a denial formula that holds for one of the processes but for for the other, or show that there is no such formula.
  2. Just like weak bisimulation equivalence, =WB, branching bisimulation equivalence, =BB, fails to be a congruence for the + operator. Namely, we have τ.a =BB a but not τ.a + d =BB a + d. Let branching bisimulation congruence =RBB be the coarsest congruence relation (for the +) that is finer than =BB. We have seen that each =WB-equivalence class of processes contains exactly two =RWB-equivalence classes. Show, by means of an example, that it is not the case that each =BB-equivalence class of processes contains exactly two =RBB-equivalence classes.
  3. (Strong) completed trace equivalence $=_{CT}$ is not a congruence for the parallel composition $\|_S$ of CSP.
    1. Show this.
    2. Let $=_{CTC}^\|$ be the coarsest congruence for $\|_S$ contained in (= finer than) $=_{CT}$. And let ~ be an arbitrary congruence for all GSOS operators that is finer than partial trace equivalence. How are $=_{CTC}^\|$ and ~ related (i.e. which one is coarser), possibly depending on the choice of ~? Give a convincing explanation for your answer.
  4. Give a specification in ACP, CCS or CSP of a FIFO queue that can hold up to three bits of data. Each bit can be a 0 or a 1. The actions of the queue should be in(0), in(1), out(0) and in(1). The actions in(0), in(1) are always possible, unless the queue is full. The actions out(0) and in(1) are only possible if the oldest bit in the queue is a 0 or 1, respectively.
  5. A preorder is a relation that is transitive and reflexive. So an equivalence relation is a preorder that moreover is symmetric. A partial order is a preorder $\leq$ that is antisymmetric:
    if $x \leq y$ and $y \leq x$ then $x=y$.
    1. Give an example of a partial order.
    2. Give an example of a preorder that is neither a partial order nor a equivalence relation.
    3. Given examples of the above two kinds that have occurred in this course.

Homework 10, Wednesday 11-5-2016

  1. Give a Petri net for the following CCS expressions:
    1. $a.(b.0 + c.0)$
    2. $a.(b.0 + (c.0|\bar c.d.0))$
    3. $(a.(b.0 + a.0)) | a.\bar a.b.0$
    4. a.0+X where X is given by the recursive equation X=a.X.
  2. Let's define a step-trace of a Petri net to be sequence, not of actions, but of multisets of actions, such that the represented system can perform the sequence in succession, at each step performing the required multiset of actions simultaneously. (If you don't know what a multiset is, just think of it as a set.) For example, the process a(b + (c||d)) would have the following completed step-traces:

    {ab, acd, adc, a[cd]}

    Here [cd] denotes the multiset containing c and d one time each.
    1. Give the set of completed step traces of a(b + c) || d
    2. Give an example of two processes that are strong bisimulation equivalent but have different step-traces.
    3. Give an example of two processes that are strong bisimulation equivalent but have different minimal running times when associating durations to actions. Here durations are allocated by a function from the set of all actions to the positive real numbers. For instance duration(a)=1 and duration(b)=2. Now all occurrences of the action b will take 2 time units. You may choose any function duration that works for you. Explain why the minimal running times will be different.
    4. Show that strong bisimilarity is not preserved under action refinement. That is, give two processes that are strongly bisimilar, such that after replacing each copy of a single action a with a more complicated process (like a1;a2) they are no longer strongly bisimilar.
    5. Give an example of two processes that have the same completed step traces, but have different minimal running times when associating durations to actions. Explain why the minimal running times will be different.
    6. Use the same example to argue that completed step trace equivalence is not preserved under action refinement. That is, give two processes with the same completed step traces, such that after replacing each copy of a single action a with a more complicated process (like a1;a2) they are no longer completed step trace equivalent.
  3. Here you find a labelled transition system. The labels are σ, E1, L1, E2, and L2, and the labels of all other (unlabelled) transitions are τ. Apply the partition refinement algorithm for branching bisimulation to partition the states of this graph until two nodes are in the same block iff they are branching bisimulation equivalent. Tell which splitters you used (in order).

Homework 11, Wednesday 18-5-2016 (given already on Monday 16-5)

To be found here. And here is an extra exercise that has nothing to do with mutual exclusion:
  1. Let Δ be the operator on processes that prepends a τ-loop at the beginning of its argument process. So a.Δb is a process with three states, one transition labelled a, one transition labelled b, and a τ-loop in the middle state.
    1. Compare the processes a.Δ(b+τ.Δ(c+τ.Δ(c+d))) and a.Δ(b+τ.Δ(c+τ.(c+d))) and a.Δ(b+τ.(c+τ.Δ(c+d))) and a.(b+τ.Δ(c+τ.Δ(c+d))). Which of these processes are rooted branching bisimulation equivalent to each other? Show bisimilarity by means of a consistent colouring.
    2. Which pairs of the above four processes are rooted branching bisimulation equivalent with explicit divergence? Show bisimilarity by means of a consistent colouring.
    3. Give three equational laws involving this operator that are valid for rooted branching bisimilarity with explicit divergence, but do not follow from any valid laws for without such an operator, nor from each other. (Do not get three different laws by making one law unnecessarily specific.) (An example of a law could be $a.\Delta x = a (\Delta x + \tau.x)$, but this one is not valid; it fails when substituting $b$ for $x$, because any branching bisimulation would need to relate a state with an internal divergence to a state that has no internal divergence. The law $a.\Delta x = a.(\Delta x + \Delta x)$ would be valid, but it doesn't count, because it is an instance of the valid law $a.x = a.(x+x)$, or even $x = x+x$.)

Homework 12, Wednesday 25-5-2016

  1. Give a simple algorithm A that transforms process graphs G into A(G), such that A(G) and A(H) are rooted branching bisimulation equivalent if and only if G and H are branching bisimulation equivalent.
  2. Consider a process with the following set of completed step traces: $\{bad,[ab]d,abd,a[bd],adb,acd,a[cd],adc\}$. Thus, in each run, the actions a, d and one out of c or b occur once each, subject to the following restrictions:
    • b and c can never occur in the same trace.
    • if c happens, it must be after a, and
    • a happens before d.
    1. Provide a Petri net with the above set of completed step traces.
    2. What are the completed partial ordered traces of your net?
    3. Give a CSP expression for this process that uses at most one occurrence of a choice operator (☐ or ⊓).
    4. Give an ACP expression for this process that uses at most one +.
    5. Give a CCS expression for this process that uses at most one +. You may have to smuggle in an internal action τ to make this possible.
  3. Consider again the four processes that figure in Question 11 of last week's homework:
    a.Δ(b+τ.Δ(c+τ.Δ(c+d))) and a.Δ(b+τ.Δ(c+τ.(c+d))) and a.Δ(b+τ.(c+τ.Δ(c+d))) and a.(b+τ.Δ(c+τ.Δ(c+d))).
    1. For each pair of them give a CTL-formula not using the next state operator (X) that holds for one but not the other. (Or explain why such a formula does not exists.)
    2. Same question for LTL-formulas not using the next state operator.
  4. The remaining questions centre around the process graph given here. It is the graph of Peterson's famous mutual exclusion algorithm, which you encountered already in Homework 11. The gray shadows represent copies of the transitions at the opposite end of the diagram, so the transitions on the far right and bottom can be considered to loop around. The name of a state $\ell_vim_jT$ where $T$ is $A$ or $B$ indicates that process $A$ is in state $\ell_i$, process $B$ in state $m_i$ and the variable $turn$ has value $T$. The actions nA, cA, nB and cB are visible: they represent the non-critical and critical sections of processes A and B in Peterson's protocol. All unlabelled transitions are $\tau$'s.
    1. How many reachable states are in the process graph after identifying strongly bisimilar states? Tell or show which states get identified (for instance by drawing lines between equivalence classes on the sheet with the graph). (The most secure way to figure this out is by using the partition refinement algorithm, or reasoning in the spirit of that algorithm.)
    2. How many reachable states are there after identifying branching bisimilar states? In other words: what is the least amount of colours needed in a consistent colouring of this graph? Tell or show which states get identified.
  5. In this question we interpret the same graph as a Kripke structure---we forget the transition labels. We have an atomic proposition IntentA, saying that Process A has expressed its intention to enter the critical section (by executing the instruction readyA:=true), but has not done so yet. It holds whenever Process A is in states $\ell_3$ or $\ell_4$. We also have an atomic proposition CritA, stating that Process A is about to enter its critical section; it holds in state $\ell_5$ only. Likewise we have atomic propositions IntentB and CritB. (An alternative approach would be to let IntentA hold in states $\ell_3$, $\ell_4$ and $\ell_5$, with CritA, stating that Process A is in the critical section, holding in a new state that is halfway $\ell_5$ and $\ell_6$. This would work equally well.)

    The purpose of the algorithm is to ensure that Processes $A$ and $B$ are never simultaneously in the critical section, and to guarantee that both processes keep making progress. It is correct if these requirements are met.

    1. Formulate an LTL property in terms of these four atomic propositions (or others if needed) expressing the correctness of Peterson's algorithm.
    2. (harder) Formulate an LTL property saying that if Process $A$ intends to go critical, then Process $B$ will enter its critical section at most once before $A$ does.
    3. Does this property hold for Peterson's algorithm? Explain.

Rob van Glabbeek notes rvg@cse.unsw.edu.au