Differences

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

--- didattica:magistrale:svl:ay_1819:main [2019/05/15 11:48]
luca [Lectures]
+++ didattica:magistrale:svl:ay_1819:main [2020/09/17 16:55] (current)
@@ Line 3: / Line 3: @@
 ===== News =====
 <WRAP center round important 95%>
+  * <wrap em>**26/05/2019**</wrap>: Project for 2018/2019 is available in the relative section below.
   * <wrap em>**13/05/2019**</wrap>: On **Thursday 16/05/2019** there will be **two extra lectures** given as seminars of **Dr. Matteo Rucco**. The first one is scheduled at 11:00am in Room AB1 and the second one is scheduled at 04.30pm in Room AB1 as well.
   * <wrap em>**07/04/2019**</wrap>: The calendar of the course has been updated, please take note of the new dates in section "Lectures" below.
@@ Line 112: / Line 113: @@
   - 15/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=d31f0c044e2b798205b5c7c03e164637|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=5db1a79662b0bde33a1b643a17d5254a|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:svl-notes-15-05-2019.pdf |Notes}}, [[https://www.youtube.com/watch?v=skM37PcZmWE|Achilles and the Tortoise]]
   - 16/05/2019 - **Seminar Lectures** of Matteo Rucco: {{ :didattica:magistrale:svl:ay_1819:locandina_per_seminari_logo_unicam_matteo_rucco_1.pdf |Seminar 1}}, {{ :didattica:magistrale:svl:ay_1819:locandina_per_seminari_logo_unicam_matteo_rucco_2.pdf |Seminar 2}}
-  - 20/05/2019
+  - 20/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=757d010998a9781d6cb8845c3fb664a2|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=79a1b8e3d1ac3e7e369bd8c1af2066b6|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:traingatetimed.xml.zip |UPPAAL Model}}
-  - 22/05/2019
+  - 22/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=bf66275e77194d5a7fbf26474fb3713c|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=99f0ba434e2ae527efb097ecea23c1f0|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:svl1819-uppaalcode-22-05-2019.zip |UPPAAL Models}}, [[http://www.prismmodelchecker.org/lectures/esslli10/esslli10pmc-part1.pdf|PRISM Slides on DTMCs]]
-  - 27/05/2019
+  - 27/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=fd2024522f965a22d558e4f5e264d1c5|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=88b6f1506cef838aa5d6b7912dcf3c47|Download the Lecture]], [[http://www.prismmodelchecker.org/lectures/esslli10/esslli10pmc-part1.pdf|PRISM Slides on DTMCs]], {{ :didattica:magistrale:svl:ay_1819:die.zip |Die example in PRISM}}
-  - 29/05/2019
+  - 29/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=2002b01720dd0c5a47db5c5e58078523|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=659b29de0a5729945b0e52aac477c53c|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:herman7.zip |PRISM Code}}, [[http://www.prismmodelchecker.org/lectures/pmc/03-dtmcs.pdf|Slides Long-run Probability]], {{ :didattica:magistrale:svl:ay_1819:svl-notes-29-05-2019.pdf |Notes}}
-  - 03/06/2019
+  - 03/06/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=8ab1c9d51279cda185dc64b5fad97ce9|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=e9720bd0c38830e0065c222d2c20a62f|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:svl-notes-03-06-2019.pdf |Notes}}
 </WRAP>
 ----
@@ Line 187: / Line 188: @@
 **Markov Chains**
