| Entrambe le parti precedenti la revisioneRevisione precedenteProssima revisione | Revisione precedente |
| magistraleinformatica:psc:start [29/04/2025 alle 12:21 (7 settimane fa)] – [Lectures (2nd part)] Roberto Bruni | magistraleinformatica:psc:start [29/05/2025 alle 15:07 (2 settimane fa)] (versione attuale) – [Lectures (2nd part)] Roberto Bruni |
|---|
| | - | Thu | 01/05 | 14:00-16:00 | C1 | **International labour day** | | | | - | Thu | 01/05 | 14:00-16:00 | C1 | **International labour day** | | |
| | - | Fri | 02/05 | 09:00-11:00 | L1 | **Long weekend** | | | | - | Fri | 02/05 | 09:00-11:00 | L1 | **Long weekend** | | |
| | 25 | Tue | 06/05 | 09:00-11:00 | E | 18 - Bisimulation (ctd.):\\ //Guarded processes (again, from Lecture 17), Knaster-Tarski's fixpoint theorem//\\ \\ 19 - Hennessy-Milner logic:\\ //modalities, HML syntax, formula satisfaction, converse of a formula, HML equivalence//\\ \\ 20 - Weak Semantics:\\ //weak transitions, weak bisimulation, weak bisimilarity, weak bisimilarity is not a congruence, weak observational congruence, Milner's tau-laws//\\ \\ 21 - CCS at work:\\ //modelling imperative programs with CCS, playing with CCS (using CAAL), modelling and verification of mutual exclusion algorithms with CCS and CAAL//\\ \\ CAAL session (copy the text and paste it in the Edit panel)\\ \\ Exercises:\\ //Erlang, CCS//\\ \\ 22 - Temporal and modal logics:\\ //linear temporal logic (LTL), linear structures models, shifting, LTL satisfaction, equivalence of formulas, automata-like models// | {{ :magistraleinformatica:psc:2025-04-29_-_18c_-_ccs_bis_as_fix.pdf |Lecture 18c}}\\ Lecture 19\\ Lecture 20\\ Lecture 21\\ [[http://caal.cs.aau.dk/|CAAL]]\\ CAAL session\\ Exercises 06\\ Lecture 22a | | | 25 | Tue | 06/05 | 09:00-11:00 | E | 18 - Bisimulation (ctd.):\\ //Guarded processes (again, from Lecture 17), Knaster-Tarski's fixpoint theorem//\\ \\ 19 - Hennessy-Milner logic:\\ //modalities, HML syntax, formula satisfaction, converse of a formula, HML equivalence//\\ \\ 20 - Weak Semantics:\\ //weak transitions, weak bisimulation, weak bisimilarity, weak bisimilarity is not a congruence, weak observational congruence, Milner's tau-laws//\\ \\ 21 - CCS at work:\\ //modelling imperative programs with CCS// | {{ :magistraleinformatica:psc:2025-04-29_-_18c_-_ccs_bis_as_fix.pdf |Lecture 18c}}\\ {{ :magistraleinformatica:psc:2025-05-06_-_19_-_hml.pdf |Lecture 19}}\\ {{ :magistraleinformatica:psc:2025-05-06_-_20_-_weak.pdf |Lecture 20}}\\ {{ :magistraleinformatica:psc:2025-05-06_-_21_-_ccs_at_work.pdf |Lecture 21}} | |
| | 26 | Thu | 08/05 | 14:00-16:00 | C1 | 22 - Temporal and modal logics (ctd.):\\ //computational tree logic (CTL* and CTL), infinite trees, infinite paths, branching structure, CTL* satisfaction, equivalence of formulas, CTL formulas, expressiveness comparison, mu-calculus, positive normal form, least and greatest fixpoints// | Lecture 22a\\ Lecture 22b | | | 26 | Thu | 08/05 | 14:00-16:00 | C1 | 21 - CCS at work (ctd.) :\\ //modelling imperative programs with CCS, playing with CCS (using CAAL), modelling and verification of mutual exclusion algorithms with CCS and CAAL//\\ \\ CAAL session (copy the text and paste it in the Edit panel) | {{ :magistraleinformatica:psc:2025-05-06_-_21_-_ccs_at_work.pdf |Lecture 21}}\\ [[http://caal.cs.aau.dk/|CAAL]]\\ {{ :magistraleinformatica:psc:caal-session1-2025.zip |CAAL session 1}} | |
| | 27 | Fri | 09/05 | 09:00-11:00 | L1 | 22 - Temporal and modal logics (ctd.):\\ //invariant properties, possibly properties, mu-calculus with labels//\\ \\ 23 - GoogleGo:\\ //an overview//\\ \\ GoogleGo playground:\\ Go principles, variable declaration, type conversion, multiple assignments, type inference, imports, packages and public names, named return values, naked return, multiple results, conditionals and loops, pointers, struct, receiver arguments and methods, interfaces, goroutines, bidirectional channels, channel types, send, receive, asynchronous communication with buffering, close, select, communicating communication means, range, handling multiple senders, concurrent prime sieve | Lecture 22b\\ Lecture 23\\ [[http://golang.org/|Google Go]]\\ go session | | | 27 | Fri | 09/05 | 09:00-11:00 | L1 | Exercises:\\ //Erlang, CCS//\\ \\ 22 - Temporal and modal logics:\\ //linear temporal logic (LTL), linear structures models, shifting, LTL satisfaction, equivalence of formulas, automata-like models// | {{ :magistraleinformatica:psc:06_-_erlang_-_ccs-2025.pdf |Exercises 06}}\\ {{ :magistraleinformatica:psc:2025-05-09_-_22a_-_ltl_ctl.pdf |Lecture 22a}} | |
| | 28 | Tue | 13/05 | 09:00-11:00 | E | 24 - Pi-calculus:\\ //name mobility, free names, bound names, syntax and operational semantics, scope extrusion, early and late bisimilarities, weak semantics// | Lecture 24 | | | 28 | Tue | 13/05 | 09:00-11:00 | E | 22 - Temporal and modal logics (ctd.):\\ //computational tree logic (CTL* and CTL), infinite trees, infinite paths, branching structure, CTL* satisfaction, equivalence of formulas, CTL formulas, expressiveness comparison, mu-calculus, positive normal form, least and greatest fixpoints, invariant properties, possibly properties, mu-calculus with labels// | {{ :magistraleinformatica:psc:2025-05-09_-_22a_-_ltl_ctl.pdf |Lecture 22a}}\\ {{ :magistraleinformatica:psc:2025-05-13_-_22b_-_mu_calculus.pdf |Lecture 22b}} | |
| | 29 | Thu | 15/05 | 14:00-16:00 | C1 | | | | | 29 | Thu | 15/05 | 14:00-16:00 | C1 | 23 - GoogleGo:\\ //an overview//\\ \\ GoogleGo playground:\\ //Go principles, variable declaration, type conversion, multiple assignments, type inference, imports, packages and public names, named return values, naked return, multiple results, conditionals and loops, pointers, struct, receiver arguments and methods, interfaces, goroutines, bidirectional channels, channel types, send, receive, asynchronous communication with buffering, close, select, communicating communication means, range, handling multiple senders, concurrent prime sieve// | {{ :magistraleinformatica:psc:2025-05-15_-_23_-_google_go.pdf |Lecture 23}}\\ [[http://golang.org/|Google Go]]\\ {{ :magistraleinformatica:psc:go-session-2025.zip |go session}} | |
| | 30 | Fri | 16/05 | 09:00-11:00 | L1 | Exercises:\\ //logics, GoogleGo, pi-calculus//\\ \\ 25 - Measure theory and Markov chains:\\ //probability space, random variables, stochastic processes, homogeneous Markov chains, DTMC, DTMC as matrices, DTMC as PTS, next state probability, ergodic DTMC, steady state distribution, finite path probability// | Exercises 07\\ Lecture 25a | | | 30 | Fri | 16/05 | 09:00-11:00 | L1 | 24 - Pi-calculus:\\ //name mobility, free names, bound names, syntax and operational semantics, scope extrusion, early and late bisimilarities, weak semantics// | {{ :magistraleinformatica:psc:2025-05-16_-_24_-_pi_calculus.pdf |Lecture 24}} | |
| | 31 | Tue | 20/05 | 09:00-11:00 | E | 25 - Measure theory and Markov chains (ctd):\\ //negative exponential distribution, CTMC, embedded DTMC, infinitesimal generator matrix, CTMC stationary distribution//\\ \\ 26 - Probabilistic bisimilarities:\\ //bisimilarity revisited, reachability predicate, CTMC bisimilarity, DTMC bisimilarity, Markov chains with actions, probabilistic reactive systems, bisimilarity for reactive systems, Larsen-Skou logic// | Lecture 25b\\ Lecture 26 | | | - | Tue | 20/05 | 09:00-11:00 | E | **University closed (due to Tour of Italy)** | | |
| | 32 | Thu | 22/05 | 14:00-16:00 | C1 | 27 - PEPA:\\ //motivation, basic ideas, PEPA workflow, PEPA syntax, cooperation combinator, bounded capacity, apparent rate, PEPA operational semantics, performance analysis, reward structures// | Lecture 27\\ [[http://www.dcs.ed.ac.uk/pepa/|PEPA]] | | | 31 | Thu | 22/05 | 14:00-16:00 | C1 | Exercises:\\ //logics, GoogleGo, pi-calculus//\\ \\ 25 - Measure theory and Markov chains:\\ //probability space, random variables, stochastic processes, homogeneous Markov chains, DTMC, DTMC as matrices, DTMC as PTS, next state probability, ergodic DTMC, steady state distribution, finite path probability// | {{ :magistraleinformatica:psc:07_-_logics_-_googlego_-_pi-2025.pdf |Exercises 07}}\\ {{ :magistraleinformatica:psc:2025-05-22_-_25a_-_dtmc.pdf |Lecture 25a}} | |
| | 33 | Fri | 23/05 | 09:00-11:00 | L1 | Exercises:\\ //Markov chains, probabilistic systems, PEPA// | Exercises 08 | | | 32 | Fri | 23/05 | 09:00-11:00 | L1 | 25 - Measure theory and Markov chains (ctd):\\ //negative exponential distribution, CTMC, embedded DTMC, infinitesimal generator matrix, CTMC stationary distribution//\\ \\ 26 - Probabilistic bisimilarities:\\ //bisimilarity revisited, reachability predicate, CTMC bisimilarity, DTMC bisimilarity, Markov chains with actions, probabilistic reactive systems, bisimilarity for reactive systems, Larsen-Skou logic// | {{ :magistraleinformatica:psc:2025-05-23_-_25b_-_ctmc.pdf |Lecture 25b}}\\ {{ :magistraleinformatica:psc:2025-05-23_-_26_-_probabilistic_bisimilarities.pdf |Lecture 26}} | |
| | 34 | Tue | 27/05 | 09:00-11:00 | E | Exercises:\\ //Samples from exam exercises// | | | | 33 | Tue | 27/05 | 09:00-11:00 | E | 27 - PEPA:\\ //motivation, basic ideas, PEPA workflow, PEPA syntax, cooperation combinator, bounded capacity, apparent rate, PEPA operational semantics, performance analysis, reward structures// | {{ :magistraleinformatica:psc:2025-05-27_-_27_-_pepa.pdf |Lecture 27}}\\ [[http://www.dcs.ed.ac.uk/pepa/|PEPA]] | |
| | 35 | Thu | 29/05 | 14:00-16:00 | C1 | Mini-projects:\\ //discussion// | | | | 34 | Thu | 29/05 | 14:00-16:00 | C1 | Exercises:\\ //Markov chains, probabilistic systems, PEPA// | {{ :magistraleinformatica:psc:08_-_probability_-_2025.pdf |Exercises 08}} | |
| | 36 | Fri | 30/05 | 09:00-11:00 | L1 | Mini-projects:\\ //discussion// | | | | 35 | Fri | 30/05 | 09:00-11:00 | L1 | Exercises:\\ //Samples from exam exercises//\\ \\ Mini-projects:\\ //discussion// | | |
| | End | | | | | | | | | End | | | | | | | |
| |
