Homework 1, Tuesday 25-2-2020
- 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.
[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
- Give an example of an equivalence relation on the domain of all
- 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?
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.
- 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.
- Draw a process graph for the ACP expression a(bc+b(c+d)).
- 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.
- Give a formal definition of the sequential composition operator
of ACP (see notes), in the style of the notes.