Exam - Languages for Concurrency and Distribution

1. Study one of the following behavioral relations: simulation (textbook, pag. 52), ready simulation (textbook, pag. 52), 2-nested simulation (textbook, pag. 70), or branching bisimulation (textbook, pag. 64). In particular, study the preorder or the equivalence properties, the relation with bisimulation equivalence, and the congruence properties; and, optionally, a possible logical characterisation (in the style of Hennessy-Milner's theorem) or a possible game-theoretical characterisation. [*]
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 (see also the video video). [*]
6. Denote by aⁱ = a. ... a. 0, i.e., a sequence of i a-labelled actions. Let A^ω = a. A^ω. Show that the processes Σ_i aⁱ   and   A^ω + Σ_i aⁱ 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 = P₀ → P₁ → P₂ → ... there exists i such that P_i ⊨ φ }. [*]
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. Prove that weak bisimilarity is a congruence in CCS with guarded sum.
11. Prove that the semantics [[P]]_η of a HML formula is independent from the value that η associates with variables which are not free in P.
12. 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. [*]
13. 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.,
    • ≈̑ ⊆ ≈
    • ≈̑ is a congruence
    • ≈̑ 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 ⊆ ≈̑). [*]
14. Prove that, if F denotes the operator having bisimilarity as a fixpoint, all the relations F⁽ⁿ⁾(Proc x Proc) are equivalences
15. 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).
16. 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 sup_nF⁽ⁿ⁾(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.
17. 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
18. 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
    • if P =P₀ →^α₀ P₁ →^α₁ ... →^α_n P_n then Q =Q₀ →^α₀ Q₁ →^α₁ ... →^α_n Q_n and P_i R Q_i for i = 1, ... n
    • dual condition
19. Prove that weak bisimilarity is strong bisimilarity on the LTS with weak transitions (Ex. 3.30 in RSBook).
20. 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 in RSBook).
21. 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
    • if P →^α P' then Q →^αQ' and P' ∼ P'' R Q'' ∼ Q'
    • dual condition
    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
    • if P →^α P' then Q →^αQ' and P' = C[P''], Q' = C[Q''] with P'' R Q''
    • dual condition

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):
   • One of the mutual exclusion algorithms in Chapters 5, 6, or 7 of The Little Book of Semaphores by Allen B. Downey.
   • Alternating bit protocol (Wikipedia).
   • Carrier-Sense Multiple Access with Collision Detection (CSMA-CD). See this paper.
   • Bounded retransmission protocol (see this link).
   • Prisoner's game
   • Dijkstra's concurrent programming control problem (mutual exclusion for 3 processes) - see this paper.
3. Study and experiment with one of the advanced tools:
   • CADP (Construction and Analysis of Distributed Processes)
   • mCRL2: a language and tool set to study communicating processes with data
   • PRISM (probabilistic model checker)
   • UPPAAL, an integrated tool environment for modeling, validation and verification of real-time systems
   • PAT: Process Analysis Toolkit
4. Realise a small project, of your interest, which involves a concurrent structuring of the application (implementation of a parallel algorithm, parallelization of intensive computations, etc.). Preferably, the program should be written in two distinct languages. Some ideas:
   • Solve Sudoku or other puzzles in parallel
   • SAT/constraints problems or graph coloring
   • Multi-room chat with message passing (ordering, failures, synchronization)
   • Dataflow computation engine: build a graph of concurrent processing nodes with data flowing
   • Actor-based simulation: simulate agents (traffic, market, ecosystem)
   • Parallel fractal renderer: compute fractals with dynamic load balancing

Theoretical themes

• Characterization of bisimilarity and model checking as a game (see this paper by Colin Stirling, and RSBook pag. 115).
• Decision algorithms for bisimulation (Kanellakis and Smolka, Paige and Tarjan) - see here.
• Bisimulation and coinduction: a historical view (see this paper by Davide Sangiorgi).
• Pi-calculus: bisimulation and congruence properties.
• Timed CCS / Timed Automata / Timed bisimulation (in RSBook).
• An approach, proposed by Leifer and Milner, for the automatic derivation of bisimulations that are congruences [paper].
• Concurrent separation logic [paper 1] [paper 2].

Other calculi, with different features

• Modeling and verifying security protocols with the Applied Pi Calculus and the tool ProVerif [paper].
• Spi-calculus, a calculus for the analysis of cryptographic protocols [paper].
• Ambient calculus, for describing systems with mobility [paper], and the corresponding spatial logic [paper].
• Reversible CCS for systems biology [paper].
• Formalization of web services [paper].
• Foundational calculi for service oriented computing [paper].
• Session types - behavioural types for concurrency [paper].
• Autonomic computing [paper].

Approaches to concurrency

• Actor model [paper 1] [paper 2] [paper 3].
• Transactional memories [paper 1] [paper 2] [paper 3].
• Weak memory models [paper].

Languages

• Jolie, for service oriented programming.
• ClojureScript, client-side Clojure.
• Channels in Clojure (start from here).
• Gleam, type safety and modern syntax on the Erlang runtime.
• OTP library in Erlang.
• Actors in the Akka toolkit.
• Rust, a multiparadigm language with ownership.
• Elixir, a fresh look at Erlang.
• ORC, for web service orchestration.
• Haskell and concurrency (e.g. this tutorial).

In general, a project of interest in this context may consist in implementing a communication paradigm seen for one language in a different language (e.g., futures and promises in Go, or actors in Clojure or in Go, ...).

Verification techniques for languages

• Language-based security on Android [paper].
• Analysis techniques for Google Go - see this paper.
• Debugging in Chess.