Indice

Modelli di calcolo - Models of computation

MOD 2016/17 (375AA, 9 CFU)

Lecturer: Roberto Bruni
web - email - phone 050 2212785 - fax 050 2212726

Office hours: Wednesday 15:00-17:00 or by appointment


Objectives

The objective of the course is to present:

and also to present some intellectual tools/techniques:

To this aim, a rigorous approach will be followed for both the syntax and the semantics of the paradigms we work on:

The focus will be on basic proof techniques (there will be not time to introduce more advanced topics in detail).

In doing so, several important notions will be presented (not necessarily in this order): context-free grammars, proof systems (axioms and inference rules), goal-driven derivations, various incarnations of well-founded induction, structural recursion, lambda-calculus, program equivalence, compositionality, completeness and correctness, type systems, domain theory (complete partial orders, continuous functions, fixpoint), labelled transition systems, bisimulation equivalences, temporal and modal logics, Markov chains, probabilistic reactive and generative systems.


Preliminary test

Preliminary test for the course on Models of Computation


Course Overview

We introduce the principles of operational semantics, the principles of denotational semantics, and the techniques to relate one to the other for an imperative language and for a higher order functional language. Operational and observational semantics of two process description languages (CCS and pi-calculus) are presented. Several examples of temporal and modal logics are also discussed (HM, LTL, CTL*, mu-calculus). Finally, we consider operational nondeterministic models with discrete probabilities, and we present them from the perspective of probabilistic and stochastic automata, and of the PEPA calculus.


Textbook(s)

Main text:

Other readings:


Exams

The evaluation will be based on written and oral exams.

The written exam is not necessary if the two (written) mid-terms exams are evaluated positively.

Registration to written exams (mandatory): Exams registration system

In the written exam the student must demonstrate

During the oral exam the student must demonstrate


Oral Exams: schedule

Date Time Name

Announcements


Lectures

N Date Time Room Lecture notes Links
1 Tue 21/02 11:00-13:00 L1 Introduction to the course
2 Wed 22/02 11:00-13:00 N1 Preliminaries:
formal semantics
3 Thu 23/02 14:00-16:00 N1 Preliminaries:
signatures, unification problem
logical systems, derivations
4 Tue 28/02 11:00-13:00 L1 Preliminaries:
goal-oriented derivations, logic programming

Operational semantics of IMP:
syntax of IMP
5 Wed 01/03 11:00-13:00 N1 Operational semantics of IMP:
inference rules, non-termination, equivalence
6 Thu 02/03 14:00-16:00 N1 Operational semantics of IMP:
equivalence and inequivalence proofs

Induction and recursion:
well-founded relations, transitive closures, acyclic relations, well-founded induction
7 Tue 07/03 11:00-13:00 L1 Exercises on unification and logic systems

Induction and recursion:
mathematical induction, structural induction
8 Wed 08/03 11:00-13:00 N1 Induction and recursion:
termination and determinacy of IMP arithmetic expressions,
induction on derivations, rule induction, determinacy of IMP commands
9 Thu 09/03 14:00-16:00 N1 Induction and recursion:
lexicographic precedence relation, primitive recursive functions
well-founded recursion, Ackermann function
10 Tue 14/03 11:00-13:00 L1 Exercises on the operational semantics of IMP and induction
11 Wed 15/03 11:00-13:00 N1 Partial orders and fixpoints:
partial orders, Hasse diagrams, least upper bound, chains, limits,
complete partial orders, bottom element, powerset completeness
12 Thu 16/03 14:00-16:00 N1 Partial orders and fixpoints:
monotonicity, continuity, Kleene's fixpoint theorem
13 Tue 21/03 11:00-13:00 L1 Partial orders and fixpoints:
immediate consequences operator

Exercises on CPOs and fixed points
14 Wed 22/03 11:00-13:00 N1 Denotational semantics of IMP:
lambda-notation, abstraction, application, alpha-conversion, beta-rule,
capture-avoiding substitutions, denotational semantics of IMP
15 Thu 23/03 14:00-16:00 N1 Denotational semantics of IMP:
equivalence between operational and denotational semantics
16 Tue 28/03 11:00-13:00 L1 Denotational semantics of IMP:
equivalence between operational and denotational semantics,
computational induction (optional argument)


Exercises about denotational semantics of IMP
17 Wed 29/03 11:00-13:00 N1 Exercises about denotational semantics of IMP

