Teaching
Modelling and Verification  Spring 201820, 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: HennessyMilner Logic
Motivation; syntax of HennessyMilner logic; semantics of HennessyMilner logic;
examples in CAAL; correspondence between strong bisimilarity and HennessyMilner logic.
Lecture 6: Tarski's FixedPoint Theorem
HennessyMilner logic and temporal properties; complete lattices;
Tarski's fixed point theorem; computing fixed points in finite lattices.
Lecture 7: HennessyMilner Logic with Recursion
Bisimulation as a fixed point; one recursively defined variable in HennessyMilner 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/20112011/2012 (only in italian!)
Esercitazione 1
Semplificazione di espressioni booleane, sintesi di circuiti logici
e semplificazione attraverso il metodo delle mappe di Karnaugh.