-  * ...
+  * [[http://www.prismmodelchecker.org/lectures/esslli10/esslli10pmc-part1.pdf|Discrete Time Markov Chains and TCTL]]
+  * [[http://www.prismmodelchecker.org/lectures/esslli10/esslli10pmc-part4.pdf|Probabilistic model checking in practice]]
+  * [[http://www.prismmodelchecker.org/tutorial/|PRISM Tutorial]]
+  * [[http://www.prismmodelchecker.org/manual/Main/Welcome|PRISM Manual]]
 ==== Exercises ====
@@ Line 193: / Line 197: @@
   * {{ :didattica:magistrale:svl:ay_1819:exsolmodelsandmodelling.pdf |Transition Systems and Modelling Languages for Reactive Systems}}
   * {{ :didattica:magistrale:svl:ay_1819:exsollineartime.pdf |Linear Time Properties}}
-  * ...
+  * {{ :didattica:magistrale:svl:ay_1819:exsolltlctl_with_exercises_from_book.pdf |Regular Properties, LTL and CTL}} - **NOTE 1:** some of the exercises on Regular Properties and on LTL require to calculate the product between the transition system and the non-Deterministic Buechi Automaton (NBA) corresponding to the formula - ignore that part and justify your answer by providing the counterexample without providing the product construction. **NOTE 2:** some of the exercises on CTL require to show the steps of the Sat algorithm for deciding the satisfaction of the formula by a state or by a transition system: ignore this request and provide, if possible, an informal justification; if not possible ignore the exercise.
 ==== Textbooks ====
@@ Line 212: / Line 215: @@
 ===== Project =====
 <WRAP box round center 95%>
-  - ... TBA
+  - {{ :didattica:magistrale:svl:ay_1819:svl18q9_project.pdf |Text of Project 2018/2019}}
 </WRAP>
@@ Line 219: / Line 222: @@
 <WRAP box round center 95%>
 **Exam Dates A.Y. 2018/2019 (Written Test Dates)**
-  - 06/02/2019, 3:00pm, Room LA1
+  - 06/02/2019, 3:00pm, Room LA1 - no students.
-  - 20/02/2019, 3:00pm, Room LA1
+  - 20/02/2019, 3:00pm, Room LA1 - no students.
-  - 13/06/2019, 3:00pm, Room TBA, please register on ESSE3 to the Partial Exam "SVL1819 Sess. III - Written Test" before 07/06/2019
+  - 13/06/2019, 3:00pm, Room AB1 - no students.
-  - 27/06/2019, 3:00pm, Room TBA, please register on ESSE3 to the Partial Exam "SVL1819 Sess. IV - Written Test" before 21/06/2019
+  - <del>27/06/2019, 3:00pm, Room TBA</del>, 28/06/2019, 11:00am, Room AB1 Polo Lodovici - {{ :didattica:magistrale:svl:ay_1819:svl1819appello1.pdf |Text}}, {{ :didattica:magistrale:svl:ay_1819:svl1819appello1solutionwithnotes.pdf |Text with Solutions}}
-  - 17/07/2019, 3:00pm, Room TBA, please register on ESSE3 to the Partial Exam "SVL1819 Sess. V - Written Test" before 12/07/2019
+  - 17/07/2019, 3:00pm, Room AB2 Polo Lodovici - {{ :didattica:magistrale:svl:ay_1819:svl1819appello2.pdf |Text}}, {{ :didattica:magistrale:svl:ay_1819:svl1819appello2withsolution.pdf |Text with Solutions}}
-  - 12/09/2019, 3:00pm, Room TBA, please register on ESSE3 to the Partial Exam "SVL1819 Sess. VI - Written Test" before 06/09/2019
+  - 12/09/2019, 3:00pm, Room AA1 Polo Lodovici - {{ :didattica:magistrale:svl:ay_1819:svl1819appello3.pdf |Text}}, {{ :didattica:magistrale:svl:ay_1819:svl1819appello3_with_solutions.pdf |Text with Solutions}}
-  - 26/09/2019, 3:00pm, Room TBA, please register on ESSE3 to the Partial Exam "SVL1819 Sess. VII - Written Test" before 20/09/2019
+  - 26/09/2019, 3:00pm, Room AA1 Polo Lodovici, please register on ESSE3 to the Partial Exam "SVL1819 Sess. VII - Written Test" before 20/09/2019
   - 24/03/2020, 3:00pm, Room TBA, please register on ESSE3 to the Partial Exam "SVL1819 Sess. VIII - Written Test" before 20/03/2020
@@ Line 232: / Line 235: @@
 The exam consists of a written test, containing open-answer questions (exercises), together with one project, realised with the tools introduced in the course (see section "Project" above). The Written Test and the Project are two independent Partial Exams (see the exam sessions in the ESSE3 career system) and can be passed in different exam sessions. The final grade, which is the average of the grades of the two Partial Exams, can be obtained and registered only if both the Partial Exams have been passed with a grade of at least 18/30.
-**Registration for the written tests** must be done using the Student Career System ESSE3 [[https://didattica.unicam.it|here]]. Please note that the registration **deadline** is usually **3 working days before** the written test date. BSc students or MSc students who did not select the Intelligent and Adaptive Systems (IAS) Curriculum will not be able to register for the written test until they communicate to the Secretary Office (Tiziana Jajani c/o Student Secretary Office, [[http://www.unicam.it/studente/segreterie-studenti|Opening Hours]]) their choice to attend to this course, code [ST1192] SYSTEMS VERIFICATION LAB.
+**Registration for the written tests** must be done using the Student Career System ESSE3 [[https://didattica.unicam.it|here]]. Please note that the registration **deadline** is usually **3 working days before** the written test date. BSc students or MSc students who did not select the Intelligent and Adaptive Systems (IAS) Curriculum will not be able to register for the written test until they communicate to the Secretary Office (Tiziana Jajani c/o Student Secretary Office, [[http://www.unicam.it/studente/segreterie-studenti|Opening Hours]]) their choice to attend to this course, code [ST1192] SYSTEMS VERIFICATION LAB. During the exercise sessions throughout the course samples of the written test questions will be presented with solutions. During the written test students can consult a hand-written A4 paper of their production for reference.
 **Instructions for Sending Projects**