Mpri concurrency (cours 2 3) final exam, 2005 2006 22 feb 2006

Sujets

• cours

Informations

• Publié par: angueran
• Nombre de lectures: 103
• Langue: Français

Extrait

MPRI Concurrency (Cours 23) Final exam, 20052006 22 Feb 2006, 16.15–19.15 [e-mail] Question annotations:∗= easy;∗∗= medium;∗∗∗= hard 1. Considerthe termP=νy.(x(x).x(x).xy)|νy.(xy.νx.(yx.x(x))) withx6=y. (a)∗What is the set of free names ofP? Solution:{x}. ′ (b)∗Define a processPthat isαequivalent toPand has all bound names distinct from each other and from all free names. ′ Solution:P=νy 1 .(x(x 1 ).x 1 (x 2 ).x 2 1 )|νy 2 .(x 2 .νx 3 .( 2 x 3 .x 3 (x 4 ))).

′ (c)∗What is the set of free names ofP? Solution:{x}, sinceαconversion doesn’t change the free names. ′ (d)∗∗Show the sequence of three reduction steps (−→) starting atP, taking care to make explicit any scope extrusions you need (i.e. use of(strex)in≡). Solution: ′ P ≡νy 1 , y 2 .(x(x 1 ).x 1 (x 2 ).x 2 y 1 |xy 2 .νx 3 .(y 2 x 3 .x 3 (x 4 ))) extrusionofy 2 −→νy 1 , y 2 .(y 2 (x 2 ).x 2 y 1 |νx 3 .(y 2 x 3 .x 3 (x 4 ))) communicationonx ≡νy 1 , y 2 , x 3 .(y 2 (x 2 ).x 2 y 1 |y 2 x 3 .x 3 (x 4 )) extrusionofx 3 −→νy 1 , y 2 , x 3 .(x 3 y 1 |x 3 (x 4 )) communicationony 2 −→νy 1 , y 2 , x 3 .(0|0on) communicationx 3

2. This question explores the relationship between name hiding and bisimulation in the coreπ calculus (i.e. the calculus on slide 3 with no extra features).

(a)∗∗∗Prove that strong bisimilarity is closed by new binding, i.e.P∼Qimpliesνx.P∼ νx.Q. Youmay only use the basic definitions of bisimulation and labelled transition (no “up to” techniques). Hint: startwith a relationR={(νx.P,νx.Q)/ P∼Q}and try to show thatRis a strong bisimulation. Youmay have to add some more pairs toR. ′ ′ Solution:TakeR=R ∪(∼aim to show that). WeRTo dois a bisimulation. α ′ ′ RandP−→Pwit that we need to consider (P 0 , Q 0 )∈ 0 0 hbn(α)∩fn(Q 0 ) =∅. We distinguish two cases. α ′ ′ CaseP∼Q:By definition of∼, there existsQsuc−→Q 0 0 0 h thatQ 0 0 and ′ ′′ ′′ P∼Q, hence (QP ,)∈ R, as desired. 0 00 0 Case(P 0 , Q 0 )∈ R:Then there existsPandQsuch thatP∼QandP 0 =νx.P andQ 0 =νx.Qconsider the two possible ways that the labelled transition. We α ′ Pould derived. P 0 −→ 0 c havebeen α ′ ′′ ′ Case(labnew):Then there existsPsuch thatP−→PandP=νx.P 0 andx /∈bn(αhypothesis, we also have). Bybn(α)∩fn(Q 0 ) =∅, hence bn(α)∩fn(Q) =∅, thus it is safe to apply the definition of bisimulation to α ′ ′′ ′ the hypothesisP∼Q; hence there existsQsuch thatQ−→QandP∼Q. α ′ ′′ ′′ ′ LetQ=νx.Qby. Then(labnew),Q 0 −→Q. Finally,(P ,Q)∈ R ⊆ R, 0 00 0 as desired.

1