Reference no: EM132385479

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

P₁ =^def a.P₁ + b.P₂ + τ.P₂, P₂ =^def a.P₂ + τ.P₃, P₃ =^def b.P₁

and

Q₁ = a.Q₁ + τ.Q₂, Q₂ =^def b.Q₁

Prove or refute that P₁ ≈ Q₁.

Q4. Consider the following equation:

X ≈ τ.X + a.Q

Prove (using 6.15) that if P₁ is a solution, then also τ.(τ.P₁ + τ.P₂), with P₂ 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^→(Q₁|Q₂| · · · |Q_n), 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^→(E₁|D₂|C₃|E₄) correspond to?

Q8. Give formal derivations of all the actions and reactions of process newc(E₁|D₂|C₃|E₄) 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 a_i, b_i or τ and each S_r an accessible state:

new c^→(D₁|D₂|A₃|E₄)

new c^→(D₁|E₂|B₃|D₄)

new c^→(E₁|D₂|C₃|E₄).

Q10. Let the relation R containing the following pairs, where {i}, X and Y form any partition of the set {1, . . . , n}:

A_i,X,Y, Sched_i,Y

B_i,X,Y, Sched_i,YUi

C_i,X,Y, Sched_i+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.