ESERCIZI

  1. Studiare una delle seguenti relazioni comportamentali
    1. Simulation (testo, pag. 52)
    2. Ready simulation (testo, pag. 52)
    3. 2-nested simulation (testo pag. 70)
    4. Branching bisimulation (testo, pag. 64)
    In particolare, studiare: e, facoltativamente:
  2. Dimostrare che ogni processo del CCS finito termina in un numero finito di passo (senza somme infinite e con).
  3. Dimostrare che la codifica del CCS con value passing nel CCS puro è vista a lezione corretta e completa rispetto alla semantica operazionale (in RSBook Esercizio 2.14)
  4. Dimostrare che la trace equivalence è una congruenza per il CCS.
  5. Siano T e T' due LTS e si assuma che esista un morfismo f : T → T' tra i due LTS visti come grafi con archi etichettati. Discutere la relazione esistente tra le proprietà di f e le proprietà di bisimulazione.
  6. Indichiamo con ai = a. ... a. 0, ovvero una sequenza di i azioni a. Sia inoltre Aω = a. Aω. Dimostrare che i processi Σi ai   e   Aω + Σi ai soddisfano le stesse formule della logica HML, ma non sono bisimili. E se si considera la logica con ricorsione?
  7. Mostrare che la codifica di uno degli operatory Inv, Pos, Safe, Even, Until (strong o weak) nel mu-calcolo cattura la proprietà intesa, ad es. che
    [[ Even(φ) ]] = { P | per ogni computazione completa P = P0 → P1 → P2 → ... esiste i tale che Pi ⊨ φ }.
  8. Mostrare che la negazione è codificabile nella logica di Hennessy-Milner, ovvero che per ogni formula φ esiste una formula φc tale che per ogni processo P vale P ⊨ φ se e solo se non vale P ⊨ φc. Discutere il caso della logica senza ricorsione, e quindi considerare l'estensione con ricorsione.
  9. Mostrare che la semantica della logica di Hennessy-Milner vista a lezione è ben definita, ovvero che quando si considerano minimi e massimi punti fissi, le funzioni corrispondenti sono monotone su di un reticolo. Discutere se e come potrebbe essere inclusa la negazione nella logica.
  10. Discutere la relazione esistente tra la congruenza osservazionale ≡c e la massima congruenza contenuta nella bisimilarità debole. [duplicato, si veda N]
  11. Verificare che la weak bisimilarity con guarded sum è una congruenza.
  12. Dimostrare che la semantica [[P]]η di una formula HML è indipendente dal valore che η associa a variabili non libere in P.
  13. Discutere una estensione del CCS con un operatore di composizione sequenziale tra processi P; Q. Dare una semantica operazionale e analizzare la possibilità di avere una codificare in CCS dell'operatore definito.
  14. Dimostrare che la chiusura contestuale della bisimilarità debole ≈ (ovvero la relazione ≈̑ definita da P ≈̑ Q se per tutti i contesti C[] risulta C[P] ≈ C[Q]) è la più grande congruenza che raffina la bisimilarità debole, ovvero
    1. ≈̑ ⊆ ≈
    2. ≈̑ è una congruenza
    3. ≈̑ è la più grande relazione che soddisfa i due punti precedenti
    Dimostrare che la suddetta relazione è la congruenza osservazionale ≡c (o almeno che ≡c ⊆ ≈̑).
  15. Verificare che se F è il funzionale della bisimulazione, allora le relazioni F(n)(Proc x Proc) sono tutte equivalenze
  16. Dimostrare il teorema di Knaster-Tarski nel caso di reticoli completi.
  17. Verificare se quando D è un reticolo completo numerabile e F : D -> D una funzione monotona allora il minimo punto fisso si ottiene come supnF(n)(0), dove 0 è il minimo del reticolo. Fonire una dimostrazione o un controesempio. Eventualmente discutere altre condizioni che assicurino la validità del risultato.
  18. Dimostrare la correttezza della tecnica di bisimulazione up-to bisimilarity.
  19. Dimostrare che P e Q sono debolmente bisimili se e solo se vale una delle tre (i) P osservazionalmente congruente a Q (ii) P osservazionalmente congruente a tau.Q (iii) tau.P osservazionalmente congruente a Q
  20. Mostrare la coincidenza di string bisimilarity e strong bisimilarity (ex. 3.9 nel libro RSBook)
  21. Mostrare che la weak bisimilarity è la strong bisimilarity sull'LTS con transizioni weak. (Ex. 3.30 nel libro RSBook).
  22. Mostrare che l'operatore τL(P) che trasforma in τ le transizioni su canali in L e lascia filtrare quelle non in L è definibile in CCS (Esercizio 3.15).

MINI-PROGETTI

Seguono alcune idee a titolo indicativo:
  1. Modellare in CCS uno dei seguenti algoritmi o protocolli e provarne la correttezza (si veda il Cap. 7 del libro RSBook). Le verifiche possono basarsi su di un tool didattico (CWB o CAAL).
  2. Studiare e sperimentare strumemti più sofisticati
  3. Realizzare un piccolo progetto, di interesse per lo studente, che preveda una strutturazione concorrente dell'applicazione. Ad esempio, realizzazione di algoritmi paralleli, parallelizzazione di computazioni intensive (nello stile dell'esempio dei frattali accennato a lezione, oppure un sudoku solver, un analizzatore di testo, etc.). Preferibilmente, il programma dovrebbe essere relizzato in due linguaggi distinti.

APPROFONDIMENTI