Course Slides
Lectures
3/10/2018: general info; reactive systems; process algebraic approach; formal methods for reactive systems (
registration)
-
17/10/2018: equivalences; functions; induction principle; inductively defined sets; inference systems (
registration)
22/10/2018: grammars; LTS; syntax of regular expressions (
registration)
24/10/2018: operational semantics of regular expressions (
registration)
29/10/2018: examples about operational semantics of regular expressions; denotational semantics of regular expressions; axiomatic semantics of regular expressions (
registration)
5/11/2018: introduction to Maude: sort, operations, equations (
registration)
-
-
14/11/2018: First in itinere test.
19/11/2018: Discussion of the in itinere test results; discussion of projects.
-
-
5/12/2018: Seminar on Polymorphic Sessions and Functions.
10/12/2018: Process Algebras operators (basic processes, sequential composition, choice, parallel composition, merge) (
registration)
12/12/2018: Process Algebras operators (hiding, recursive definitions, replication) (
registration)
19/12/2018: Behavioural equivalences (strong bisimilarity, weak trace equivalence, weak bisimilarity) (
registration)
9/1/2019: Exercises on CCS and behavioural equivalences (
registration)
14/1/2019: Second in itinere test
21/1/2019: Project presentations (from 9:00 to 12:00).
Reference books
The main material of the course consists of:
Rocco De Nicola.
A gentle introduction to Process Algebras. Notes obtained by the restructuring of two entries (Process Algebras - Behavioural Equivalences) of Encyclopedia of Parallel Computing, David A. Padua (Ed.). Springer 2011; pp. 120-127 and pp. 1624-1636.
Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen and Jiri Srba, “Reactive Systems. Modelling, Specification and Verification”, Cambridge University Press, 2007. ISBN: 9780521875462. Website of the book with additional material available:
http://rsbook.cs.aau.dk
Morover, lecture notes, papers and slides may be provided in this website.
The Maude tool can be downloaded for free for academic use, together with documentation and tutorials, from the website: http://maude.cs.illinois.edu/
The TAPAs tool can be downloaded for free for academic use, together with documentation and tutorials, from the website: http://rap.dsi.unifi.it/tapas/
The mCRL2 tool can be downloaded for free for academic use, together with documentation and tutorials, from the website: http://www.mcrl2.org/release/user_manual/index.html