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/13 12:45] luca [Study material] |
didattica:magistrale:rtpsv:ay_1617:main [2020/09/17 16:55] (current) |
||
---|---|---|---|
Line 128: | Line 128: | ||
* 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 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 - 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 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 - Exercises on Cylinder Sets, Calculating Probabilities of Reachability Properties on DTMCs, Modelling and Verification of MDPs and CTMCs in PRISM | + | * 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 - Exercises on Cylinder Sets, Calculating Probabilities of Reachability Properties on DTMCs, Modelling and Verification of MDPs and CTMCs in PRISM | + | * 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** |