Teaching

Modelling and Verification - Spring 2018-20, Aalborg University

• Lecture 1: Labelled Transition Systems

  Introduction; reactive systems; labelled transition systems; binary relations; CCS informally.

  (slides)
• Lecture 2: The Calculus of Communicating Systems (CCS)

  CCS informally (continuation); formal definition of CCS; semantics of CCS; examples.

  (slides)
• Lecture 3: Strong Bisimilarity

  Value passing CCS; trace equivalence; strong bisimilarity; bisimulation games; properties of strong bisimilarity.

  (slides)
• Lecture 4: Weak Bisimilarity

  Properties of strong bisimilarity; weak bisimilarity; weak bisimulation games; properties of weak bisimilarity; example (a simple communication protocol).

  CAAL: protocol.caal | Tutorial | (slides)
• 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.

  CAAL: hm.caal | (slides)
• 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.

  (slides)
• 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.

  (slides)

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.

  (handwritten notes)

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.

  (appunti)

valid XHTML | CSS