| Entrambe le parti precedenti la revisioneRevisione precedenteProssima revisione | Revisione precedente |
| magistraleinformatica:psc:start [29/04/2025 alle 12:23 (3 mesi fa)] – [Lectures (2nd part)] Roberto Bruni | magistraleinformatica:psc:start [27/06/2025 alle 10:59 (4 settimane fa)] (versione attuale) – [Oral Exams: schedule] Roberto Bruni |
|---|
| * problem solving: the ability to solve some simple exercises, and | * problem solving: the ability to solve some simple exercises, and |
| * understanding: the ability to discuss the reading matter thoughtfully and with propriety of expression. | * understanding: the ability to discuss the reading matter thoughtfully and with propriety of expression. |
| |
| ---- | |
| |
| ==== Oral Exams: schedule ==== | |
| |
| See the channel **Exams** in the Microsoft Teams platform | |
| |
| ---- | ---- |
| | - | 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// | Lecture 22b | | | 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 | 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 | | | 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 | 24 - Pi-calculus:\\ //name mobility, free names, bound names, syntax and operational semantics, scope extrusion, early and late bisimilarities, weak semantics// | Lecture 24 | | | 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 | | | | | | | |
| |
