EXERCISES

  1. Study one of the following behavioral relations
    1. Simulation (textbook, pag. 52)
    2. Ready simulation (textbook, pag. 52)
    3. 2-nested simulation (textbook pag. 70)
    4. Branching bisimulation (textbook, pag. 64)
    In particular, study: and, optionally:

  2. Prove that each process in the finite fragment of CCS with finite sums terminates in a finite number of steps and prove also that the number of reachable states is finite. Discuss the case of infinite sums.
  3. Prove that the encoding of CCS with value passing into pure CCS is sound with respect to the operational semantics (in RSBook, Exercise 2.14)

  4. Prove that trace equivalence is a congruence for CCS.

  5. Let T and T' be two LTSs and assume that there is a morphism f : T → T' between the two LTSs seen as graphs with labelled edges. Discuss the relation between the properties of f and the bisimulation properties.

  6. Denote by ai = a. ... a. 0, i.e., a sequence of i a-labelled actions. Let Aω = a. Aω. Show that the processes Σi ai   and   Aω + Σi ai satisfy the same formulae in Hennessy-Milner logic, but they are not bisimilar. What happens if we consider the logic with recursion?

  7. Show that the encoding of one of the operators Inv, Pos, Safe, Even, Until (strong or weak) in the mu-calculus captures the property of interest, e.g., that
    [[ Even(φ) ]] = { P | for each complete computation P = P0 → P1 → P2 → ... there exists i such that Pi ⊨ φ }.

  8. Show that negation can be encoded in Hennessy-Milner logic, i.e., that for all formula φ there exists a formula φc such that for all processes P it holds P ⊨ φ iff it does not hold P ⊨ φc. Discuss first the logic without recursion and then consider the extension to the logic with recursion.

  9. Show that the semantics of Hennessy-Milner's logic discussed during the lectures is well defined, that is, when we consider least and greatest fixed points, the corresponding functions are monotone on a complete lattice. Discuss whether and how negation might be included in the logic.
  10. Discuss the relation between observational congruence ≡c and the largest congruence included in weak bisimilarity. [duplicated, see N]

  11. Prove that weak bisimilarity is a congruence in CCS with guarded sum.

  12. Prove that the semantics [[P]]η of a HML formula is independent from the value that η associates with variables which are not free in P.

  13. Discuss an extension of CCS with an operator of sequential composition between processes P; Q. Provide an operational semantics and analyze the possibility of having an encoding in CCS of the defined operator.

  14. Show that the contextual closure of weak bisimilarity ≈ (i.e., the relation ≈̑ defined by P ≈̑ Q if for all contexts C[] we have C[P] ≈ C[Q]) is the largest congruence refining weak bisimilarity, i.e.,
    1. ≈̑ ⊆ ≈
    2. ≈̑ is a congruence
    3. ≈̑ is the largest relation satisfying the two items above
    Show that the relation above coincides with the observational congruence ≡c (or, at least, that ≡c ⊆ ≈̑).

  15. Prove that, if F denotes the operator having bisimilarity as a fixpoint, all the relations F(n)(Proc x Proc) are equivalences

  16. Prove Knaster-Tarski's theorem for complete lattices (the set of fixed points of a monotone function over a complete lattice is a complete lattice).

  17. Is it true that if D is a denumerable complete lattice and F : D → D is a monotone function then its least fixed point can be obtained as supnF(n)(0), where 0 is the least element of the lattice? Give a proof or a counterexample. If the answer is negative, discuss further conditions that ensure that the result holds. Discuss also the non denumerable case.

  18. Prove the correctness of the up-to bisimilarity proof technique.

  19. Prove that P and Q are weak bisimilar iff one of the following holds: (i) P observational congruent to Q (ii) P observational congruent to τ.Q (iii) τ.P observational congruent to Q

  20. Prove that string bisimilarity and strong bisimilarity coincide. The definition of string bisimilarity is slightly different from Ex. 3.9 in RSBook. Define a relation R a string bisimilarity if for all processes P, Q

  21. Prove that weak bisimilarity is strong bisimilarity on the LTS with weak transitions. (Ex. 3.30 in RSBook).

  22. Prove that the operator τL(P) which transforms into a τ all communications on the channel in L and leave the others unchanged is definable in CCS (Exercise 3.15).

  23. Prove soundness of bisimulation up-to bisimilarity technique. In detail, say that a relation R is a bisimulation up-to bisimilarity if whenever P R Q Then prove that if R is a bisimulation up-to bisimilarity and P R Q then P ∼ Q.

    Prove soundness also for bisimulation up-to context, i.e., a relation R such that whenever P R Q

MINI-PROJECTS

Some ideas for the second part of the exam are listed below. The list is not intended to be exhaustive.
  1. Realise a compiler of CCS with value passing into CCS with pure synchronisation. The source code could specify for the involved value variables a type which can be an integer range or an enumeration type.

  2. Model one of the following algorithms or protocols in CCS and prove its correctness (see Chapter 7 of the RSBook). Verification can be carried out using one of the didactic tools (CWB or CAAL).
  3. Study and experiment with one of the advanced tools
  4. Realise a small project, of your interest, which involves a concurrent structuring of the application. For example, implementation of some parallel algorithm, parallelization of intensive computations (in the style of the example of fractals discussed in class, or a Sudoku solver, a text analyzer, etc.). Preferably, the program should be written in two distinct languages.

APPROFONDIMENTI