Modelling and Verification - Spring 2018-20, Aalborg University

  • Lecture 1: Labelled Transition Systems
    Introduction; reactive systems; labelled transition systems; binary relations; CCS informally.
  • Lecture 2: The Calculus of Communicating Systems (CCS)
    CCS informally (continuation); formal definition of CCS; semantics of CCS; examples.
  • Lecture 3: Strong Bisimilarity
    Value passing CCS; trace equivalence; strong bisimilarity; bisimulation games; properties of strong bisimilarity.
  • Lecture 4: Weak Bisimilarity
    Properties of strong bisimilarity; weak bisimilarity; weak bisimulation games; properties of weak bisimilarity; example (a simple communication protocol).
  • Lecture 5: Hennessy-Milner Logic
    Motivation; syntax of Hennessy-Milner logic; semantics of Hennessy-Milner logic; examples in CAAL; correspondence between strong bisimilarity and Hennessy-Milner logic.
  • Lecture 6: Tarski's Fixed-Point Theorem
    Hennessy-Milner logic and temporal properties; complete lattices; Tarski's fixed point theorem; computing fixed points in finite lattices.
  • Lecture 7: Hennessy-Milner Logic with Recursion
    Bisimulation as a fixed point; one recursively defined variable in Hennessy-Milner logic; game characterization; more recursively defined variables; characteristic properties.

DEIS Ph.D. Study Group - Aalborg University

  • From Metrics to Topologies
    A short excursus about why metric and topological spaces have been introduced. The notes introduce only the very basic definitions: boundary, interior and closure operators, open/closed sets, neighborhood, base, sequential and net convergence, continuous functions, etc.

Architettura degli elaboratori (Esercitazioni) - 2010/2011-2011/2012 (only in italian!)

  • Esercitazione 1
    Semplificazione di espressioni booleane, sintesi di circuiti logici e semplificazione attraverso il metodo delle mappe di Karnaugh.

valid XHTML | CSS