ESERCIZI
-
Studiare una delle seguenti relazioni comportamentali
- Simulation (testo, pag. 52)
- Ready simulation (testo, pag. 52)
- 2-nested simulation (testo pag. 70)
- Branching bisimulation (testo, pag. 64)
In particolare, studiare:
- le proprietà di preordine o di equivalenza
- la relazione con la bisimulation equivalence
- le proprietà di congruenza
e, facoltativamente:
- una possibile caratterizzazione logica (nello stile del teorema
di Hennessy-Milner)
-
una possibile caratterizzazione come gioco
-
Dimostrare che ogni processo del CCS finito termina in un numero finito di passo (senza somme infinite e con).
-
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)
-
Dimostrare che la trace equivalence è una congruenza per il CCS.
-
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.
-
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?
-
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 ⊨ φ }.
-
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.
-
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.
-
Discutere la relazione esistente tra
la congruenza osservazionale ≡c e la massima
congruenza contenuta nella bisimilarità debole. [duplicato, si veda N]
-
Verificare che la weak bisimilarity con guarded sum è una congruenza.
-
Dimostrare che la semantica [[P]]η di una formula HML è indipendente dal valore che η associa a variabili non libere in P.
-
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.
- 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
- ≈̑ ⊆ ≈
- ≈̑ è una congruenza
- ≈̑ è la più grande relazione che soddisfa i due punti precedenti
Dimostrare che la
suddetta relazione è la congruenza osservazionale
≡c (o almeno che ≡c ⊆ ≈̑).
-
Verificare che se F è il funzionale della bisimulazione, allora le
relazioni F(n)(Proc x Proc) sono tutte
equivalenze
-
Dimostrare il teorema di Knaster-Tarski nel caso di reticoli completi.
-
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.
-
Dimostrare la correttezza della tecnica di bisimulazione up-to bisimilarity.
-
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
-
Mostrare la coincidenza di string bisimilarity e
strong bisimilarity (ex. 3.9 nel libro RSBook)
-
Mostrare che la weak bisimilarity
è la strong bisimilarity sull'LTS con transizioni
weak. (Ex. 3.30 nel libro RSBook).
-
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:
-
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).
-
Uno dei problemi degli algoritmi di mutua esclusione nei capitoli
5, 6 o 7 del libro
The
Little Book of Semaphores di Allen B. Downey.
- Alternating bit protocol (si veda il link
su Wikipedia oppure qui).
- Il protocollo Carrier-Sense Multiple Access with Collision
Detection (CSMA-CS). Si
veda il lavoro.
- Bounded retransmission protocol (si
veda qui).
-
Prisoner's game
- Dijkstra's concurrent programming control problem (mutual
exclusion for 3 processes) - si veda
questo articolo
- Studiare e sperimentare strumemti più
sofisticati
- CADP
(Construction and Analysis of Distributed Processes)
-
mCRL2: A language and tool set
to study communicating processes with data
- UPPAAL, an integrated
tool environment for modeling, validation and verification of
real-time systems.
-
PAT: Process Analysis
Toolkit
- 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
-
Aspetti teorici.
- Caratterizzazione della bisimilarità e del model checking
come gioco (si veda
il lavoro
di Colin Stirling e il libro RSBook a pag. 115).
- Algoritmi di decisione per la bisimulazione (Kannelakis e
Smolka, Paige e Tarjan) - si
veda qui.
- Bisimulazione, coinduzione: una visione storica (si veda
l'articolo
di Davide Sangiorgi).
- Pi-calcolo: Bisimulazione e proprietà di congruenza.
- Timed CCS / Timed Automata / Timed bisimulation (libro RSBook)
- Un approccio, proposto da Leifer e Milner, per la
derivazione automatica di bisimulazioni che sono congruenze
[articolo]
- Concurrent separation logic [Articolo1] [Articolo2]
- Altri calcoli, con funzionalità diverse.
- Modeling and Verifying Security Protocols with the Applied Pi
Calculus e il tool
"ProVerif" [articolo]
- Spi-calcolo, un calcolo per l'analisi di protocolli crittografici [Articolo]
- Ambient-calcolo, un calcolo per descrivere sistemi con
mobilità (computazione su dispositivi mobili e codice
mobile)
[Articolo]
e la corrispondente logica spaziale
[Articolo]
- CCS reversibile per systems biology
[Articolo]
- Formalizzazione di web-services
[Articolo]
-
Calcoli fondazionali per il service oriented computing
[articolo]
- Session types - tipi comportamentali per la concorrenza
[articolo]
-
Autonomic computing [Articolo]
-
Approcci alla concorrenza.
-
Linguaggi.
- Jolie, for service oriented programming
- ORC, for web service orchestration
- ClojureScript, client side Clojure
- Channels in Clojure (start
from here)
- OTP library in Erlang
- Elixir, a fresh look on Erlang
- Actors in the Akka toolkit
- Rust, a multiparadigm language with ownership
- Haskell and concurrency (e.g. this tutorial)
In generale, un progetto di interesse in questo contesto può
consistere nel implementare un paradigma di comunicazione visto per un
linguaggio in un linguaggio diverso (e.g., futures and promises in Go,
oppure actors in Clojure o in Go, ....).
-
Tecniche di verifica su Linguaggi.