ESERCIZI

Esercizio A. Studiare una delle seguenti relazioni comportamentali
  1. 2-nested simulation (testo pag. 70)
  2. Branching bisimulation (testo, pag. 64)
In particolare, studiare: e, facoltativamente:

Esercizio B. Dimostrare che la codifica del CCS con value passing nel CCS puro è vista a lezione corretta e completa rispetto alla semantica operazionale.

Esercizio C. Dimostrare che la trace equivalence è una congruenza per il CCS.

Esercizio D. 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.

Esercizio E. 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?

Esercizio F. 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 |= φ }.

Esercizio G. 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..

Esercizio H. Discutere la relazione esistente tra la congruenza osservazionale e la massima congruenza contenuta nella bisimilarità debole.

Esercizio I. Dimostrare che la semantica [[P]]η di una formula HML è indipendente dal valore che η associa a variabili non libere in P.

Esercizio L. 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.

Esercizio M. Dimostrare nel pi-calcolo i seguenti due fatti:

Esercizio N. Definire la bisimulazione debole (≈) nel pi-calcolo. Definire tre processi True(l), False(l), Test(l,P,Q) del pi-calcolo monadico senza operatore di scelta, tali che valgano le seguenti equivalenze: (ν l) (True(l) | Test(l,P,Q)) ≈ P e (ν l) (False(l) | Test(l,P,Q)) ≈ Q. Dimostrare una di queste due equivalenze.

Esercizio O. Dimostrare che nel pi-calcolo l'operatore di restrizione preserva la bisimulazione forte, cioe' se P ∼ Q allora (ν a) P ∼ (ν a) Q

MINI-PROGETTI

Modellare in CCS uno dei seguenti algoritmi o protocolli e provarne la correttezza (si veda il Cap. 7 del libro). Una ulteriore alternativa è la seguente:

APPROFONDIMENTI