Schema della sezione

  • Modelli di sistemi concorrenti - CCS

    Presentiamo un linguaggio (CCS - Calculus of Communicating Systems) con il quale è possibile specificare, in forma astratta, sistemi concorrenti, cioè formati da componenti che interagiscono. Studiamo una nozione di equivalenza fra "programmi" scritti in questo linguaggio, e il suo interesse, sia teorico sia applicativo.

    • Lezione del 20 ottobre 2022, ore 15:30-18:30, aula U24-C1

      Dalla programmazione sequenziale a quella concorrente: i sistemi reattivi; problematiche relative alla semantica.  Introduzione al Calcolo dei sistemi comunicanti (CCS). I sistemi di transizioni etichettati (LTS): definizioni. La sintassi del CCS puro e la sua semantica come LTS attraverso regole di inferenza.

    • File
      appunti_della lezione_22ottobre22 File

    • Lezione del 24 ottobre 2022, ore 15:30-17:30, aula U4-02

      Il CCS puro sintassi e semantica  tramite LTS. L'esempio del produttore e consumatore con buffer a una posizione: la specifica in CCS e il sistema di transizioni associato. Requisiti per una nozione di equivalenza per i sistemi reattivi: congruenza rispetto agli operatori. Equivalenza rispetto alle Tracce:definizione formale e discussione rispetto alla possibilità di generare deadlock (si veda l'esempio delle due macchinette del caffè).

    • File
      appunti_della lezione_24_ottobre_22 File

    • Lezione del 27 ottobre 2022, ore 15:30-16:30, aula U24-C1 

      Bisimulazione (forte). Definizione formale e discussione su esempi.

    • File
      appunti_della lezione_27_ottobre_22 File

    • Lezione del 3 novembre 2022, ore 15:30-18:30, aula U24-C1

      Bisimulazione forte, esempi (confronto tra buffer a due posizioni e composizione parallela di due buffer a una posizione) La Bisimulazione forte è una congruenza rispetto agli operatori del CCS. 

      Relazione di transizione debole, equivalenza rispetto alle Tracce debole; Bisimulazione debole. Discussione su esempi.

      La verifica della Bisimulazione con il gioco "attaccante-difensore".

    • File
      slide sulla Bisimulazione debole e il gioco per verificarla File

    • Lezione del 7 novembre 2022, ore 15:30-18:30, aula U4-02

      Relazioni tra equivalenza rispetto alle Tracce e Bisimulazione forte e debole.
      Processi deterministici ed equivalenze.
      Esercizi sulla verifica della bisimulazione. (si vedano le slide 13, 14 e 15 del file  "Bisimulazione e congruenza")

    • File
      Bisimulazione debole proprietà - slide File

    • Lezione del 10 novembre 2022, ore 15:30-18:30, aula U24-C1

      La Bisimulazione debole è una congruenza rispetto agli operatori del CCS tranne che rispetto all'operatore + e alla ricorsione.
      Bisimulazione e Relazione di congruenza definita con Assiomi.
      Esercizi sulla Bisimulazione come gioco

    • File
      Bisimulazione e congruenza File
    • File
      Esercizi sulla verifica della Bisimulazione - da svolgere File

      Questi esercizi verranno corretti lunedì 14 novembre.

    • Lezione del 14 novembre 2022, ore 15:30-18:30, aula U4-02

      Soluzione degli esercizi assegnati sulla verifica della Bisimulazione.
      Discussione su semantica a "interleaving" del CCS e ipotesi di atomicità delle azioni.
      La specifica di un protocollo di comunicazione con CCS e con reti di Petri.

    • File
      soluzioni degli esercizi sulla verifica della Bisimulazione File
    • File
      lez 14 nov File
    • File
      la specifica di un protocollo di comunicazione File

    • -------------------------------------------

      Materiale per questo argomento

    • Pagina
      Reactive Systems: Modelling, Specification and Verification Pagina
    • File
      Bisimulazione debole e il gioco per la sua verifica File

      Per la verifica della bisimulazione con la tecnica tratta dalla teoria dei giochi dell'"attaccante e difensore" si veda anche la sezione 3.5 e 3.5.1 del testo  "Reactive Systems" al link precedente. (Si noti che viene presentata la tecnica per la Bisimulazione forte e solo nella sezione 3.5.1 quella per la Bisimulazione debole.) 

    • File
      Bisimulazione, esempi File
      Alcuni di questi esercizi sono stati discussi a lezione

    • Letture

    • File
      C.A.R. Hoare, Communicating Sequential Processes, 1978 File
    • File
      R. Milner, Elements of Interactions File
    • File
      caal_tutorial File

      Caal è un tool open source sviluppato presso l'Università di  Aalborg, in Danimarca e disponibile al link: https://caal.cs.aau.dk/. Consiste di vari moduli tra cui un editor per CCS, uno per la visualizzazione dei processi, uno per la verifica delle equivalenze e il model checking e uno per il gioco della bisimulazione. Questo file presenta gli aspetti fondamentali del tool e contiene indicazioni su come utilizzarlo.