| Entrambe le parti precedenti la revisioneRevisione precedenteProssima revisione | Revisione precedente |
| magistraleinformatica:psc:2020-21:start [05/02/2022 alle 16:28 (3 anni fa)] – [Exam sessions] Roberto Bruni | magistraleinformatica:psc:2020-21:start [05/02/2022 alle 16:55 (3 anni fa)] (versione attuale) – [Lectures (1st part)] Roberto Bruni |
|---|
| | 7 | Mon | 01/03 | 16:00-18:00 | Teams | 05 - Induction (ctd.):\\ //determinacy of arithmetic expressions, structural induction over many-sorted signatures, termination of boolean expressions, memories, update operation, operational semantics of commands, divergence// | {{ :magistraleinformatica:psc:2021-03-01_-_05b_-_more_induction.pdf |Lecture 05b}} | | | 7 | Mon | 01/03 | 16:00-18:00 | Teams | 05 - Induction (ctd.):\\ //determinacy of arithmetic expressions, structural induction over many-sorted signatures, termination of boolean expressions, memories, update operation, operational semantics of commands, divergence// | {{ :magistraleinformatica:psc:2021-03-01_-_05b_-_more_induction.pdf |Lecture 05b}} | |
| | 8 | Wed | 03/03 | 14:00-16:00 | Teams | 05 - Induction (ctd.):\\ //rule for divergence, limits of structural induction, induction on derivations, rule induction, determinacy of commands// | {{ :magistraleinformatica:psc:2021-03-03_-_05c_-_rule_induction.pdf |Lecture 05c}} | | | 8 | Wed | 03/03 | 14:00-16:00 | Teams | 05 - Induction (ctd.):\\ //rule for divergence, limits of structural induction, induction on derivations, rule induction, determinacy of commands// | {{ :magistraleinformatica:psc:2021-03-03_-_05c_-_rule_induction.pdf |Lecture 05c}} | |
| | 9 | Fri | 05/03 | 14:00-16:00 | Teams | Exercises:\\ //induction, termination, determinacy, divergence//\\ \\ 06 - Equivalence:\\ //operational equivalence, concrete equivalences, parametric equivalences, equivalence and divergence// | {{ :magistraleinformatica:psc:2021-03-05_-_exercises_02.pdf |Exercises 02}}\\ \\ {{ :magistraleinformatica:psc:2021-03-05_-_06_-_equivalence.pdf |Lecture 06}} | | | 9 | Fri | 05/03 | 14:00-16:00 | Teams | Exercises:\\ //induction, termination, determinacy, divergence//\\ \\ 06 - Equivalence:\\ //operational equivalence, concrete equivalences, parametric equivalences, equivalence and divergence// | {{ :magistraleinformatica:psc:2020-21:02_-_properties.pdf |Exercises 02}}\\ \\ {{ :magistraleinformatica:psc:2021-03-05_-_06_-_equivalence.pdf |Lecture 06}} | |
| | 10 | Mon | 08/03 | 16:00-18:00 | Teams | 07 - Induction and recursion:\\ //well-founded recursion, denotational semantics of arithmetic expressions, consistency of operational and denotational semantics for arithmetic expressions, lexicographic precedence relation, Ackermann function, fixpoint equations// | {{ :magistraleinformatica:psc:2021-03-08_-_07_-_recursion.pdf |Lecture 07}} | | | 10 | Mon | 08/03 | 16:00-18:00 | Teams | 07 - Induction and recursion:\\ //well-founded recursion, denotational semantics of arithmetic expressions, consistency of operational and denotational semantics for arithmetic expressions, lexicographic precedence relation, Ackermann function, fixpoint equations// | {{ :magistraleinformatica:psc:2021-03-08_-_07_-_recursion.pdf |Lecture 07}} | |
| | 11 | Wed | 10/03 | 14:00-16:00 | Teams | Exercises:\\ //x++, arithmetic expressions with side-effects//\\ \\ 08 - Partial orders and fixpoints:\\ //partial orders, Hasse diagrams, chains, least element, minimal element, bottom element, upper bounds, least upper bound, chains, limits, complete partial orders, powerset completeness// | {{ :magistraleinformatica:psc:2021-03-10_-_08a_-_cpo.pdf |Lecture 08a}} | | | 11 | Wed | 10/03 | 14:00-16:00 | Teams | Exercises:\\ //x++, arithmetic expressions with side-effects//\\ \\ 08 - Partial orders and fixpoints:\\ //partial orders, Hasse diagrams, chains, least element, minimal element, bottom element, upper bounds, least upper bound, chains, limits, complete partial orders, powerset completeness// | {{ :magistraleinformatica:psc:2021-03-10_-_08a_-_cpo.pdf |Lecture 08a}} | |
| | 12 | Fri | 12/03 | 14:00-16:00 | Teams | 08 - Partial orders and fixpoints (ctd.):\\ //prefix independence, CPO of partial functions, monotonicity, continuity, Kleene's fixpoint theorem// | {{ :magistraleinformatica:psc:2021-03-12_-_08b_-_kleene.pdf |Lecture 08b}} | | | 12 | Fri | 12/03 | 14:00-16:00 | Teams | 08 - Partial orders and fixpoints (ctd.):\\ //prefix independence, CPO of partial functions, monotonicity, continuity, Kleene's fixpoint theorem// | {{ :magistraleinformatica:psc:2021-03-12_-_08b_-_kleene.pdf |Lecture 08b}} | |
| | 13 | Mon | 15/03 | 16:00-18:00 | Teams | 08 - Partial orders and fixpoints (ctd.):\\ //recursive definitions of partial functions as logical systems, immediate consequences operator, set of theorems as fixpoint//\\ \\ 09 - Denotational semantics:\\ //lambda-notation, free variables, capture-avoiding substitutions, alpha-conversion, beta rule, conditionals// | {{ :magistraleinformatica:psc:2021-03-15_-_08c_-_ico.pdf |Lecture 08c}}\\ \\ {{ :magistraleinformatica:psc:2021-03-15_-_09_-_denotational_imp.pdf |Lecture 09}} | | | 13 | Mon | 15/03 | 16:00-18:00 | Teams | 08 - Partial orders and fixpoints (ctd.):\\ //recursive definitions of partial functions as logical systems, immediate consequences operator, set of theorems as fixpoint//\\ \\ 09 - Denotational semantics:\\ //lambda-notation, free variables, capture-avoiding substitutions, alpha-conversion, beta rule, conditionals// | {{ :magistraleinformatica:psc:2021-03-15_-_08c_-_ico.pdf |Lecture 08c}}\\ \\ {{ :magistraleinformatica:psc:2021-03-15_-_09_-_denotational_imp.pdf |Lecture 09}} | |
| | 14 | Wed | 17/03 | 14:00-16:00 | Teams | 09 - Denotational semantics (ctd.):\\ //denotational semantics of commands, fixpoint computation//\\ \\ 10 - Consistency:\\ //denotational equivalence, congruence, compositionality principle, consistency of commands, correctness, completeness//\\ \\ Exercises:\\ //well-founded recursion, posets, semantics// | {{ :magistraleinformatica:psc:2021-03-17_-_10_-_consistency_imp.pdf |Lecture 10}}\\ \\ {{ :magistraleinformatica:psc:2021-03-17_-_exercises_03.pdf |Exercises 03}} | | | 14 | Wed | 17/03 | 14:00-16:00 | Teams | 09 - Denotational semantics (ctd.):\\ //denotational semantics of commands, fixpoint computation//\\ \\ 10 - Consistency:\\ //denotational equivalence, congruence, compositionality principle, consistency of commands, correctness, completeness//\\ \\ Exercises:\\ //well-founded recursion, posets, semantics// | {{ :magistraleinformatica:psc:2021-03-17_-_10_-_consistency_imp.pdf |Lecture 10}}\\ \\ {{ :magistraleinformatica:psc:2020-21:03_-_poset.pdf |Exercises 03}} | |
| | 15 | Fri | 19/03 | 14:00-16:00 | Teams | 10 - Consistency (ctd.):\\ //completeness//\\ \\ Exercises:\\ //well-founded recursion, rule induction//\\ \\ 11 - Haskell:\\ //an overview// | {{ :magistraleinformatica:psc:2021-03-19_-_11_-_haskell.pdf |Lecture 11}} | | | 15 | Fri | 19/03 | 14:00-16:00 | Teams | 10 - Consistency (ctd.):\\ //completeness//\\ \\ Exercises:\\ //well-founded recursion, rule induction//\\ \\ 11 - Haskell:\\ //an overview// | {{ :magistraleinformatica:psc:2021-03-19_-_11_-_haskell.pdf |Lecture 11}} | |
| | 16 | Mon | 22/03 | 16:00-18:00 | Teams | Haskell ghci:\\ //basics, lambda, tuples, lists, list comprehension, guards, pattern matching, partial application, recursive definitions, zip, exercises//\\ {{ :magistraleinformatica:psc:ghci-session1-2021.txt.zip |ghci session 01}} | [[https://www.haskell.org/|Haskell]] | | | 16 | Mon | 22/03 | 16:00-18:00 | Teams | Haskell ghci:\\ //basics, lambda, tuples, lists, list comprehension, guards, pattern matching, partial application, recursive definitions, zip, exercises//\\ {{ :magistraleinformatica:psc:ghci-session1-2021.txt.zip |ghci session 01}} | [[https://www.haskell.org/|Haskell]] | |
| | 17 | Wed | 24/03 | 14:00-16:00 | Teams | Haskell ghci (ctd.):\\ //costrutto let-in, costrutto where, map, filter, fixpoint operator, exercises//\\ {{ :magistraleinformatica:psc:ghci-session2-2021.txt.zip |ghci session 02}} | [[https://www.haskell.org/|Haskell]] | | | 17 | Wed | 24/03 | 14:00-16:00 | Teams | Haskell ghci (ctd.):\\ //costrutto let-in, costrutto where, map, filter, fixpoint operator, exercises//\\ {{ :magistraleinformatica:psc:ghci-session2-2021.txt.zip |ghci session 02}} | [[https://www.haskell.org/|Haskell]] | |
| | 18 | Fri | 26/03 | 14:00-16:00 | Teams | Haskell ghci (ctd.):\\ //tail recursion, folds, application, function composition, data types, type classes, recursive data structures, derived instances, exercises//\\ {{ :magistraleinformatica:psc:ghci-session3-2021.txt.zip |ghci session 03}} | [[https://www.haskell.org/|Haskell]] | | | 18 | Fri | 26/03 | 14:00-16:00 | Teams | Haskell ghci (ctd.):\\ //tail recursion, folds, application, function composition, data types, type classes, recursive data structures, derived instances, exercises//\\ {{ :magistraleinformatica:psc:ghci-session3-2021.txt.zip |ghci session 03}} | [[https://www.haskell.org/|Haskell]] | |
| | 19 | Mon | 29/03 | 16:00-18:00 | Teams | Exercises:\\ //Haskell//\\ \\ 12 - HOFL:\\ //syntax, type system, type checking// | {{ :magistraleinformatica:psc:2021-03-29_-_12a_-_hofl_types.pdf |Lecture 12a}} | | | 19 | Mon | 29/03 | 16:00-18:00 | Teams | Exercises:\\ //Haskell//\\ \\ 12 - HOFL:\\ //syntax, type system, type checking// | {{ :magistraleinformatica:psc:2020-21:04_-_haskell.pdf |Exercises 04}}\\ {{ :magistraleinformatica:psc:2021-03-29_-_12a_-_hofl_types.pdf |Lecture 12a}} | |
| | 20 | Wed | 31/03 | 14:00-16:00 | Teams | 12 - HOFL (ctd.):\\ //type inference, principal type, canonical forms, operational semantics, lazy vs eager evaluation// | Exercises 04\\ {{ :magistraleinformatica:psc:2021-03-31_-_12b_-_hofl_operational.pdf |Lecture 12b}} | | | 20 | Wed | 31/03 | 14:00-16:00 | Teams | 12 - HOFL (ctd.):\\ //type inference, principal type, canonical forms, operational semantics, lazy vs eager evaluation// | {{ :magistraleinformatica:psc:2021-03-31_-_12b_-_hofl_operational.pdf |Lecture 12b}} | |
| |
| |
| | 22 | Fri | 09/04 | 14:00-16:00 | Teams | 13 - Domain theory (ctd.):\\ //functional domains, lifting, continuity theorems, apply, fix, let notation// | {{ :magistraleinformatica:psc:2021-04-09_-_13c_-_continuity_theorems.pdf |Lecture 13c}} | | | 22 | Fri | 09/04 | 14:00-16:00 | Teams | 13 - Domain theory (ctd.):\\ //functional domains, lifting, continuity theorems, apply, fix, let notation// | {{ :magistraleinformatica:psc:2021-04-09_-_13c_-_continuity_theorems.pdf |Lecture 13c}} | |
| | 23 | Mon | 12/04 | 16:00-18:00 | Teams | 14 - Denotational semantics of HOFL:\\ //definition and examples, type consistency, substitution lemma, compositionality and other properties// | {{ :magistraleinformatica:psc:2021-04-12_-_14_-_hofl_denotational.pdf |Lecture 14}} | | | 23 | Mon | 12/04 | 16:00-18:00 | Teams | 14 - Denotational semantics of HOFL:\\ //definition and examples, type consistency, substitution lemma, compositionality and other properties// | {{ :magistraleinformatica:psc:2021-04-12_-_14_-_hofl_denotational.pdf |Lecture 14}} | |
| | 24 | Wed | 14/04 | 14:00-16:00 | Teams | 15 - Consistency of HOFL:\\ //Counterexample to completeness, correctness of the operational semantics, operational convergence, denotational convergence, operational convergence implies denotational convergence (and vice versa), operational and denotational equivalence, correspondence for type int, unlifted semantics//\\ \\ Exercises:\\ //HOFL, domains// | {{ :magistraleinformatica:psc:2021-04-14_-_15_-_consistency_hofl.pdf |Lecture 15}}\\ {{ :magistraleinformatica:psc:2021-04-14_-_exercises_05.pdf |Exercises 05}} | | | 24 | Wed | 14/04 | 14:00-16:00 | Teams | 15 - Consistency of HOFL:\\ //Counterexample to completeness, correctness of the operational semantics, operational convergence, denotational convergence, operational convergence implies denotational convergence (and vice versa), operational and denotational equivalence, correspondence for type int, unlifted semantics//\\ \\ Exercises:\\ //HOFL, domains// | {{ :magistraleinformatica:psc:2021-04-14_-_15_-_consistency_hofl.pdf |Lecture 15}}\\ {{ :magistraleinformatica:psc:2020-21:05_-_hofl.pdf |Exercises 05}} | |
| | 25 | Fri | 16/04 | 14:00-16:00 | Teams | Exercises:\\ //HOFL//\\ \\ 16 - Erlang:\\ //an overview// | {{ :magistraleinformatica:psc:2021-04-16_-_16_-_erlang.pdf |Lecture 16}} | | | 25 | Fri | 16/04 | 14:00-16:00 | Teams | Exercises:\\ //HOFL//\\ \\ 16 - Erlang:\\ //an overview// | {{ :magistraleinformatica:psc:2021-04-16_-_16_-_erlang.pdf |Lecture 16}} | |
| | 26 | Mon | 19/04 | 16:00-18:00 | Teams | 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//\\ {{ :magistraleinformatica:psc:erl_2021.zip |erl session}} | [[http://www.erlang.org/|Erlang]] | | | 26 | Mon | 19/04 | 16:00-18:00 | Teams | 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//\\ {{ :magistraleinformatica:psc:erl_2021.zip |erl session}} | [[http://www.erlang.org/|Erlang]] | |
| | 31 | Fri | 30/04 | 14:00-16:00 | Teams | 20 - Weak Semantics:\\ //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)//\\ {{ :magistraleinformatica:psc:buffers_in_caal_2021.zip |CAAL session 01}} (copy the text and paste it in the Edit panel) | {{ :magistraleinformatica:psc:2021-04-30_-_21_-_ccs_at_work.pdf |Lecture 21}}\\ [[http://caal.cs.aau.dk/|CAAL]] | | | 31 | Fri | 30/04 | 14:00-16:00 | Teams | 20 - Weak Semantics:\\ //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)//\\ {{ :magistraleinformatica:psc:buffers_in_caal_2021.zip |CAAL session 01}} (copy the text and paste it in the Edit panel) | {{ :magistraleinformatica:psc:2021-04-30_-_21_-_ccs_at_work.pdf |Lecture 21}}\\ [[http://caal.cs.aau.dk/|CAAL]] | |
| | 32 | Mon | 03/05 | 16:00-18:00 | Teams | 21 - CCS at work:\\ //modelling and verification of mutual exclusion algorithms with CCS and CAAL//\\ {{ :magistraleinformatica:psc:peterson_hyman_in_caal_2021.zip |CAAL session 02}} (copy the text and paste it in the Edit panel) | [[http://caal.cs.aau.dk/|CAAL]] | | | 32 | Mon | 03/05 | 16:00-18:00 | Teams | 21 - CCS at work:\\ //modelling and verification of mutual exclusion algorithms with CCS and CAAL//\\ {{ :magistraleinformatica:psc:peterson_hyman_in_caal_2021.zip |CAAL session 02}} (copy the text and paste it in the Edit panel) | [[http://caal.cs.aau.dk/|CAAL]] | |
| | 33 | Wed | 05/05 | 14:00-16:00 | Teams | Exercises:\\ //CAAL, Erlang, CCS// | {{ :magistraleinformatica:psc:2021-05-05_-_exercises_06.pdf |Exercises 06}}\\ [[http://caal.cs.aau.dk/|CAAL]] | | | 33 | Wed | 05/05 | 14:00-16:00 | Teams | Exercises:\\ //CAAL, Erlang, CCS// | {{ :magistraleinformatica:psc:2020-21:06_-_erlang_-_ccs.pdf |Exercises 06}}\\ [[http://caal.cs.aau.dk/|CAAL]] | |
| | 34 | Fri | 07/05 | 14:00-16:00 | Teams | Exercises:\\ //CCS//\\ \\ 22 - Temporal and modal logics:\\ //linear temporal logic (LTL), linear structures models, shifting, LTL satisfaction, equivalence of formulas, automata-like models// | {{ :magistraleinformatica:psc:2021-05-07_-_22a_-_ltl_ctl.pdf |Lecture 22a}} | | | 34 | Fri | 07/05 | 14:00-16:00 | Teams | Exercises:\\ //CCS//\\ \\ 22 - Temporal and modal logics:\\ //linear temporal logic (LTL), linear structures models, shifting, LTL satisfaction, equivalence of formulas, automata-like models// | {{ :magistraleinformatica:psc:2021-05-07_-_22a_-_ltl_ctl.pdf |Lecture 22a}} | |
| | 35 | Mon | 10/05 | 16:00-18:00 | Teams | 22 - Temporal and modal logics:\\ //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:2021-05-10_-_22b_-_mu_calculus.pdf |Lecture 22b}} | | | 35 | Mon | 10/05 | 16:00-18:00 | Teams | 22 - Temporal and modal logics:\\ //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:2021-05-10_-_22b_-_mu_calculus.pdf |Lecture 22b}} | |
| | 36 | Wed | 12/05 | 14:00-16:00 | Teams | 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\\ {{ :magistraleinformatica:psc:go-session1-2021.zip |go session 01}} | {{ :magistraleinformatica:psc:2021-05-12_-_23_-_google_go.pdf |Lecture 23}}\\ [[http://golang.org/|Google Go]] | | | 36 | Wed | 12/05 | 14:00-16:00 | Teams | 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\\ {{ :magistraleinformatica:psc:go-session1-2021.zip |go session 01}} | {{ :magistraleinformatica:psc:2021-05-12_-_23_-_google_go.pdf |Lecture 23}}\\ [[http://golang.org/|Google Go]] | |
| | 37 | Fri | 14/05 | 14:00-16:00 | Teams | GoogleGo playground:\\ range, handling multiple senders, concurrent prime sieve\\ {{ :magistraleinformatica:psc:go-session2-2021.zip |go session 02}}\\ \\ 24 - Pi-calculus:\\ //name mobility, free names, bound names, syntax and operational semantics, scope extrusion, early and late bisimilarities, weak semantics// | {{ :magistraleinformatica:psc:2021-05-14_-_24_-_pi_calculus.pdf |Lecture 24}} | | | 37 | Fri | 14/05 | 14:00-16:00 | Teams | GoogleGo playground:\\ range, handling multiple senders, concurrent prime sieve\\ {{ :magistraleinformatica:psc:go-session2-2021.zip |go session 02}}\\ \\ 24 - Pi-calculus:\\ //name mobility, free names, bound names, syntax and operational semantics, scope extrusion, early and late bisimilarities, weak semantics// | {{ :magistraleinformatica:psc:2021-05-14_-_24_-_pi_calculus.pdf |Lecture 24}} | |
| | 38 | Mon | 17/05 | 16:00-18:00 | Teams | Exercises:\\ //logics, GoogleGo, pi-calculus//\\ \\ 25 - Measure theory and Markov chains:\\ //probability space, random variables, stochastic processes// | {{ :magistraleinformatica:psc:2021-05-17_-_exercises_07.pdf |Exercises 07}}\\ {{ :magistraleinformatica:psc:2021-05-17_-_25a_-_dtmc.pdf |Lecture 25a}} | | | 38 | Mon | 17/05 | 16:00-18:00 | Teams | Exercises:\\ //logics, GoogleGo, pi-calculus//\\ \\ 25 - Measure theory and Markov chains:\\ //probability space, random variables, stochastic processes// | {{ :magistraleinformatica:psc:2020-21:07_-_logics_-_googlego_-_pi.pdf |Exercises 07}}\\ {{ :magistraleinformatica:psc:2021-05-17_-_25a_-_dtmc.pdf |Lecture 25a}} | |
| | 39 | Wed | 19/05 | 14:00-16:00 | Teams | 25 - Measure theory and Markov chains:\\ //homogeneous Markov chains, DTMC, DTMC as matrices, DTMC as PTS, next state probability, finite path probability, ergodic DTMC, steady state distribution, negative exponential distribution, CTMC, embedded DTMC, infinitesimal generator matrix, CTMC stationary distribution// | {{ :magistraleinformatica:psc:2021-05-19_-_25b_-_ctmc.pdf |Lecture 25b}} | | | 39 | Wed | 19/05 | 14:00-16:00 | Teams | 25 - Measure theory and Markov chains:\\ //homogeneous Markov chains, DTMC, DTMC as matrices, DTMC as PTS, next state probability, finite path probability, ergodic DTMC, steady state distribution, negative exponential distribution, CTMC, embedded DTMC, infinitesimal generator matrix, CTMC stationary distribution// | {{ :magistraleinformatica:psc:2021-05-19_-_25b_-_ctmc.pdf |Lecture 25b}} | |
| | 40 | Fri | 21/05 | 14:00-16:00 | Teams | 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//\\ \\ 27 - PEPA:\\ //motivation, basic ideas, PEPA workflow, PEPA syntax, cooperation combinator, bounded capacity, apparent rate, PEPA operational semantics, performance analysis, reward structures//\\ \\ Exercises:\\ //Markov chains, probabilistic systems, PEPA// | {{ :magistraleinformatica:psc:2021-05-21_-_26_-_probabilistic_bisimilarities.pdf |Lecture 26}}\\ Lecture 27\\ Exercises 08\\ [[http://www.dcs.ed.ac.uk/pepa/|PEPA]] | | | 40 | Fri | 21/05 | 14:00-16:00 | Teams | 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//\\ \\ 27 - PEPA:\\ //motivation, basic ideas, PEPA workflow, PEPA syntax, cooperation combinator, bounded capacity, apparent rate, PEPA operational semantics, performance analysis, reward structures//\\ \\ Exercises:\\ //Markov chains, probabilistic systems, PEPA// | {{ :magistraleinformatica:psc:2021-05-21_-_26_-_probabilistic_bisimilarities.pdf |Lecture 26}}\\ {{ :magistraleinformatica:psc:2020-21:2021-05-21_-_27_-_pepa.pdf |Lecture 27}}\\ {{ :magistraleinformatica:psc:2020-21:08_-_probability.pdf |Exercises 08}}\\ [[http://www.dcs.ed.ac.uk/pepa/|PEPA]] | |
| | End | | | | | | | | | End | | | | | | | |
| |
