Reference no: EM132385745
Questions -
Q1. Consider the automaton on page 15 in Milner's book, with the initial state as accepting state. Derive a regular expression for the language accepted by this automaton.
Q2. Give the standard form of
(newa((a.Q + b.S)|(b-.P + a-.P)))|newb(a.Q|a-.0)
and prove that it is structurally equivalent.
Q3. Consider
P1 =def a.P1 + b.P2 + τ.P2, P2 =def a.P2 + τ.P3, P3 =def b.P1
and
Q1 = a.Q1 + τ.Q2, Q2 =def b.Q1
Prove or refute that P1 ≈ Q1.
Q4. Consider the following equation:
X ≈ τ.X + a.Q
Prove (using 6.15) that if P1 is a solution, then also τ.(τ.P1 + τ.P2), with P2 any process, is a solution.
Q5. Why does this weak equivalence not hold? Argue informally why it is not true. There is a state of S which is equivalent to no possible state of the specification Scheduler. (Hint: This state only occurs after about 2n transitions from the start.)
Q6. Draw the transition graph of S, when n = 2. In general, every state is clearly of the form new c→(Q1|Q2| · · · |Qn), where each Q is one of A, B, C, D, E (with subscript). Convince yourself that the only accessible states are those in which one Q is A, B or C, and all the others are either D or E.
Q7. What state of Scheduler does new c→(E1|D2|C3|E4) correspond to?
Q8. Give formal derivations of all the actions and reactions of process newc(E1|D2|C3|E4) from question 7.
Q9. Using the Expansion Law, Proposition 5.23, show that each of the following is strongly equivalent to a summation Σr αr.S=, where each αr is ai, bi or τ and each Sr an accessible state:
new c→(D1|D2|A3|E4)
new c→(D1|E2|B3|D4)
new c→(E1|D2|C3|E4).
Q10. Let the relation R containing the following pairs, where {i}, X and Y form any partition of the set {1, . . . , n}:
Ai,X,Y, Schedi,Y
Bi,X,Y, Schedi,YUi
Ci,X,Y, Schedi+1,YUi.
Then show that R is a weak bi simulation up to ∼.
Textbook - Communicating and Mobile Systems: the π-Calculus by Robin Milner. ISBN 0 521 64320.