Differences

This shows you the differences between two versions of the page.

--- didattica:magistrale:rtpsv:ay_1617:main [2017/02/09 18:14]
luca [Study material]
+++ didattica:magistrale:rtpsv:ay_1617:main [2020/09/17 16:55] (current)
@@ Line 126: / Line 126: @@
   * 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 - 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 - ... - [[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 - ... - [[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**
@@ 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 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**