| Entrambe le parti precedenti la revisioneRevisione precedenteProssima revisione | Revisione precedente |
| magistraleinformatica:psc:start [29/04/2025 alle 12:30 (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// | {{ :magistraleinformatica:psc:2025-04-29_-_18c_-_ccs_bis_as_fix.pdf |Lecture 18c}}\\ Lecture 19\\ Lecture 20\\ Lecture 21 | | | 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 | 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) | Lecture 21\\ [[http://caal.cs.aau.dk/|CAAL]]\\ CAAL session | | | 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 | Exercises:\\ //Erlang, CCS//\\ \\ 22 - Temporal and modal logics:\\ //linear temporal logic (LTL), linear structures models, shifting, LTL satisfaction, equivalence of formulas, automata-like models// | Exercises 06\\ Lecture 22a | | | 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 | 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// | Lecture 22a\\ Lecture 22b | | | 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 | 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 23\\ [[http://golang.org/|Google Go]]\\ go session | | | 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 | 24 - Pi-calculus:\\ //name mobility, free names, bound names, syntax and operational semantics, scope extrusion, early and late bisimilarities, weak semantics// | Lecture 24 | | | 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 | 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 | | | - | Tue | 20/05 | 09:00-11:00 | E | **University closed (due to Tour of Italy)** | | |
| | 32 | Thu | 22/05 | 14:00-16:00 | C1 | 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 | | | 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 | 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]] | | | 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 | Exercises:\\ //Markov chains, probabilistic systems, PEPA// | Exercises 08 | | | 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 | E | Exercises:\\ //Samples from exam exercises// | | | | 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 | | | | | | | |
| |