Operational semantics of HOFL:
Pre-terms, well-formed terms
18 Thu 30/03 14:00-16:00 N1 Operational semantics of HOFL:
typability, lazy and eager semantics, canonical forms
19 Tue 04/04 11:00-13:00 L1 Exercises on the operational semantics of HOFL

Domain theory:
Integers with bottom, cartesian product
20 Wed 05/04 11:00-13:00 N1 Domain theory:
Functional domains, lifting, continuity theorems
21 Thu 06/04 11:00-13:00 A1 First mid-term written exam
Exam
Appello Straordinario
- Thu 20/04 14:00-16:00 N1 Canceled
22 Wed 26/04 11:00-13:00 N1 Domain theory:
continuity theorems, apply, fix, let

Denotational semantics of HOFL
23 Thu 27/04 14:00-16:00 N1 Exercises on domain theory

Denotational semantics of HOFL:
Type consistency, substitution lemma, compositionality and other properties

Equivalence between the operational and denotational semantics of HOFL:
Correctness of the operational semantics, counterexample to completeness
24 Tue 02/05 11:00-13:00 L1 Equivalence between the operational and denotational semantics of HOFL:
Operational convergence, denotational convergence,
operational convergence implies denotational convergence,
denotational convergence implies operational convergence (optional),
operational equivalence, denotational equivalence, unlifted semantics


Exercises on the denotational semantics of HOFL and on the equivalence between the operational and denotational semantics of HOFL
25 Wed 03/05 11:00-13:00 N1 CCS:
extensible stack, syntax, operational semantics
26 Thu 04/05 14:00-16:00 N1 CCS:
linking operator, CCS with value-passing, recursive declarations,
abstract semantics, graph isomorphism, trace equivalence, bisimulation game,
strong bisimulation, strong bisimilarity
27 Tue 09/05 11:00-13:00 L1 CCS:
properties of strong bisimilarity, guarded processes
28 Wed 10/05 11:00-13:00 N1 CCS:
Knaster-Tarski's fixpoint theorem, compositionality, Hennessy-Milner logic,
axiomatisation of strong bisimilarity
29 Thu 11/05 14:00-16:00 N1 CCS:
Weak bisimilarity, weak observational congruence, Milner's tau-laws,
dynamic bisimilarity, other bisimulation games, modelling with CCS
CAAL
PseuCo
TAPAS
30 Tue 16/05 11:00-13:00 L1 Exercises on CCS
31 Wed 17/05 11:00-13:00 N1 Temporal and modal logics:
linear temporal logic (LTL), computational tree logic (CTL* and CTL), mu-calculus
32 Thu 18/05 14:00-16:00 N1 Pi-calculus:
syntax and operational semantics,
structural equivalence and reduction semantics (optional reading)
abstract semantics, early and late bisimilarities, weak bisimilarities
Google Go
33 Mon 22/05 17:00-18:30 C1 Exercises on modal logics and pi-calculus
34 Tue 23/05 11:00-13:00 L1 Measure theory and Markov chains:
probability space, random variables, exponential distribution,
stochastic processes, homogeneous Markov chains, DTMC, ergodic DTMC,
steady state distribution
35 Wed 24/05 11:00-13:00 N1 Measure theory and Markov chains:
finite path probability, CTMC, infinitesimal generator matrix, embedded DTMC,
bisimilarity revisited, reachability predicate, CTMC bisimilarity, DTMC bisimilarity


Markov chains with actions and nondeterminism:
reactive systems, bisimilarity for reactive systems, Larsen-Skou logic,
generative systems, simple Segala automata, Segala automata
alternating and bundle transitions systems (optional reading)
36 Thu 25/05 14:00-16:00 N1 PEPA:
CSP syntax, CSP operational semantics, PEPA syntax, apparent rate,
PEPA operational semantics
PEPA
37 Tue 30/05 11:00-13:00 L1 Exercises on probabilistic systems
38 Wed 01/06 11:00-13:00 A1 Second mid-term written exam
Exam
39 Thu 15/06 14:00-16:00 C Exam
40 Thu 06/07 14:00-16:00 C Exam
41 Tue 25/07 14:00-16:00 A1 Exam
42 Thu 07/09 14:00-16:00 N1 Exam
43 Tue 31/10 14:00-16:00 C1 Extra-ordinary Exam
44 Tue 16/01 14:00-16:00 N1 Exam
45 Tue 13/02 14:00-16:00 N1 Exam
46 Thu 05/04 14:00-16:00 L1 Extra-ordinary Exam

Past courses