## Homework 1, Tuesday 25-2-2020

1. A binary relation ~ on a set D is an equivalence relation if it is
• reflexive: p ~ p for all processes p in D,
• symmetric: if p ~ q then q ~ p,
• and transitive: if p ~ q and q ~ r then p ~ r.
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.) Assume that the machine does not give change, and that it accepts any amount of surplus money. Try to make the number of states in your LTS as small as possible.
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.

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