Differenze

Queste sono le differenze tra la revisione selezionata e la versione attuale della pagina.

--- magistraleinformatica:psc:start [27/04/2025 alle 22:01 (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
@@ Linea 127: / Linea 127: @@
 | 20 | Thu | 10/04 | 14:00-16:00 | C1 | Exercises:\\ //HOFL, domains//\\ \\ 16 - Erlang:\\ //an overview//  | {{ :magistraleinformatica:psc:2025-04-10_-_16_-_erlang.pdf |Lecture 16}}\\ [[http://www.erlang.org/|Erlang]] |
 |  - | Fri | 11/04 | 09:00-11:00 | L1 | **Canceled due to graduation event** |  |
-| 21 | Tue | 15/04 | 09:00-11:00 | E | Erlang erl:\\ //numbers, atoms, tuples, lists, terms, variables, term comparison, pattern matching, list comprehension, modules, functions, guards, higher order, recursion, pids, spawn, self, send, receive, examples//\\ \\ 17 - CCS:\\ //Introduction to concurrency// | [[http://www.erlang.org/|Erlang]]\\ erl session\\ Lecture 17a |
+| 21 | Tue | 15/04 | 09:00-11:00 | E | Erlang erl:\\ //numbers, atoms, tuples, lists, terms, variables, term comparison, pattern matching, list comprehension, modules, functions, guards, higher order, recursion, pids, spawn, self, send, receive, examples//\\ \\ 17 - CCS:\\ //Introduction to concurrency// | [[http://www.erlang.org/|Erlang]]\\ {{ :magistraleinformatica:psc:2025-04-15_-_16a_-_erlang_session.pdf |erl session}}\\ {{ :magistraleinformatica:psc:2025-04-15_-_17a_-_ccs.pdf |Lecture 17a}} |
-| 22 | Thu | 17/04 | 14:00-16:00 | C1 | 17 - CCS (ctd.)\\ //Syntax, operational semantics, value passing, finitely branching processes, guarded processes// | Lecture 17a\\ Lecture 17b |
+| 22 | Thu | 17/04 | 14:00-16:00 | C1 | 17 - CCS (ctd.)\\ //Syntax, operational semantics, value passing, finitely branching processes, guarded processes// | {{ :magistraleinformatica:psc:2025-04-15_-_17a_-_ccs.pdf |Lecture 17a}}\\ {{ :magistraleinformatica:psc:2025-04-17_-_17b_-_ccs_guarded.pdf |Lecture 17b}} |
 |  - | Fri | 18/04 | 09:00-11:00 | L1 | **Easter holidays** |  |
 |  - | Tue | 22/04 | 09:00-11:00 | E | **Easter holidays** |  |
-| 23 | Thu | 24/04 | 14:00-16:00 | C1 | 18 - Bisimulation:\\ //abstract semantics, graph isomorphism, trace equivalence, bisimulation game, strong bisimulation// | Lecture 18a\\ Lecture 18b\\ Lecture 18c\\ Lecture 19\\ Lecture 20 |
+| 23 | Thu | 24/04 | 14:00-16:00 | C1 | 18 - Bisimulation:\\ //abstract semantics, graph isomorphism, trace equivalence, bisimulation game, strong bisimulation// | {{ :magistraleinformatica:psc:2025-04-24_-_18a_-_ccs_abstract.pdf |Lecture 18a}}\\ {{ :magistraleinformatica:psc:2025-04-24_-_18b_-_ccs_bisimulation.pdf |Lecture 18b}} |
 |  - | Fri | 25/04 | 09:00-11:00 | L1 | **Italian liberation day** |  |
-| 24 | Tue | 29/04 | 09:00-11:00 | E | 18 - Bisimulation (ctd.):\\ //strong bisimilarity, strong bisimilarity is an equivalence, strong bisimilarity is a bisimulation, strong bisimilarity is the coarsest strong bisimulation, strong bisimilarity is a congruence, some laws for strong bisimilarity, strong bisimilarity as a fixpoint, strong bisimilarity as a fixpoint, Phi operator, Phi is monotone, Phi is continuous (on finitely branching processes), 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) | Lecture 21\\ [[http://caal.cs.aau.dk/|CAAL]]\\ CAAL session |
+| 24 | Tue | 29/04 | 09:00-11:00 | E | 18 - Bisimulation (ctd.):\\ //strong bisimilarity, strong bisimilarity is an equivalence, strong bisimilarity is a bisimulation, strong bisimilarity is the coarsest strong bisimulation, strong bisimilarity is a congruence, some laws for strong bisimilarity, strong bisimilarity as a fixpoint, strong bisimilarity as a fixpoint, Phi operator, Phi is monotone, Phi is continuous (on finitely branching processes)// | {{ :magistraleinformatica:psc:2025-04-24_-_18b_-_ccs_bisimulation.pdf |Lecture 18b}}\\ {{ :magistraleinformatica:psc:2025-04-29_-_18c_-_ccs_bis_as_fix.pdf |Lecture 18c}} |
 |  - | Thu | 01/05 | 14:00-16:00 | C1 | **International labour day** |  |
 |  - | Fri | 02/05 | 09:00-11:00 | L1 | **Long weekend** |  |
-| 25 | Tue | 06/05 | 09:00-11:00 | E | 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 |
+| 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 | 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//   | Exercises 07\\ Lecture 25a |
+| 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 | 25 - Measure theory and Markov chains (ctd):\\ //next state probability, ergodic DTMC, steady state distribution, finite path probability, 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// | Lecture 25a\\ Lecture 25b\\ Lecture 26 |
+| 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 | 26 - Probabilistic bisimilarities (ctd.):\\ //probabilistic reactive systems, bisimilarity for reactive systems, Larsen-Skou logic//\\ \\ 27 - PEPA:\\ //motivation, basic ideas, PEPA workflow, PEPA syntax, cooperation combinator, bounded capacity, apparent rate, PEPA operational semantics, performance analysis, reward structures// | Lecture 26\\ Lecture 27\\ [[http://www.dcs.ed.ac.uk/pepa/|PEPA]] |
+| - | Tue | 20/05 | 09:00-11:00 | E | **University closed (due to Tour of Italy)** |  |
-| 32 | Thu | 22/05 | 14:00-16:00 | C1 | Exercises:\\ //Markov chains, probabilistic systems, PEPA// | Exercises 08 |
+| 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:\\ //Samples from exam exercises// |  |
+| 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 | Mini-projects:\\ //discussion// |  |
+| 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 |  |  |  |  |  |  |