Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
didattica:magistrale:rtpsv:ay_1617:main [2017/02/01 12:27] luca [Study material] |
didattica:magistrale:rtpsv:ay_1617:main [2020/09/17 16:55] (current) |
||
|---|---|---|---|
| Line 124: | Line 124: | ||
| * Lecture of 25/01/2017 - Zones, forward reachability analysis with zones, time divergence, time locks, zeno paths. {{ :didattica:magistrale:rtpsv:ay_1617:luca.tesei_26-01-2017_19-33-48.pdf |Minutes of the lecture}}, {{ :didattica:magistrale:rtpsv:ay_1617:reachability_analysis_with_zones.pdf |Slides Zones}} {{ :didattica:magistrale:rtpsv:ay_1617:time_divergence_timelocks_zenoness.pdf |Slides Time Divergence, Timelocks, Zenoness}}. [[https://unicam.webex.com/unicam/lsr.php?RCID=dcf7b1fede13492fbf68a28d3eb136b6 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=830257830cf87fed39b24e4582bd0cb9|Link for downloading the lecture]] - Password to visualise and download the video: none | * Lecture of 25/01/2017 - Zones, forward reachability analysis with zones, time divergence, time locks, zeno paths. {{ :didattica:magistrale:rtpsv:ay_1617:luca.tesei_26-01-2017_19-33-48.pdf |Minutes of the lecture}}, {{ :didattica:magistrale:rtpsv:ay_1617:reachability_analysis_with_zones.pdf |Slides Zones}} {{ :didattica:magistrale:rtpsv:ay_1617:time_divergence_timelocks_zenoness.pdf |Slides Time Divergence, Timelocks, Zenoness}}. [[https://unicam.webex.com/unicam/lsr.php?RCID=dcf7b1fede13492fbf68a28d3eb136b6 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=830257830cf87fed39b24e4582bd0cb9|Link for downloading the lecture]] - Password to visualise and download the video: none | ||
| * Lecture of 26/01/2017 - TCTL, Model Checking for TCTL {{ :didattica:magistrale:rtpsv:ay_1617:tctl.pdf |Slides TCTL Model Checking}} - [[https://unicam.webex.com/unicam/lsr.php?RCID=fd9b358f34ad49d698228c31c82fb09a | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=78261b24cead2af81b3b3396cbfbb852|Link for downloading the lecture]] - Password to visualise and download the video: none | * Lecture of 26/01/2017 - TCTL, Model Checking for TCTL {{ :didattica:magistrale:rtpsv:ay_1617:tctl.pdf |Slides TCTL Model Checking}} - [[https://unicam.webex.com/unicam/lsr.php?RCID=fd9b358f34ad49d698228c31c82fb09a | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=78261b24cead2af81b3b3396cbfbb852|Link for downloading the lecture]] - Password to visualise and download the video: none | ||
| - | * Lecture of 01/02/2017 - Introduction to probabilistic systems and their verification. Definition of Discrete Time Markov Chain. Introduction to the tool PRISM. Examples of DTMC in PRISM, - [[https://unicam.webex.com/unicam/ldr.php?RCID=405a578a3cfb5ded991a12f9d74b6ee4 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=6e80b635f3cb266da01646f6b11369a5 |Link for downloading the lecture]] - Password to visualise and download the video: none | + | * Lecture of 01/02/2017 - Introduction to probabilistic systems and their verification. Definition of Discrete Time Markov Chain. Introduction to the tool PRISM. Examples of DTMC in PRISM. {{ :didattica:magistrale:rtpsv:ay_1617:luca.tesei_01-02-2017_12-25-06.pdf |Notes from the lecture}} - [[https://unicam.webex.com/unicam/ldr.php?RCID=405a578a3cfb5ded991a12f9d74b6ee4 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=6e80b635f3cb266da01646f6b11369a5 |Link for downloading the lecture]] - Password to visualise and download the video: none |
| - | * Lecture of 02/02/2017 - ... | + | * Lecture of 02/02/2017 - Definition of Cylinder Sets and of the probability measure on the set of paths of a DTMC. Formal syntax and semantics of PCTL. Introduction to Markov Decision Processes. {{ :didattica:magistrale:rtpsv:ay_1617:luca.tesei_02-02-2017_11-16-02.pdf |Notes form the lecture}} - [[https://unicam.webex.com/unicam/ldr.php?RCID=f23efe06edc31d6f1153d30e433e4629 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=83d03c57dc60ffe0a9f8a12a38fca648 |Link for downloading the lecture]] - Password to visualise and download the video: none |
| - | * Lecture of 08/02/2017 - ... | + | * Lecture of 08/02/2017 - Exponential Distributions. Continuous Time Markov Chains. Examples in PRISM. {{ :didattica:magistrale:rtpsv:ay_1617:negative_exponential_distributions._continuous_time_markov_chains.pdf |Slides}}, [[http://www.prismmodelchecker.org/tutorial/power.php | PRISM Tutorial and example]] - [[https://unicam.webex.com/unicam/ldr.php?RCID=75460821c878b5dee6cf4d1d742a3603 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=3b9da98ee7f50dbe3165abd04e3ebb84 |Link for downloading the lecture]] - Password to visualise and download the video: none |
| - | * Lecture of 09/02/2017 - ... | + | * Lecture of 09/02/2017 - Continuous Stochastic Logic. Reachability Probabilities in MDPs. {{ :didattica:magistrale:rtpsv:ay_1617:continuous_stochastic_logic.pdf |Slides CSL}}, {{ :didattica:magistrale:rtpsv:ay_1617:reachability_probabilities_in_mdps.pdf |Slides MDPs}}, [[http://www.prismmodelchecker.org/tutorial/phil.php|Example of MDP in PRISM]] - [[https://unicam.webex.com/unicam/ldr.php?RCID=849b4cf63dd75a91a309f64a404de0bf | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=a225cf7ef9f85508c971aeeb72da84fa |Link for downloading the lecture]] - Password to visualise and download the video: none |
| - | * Lecture of 16/02/2017 - ... | + | * Lecture of 15/02/2017 - Exercises on Modelling and Verification of MDPs and CTMCs in PRISM. [[http://www.prismmodelchecker.org/tutorial/phil.php |Randomised Dining Philosophers]], {{ :didattica:magistrale:rtpsv:ay_1617:randomized_philosophers.pdf |Module relabelling for 3 and 5 philosophers}}, {{ :didattica:magistrale:rtpsv:ay_1617:lehman_d._rabin_m._o._1981_-_on_the_advantages_of_free_choice._a_symmetric_and_fully_distributed_solution_to_the_dining_philosophers_problem_extended_abstract_.pdf |Historical Paper on Randomised Dining Philosophers}}, and [[http://www.prismmodelchecker.org/tutorial/circadian.php |Circadian Clock]] - [[https://unicam.webex.com/unicam/ldr.php?RCID=8f0b6043f75073e47d038d549fc3aabc | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=125f269b776220e7dbab207bacac31ce |Link for downloading the lecture]] - Password to visualise and download the video: none |
| - | * Lecture of 17/02/2017 - ... | + | * Lecture of 16/02/2017 - [[http://www.prismmodelchecker.org/manual/ThePRISMLanguage/PTAs |Probabilistic Timed Automata in PRISM]]. [[http://www.prismmodelchecker.org/casestudies/zeroconf.php |Simplified IPv4 ZeroConf Protocol]], {{ :didattica:magistrale:rtpsv:ay_1617:simplified_ipv4_zeroconf_protocol_as_pta.pdf |Simplified protocol as PTA}}. [[http://www.prismmodelchecker.org/casestudies/molecules.php |Biochemical Reactions as CTMC]]. - [[https://unicam.webex.com/unicam/ldr.php?RCID=0c65254ac79c72bd5e530c3538eaa829 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=96b1ba89ded3cdc6586835882da0bb62 |Link for downloading the lecture]] - Password to visualise and download the video: none |
| **Reference books** | **Reference books** | ||
| Line 143: | Line 143: | ||
| * Assignment 1 - Self-study report on "Partition-based minimization algorithm for Finite State Automata recognizing regular languages", deadline 14/10/2016 23.59. Send the pdf by email to luca.tesei@unicam.it | * Assignment 1 - Self-study report on "Partition-based minimization algorithm for Finite State Automata recognizing regular languages", deadline 14/10/2016 23.59. Send the pdf by email to luca.tesei@unicam.it | ||
| * Assignment 2 - {{ :didattica:magistrale:rtpsv:ay_1617:rtpsv1617-assignment-2.pdf |Text of the Assignment}}, deadline 10/02/2017 23.59. | * Assignment 2 - {{ :didattica:magistrale:rtpsv:ay_1617:rtpsv1617-assignment-2.pdf |Text of the Assignment}}, deadline 10/02/2017 23.59. | ||
| + | * Assignment 3 - {{ :didattica:magistrale:rtpsv:ay_1617:rpsv1617-assignment-3.pdf |Text of the Assignment}}, deadline 10/03/2017 23.59. | ||
| **Exam Dates A.Y. 2016/2017** | **Exam Dates A.Y. 2016/2017** | ||
