Differences

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

--- didattica:magistrale:rtpsv:ay_1718:main [2017/09/20 14:47]
luca [Study material]
+++ didattica:magistrale:rtpsv:ay_1718:main [2020/09/17 16:55] (current)
@@ Line 1: / Line 1: @@
-====== Real-time and Probabilistic System Verification ======
+====== Real-time and Probabilistic Systems Verification ======
 ----
 ===== News =====
 <WRAP center round important 95%>
   * <wrap em>**October 2nd, 2017**</wrap>: The course starts officially at 11.00 in Room LA1
+  * <wrap em>**October 12th 2017**</wrap>: the lecture of Thursday 12th October is cancelled for a commitment of the teacher.
+  * <wrap em>**October 30th 2017**</wrap>: the lecture of Thursday 9th November is cancelled for a commitment of the teacher.
 </WRAP>
@@ Line 83: / Line 85: @@
 </WRAP>
 ----
-===== Study material =====
+===== Study Material =====
 <WRAP box round center 95%>
-**Lectures**
+**Additional Material besides the Reference Books**
   * {{ :didattica:magistrale:rtpsv:ay_1718:strong_bisimilarity.pdf |Strong Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1718:exercises_strong_bisimilarity_with_solutions.pdf |Exercises on Strong Bisimilarity}} - Reactive Systems Book pages: 31-53
   * {{ :didattica:magistrale:rtpsv:ay_1718:weak_bisimilarity.pdf |Weak Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1718:weak_bisimilarity_exercises_with_solutions.pdf |Exercises on Weak Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1718:hennessy-milner_logic.pdf |Hennessy-Milner Logic (HML)}} - Reactive Systems Book pages: 53 - 72 and 89 - 101
@@ Line 108: / Line 110: @@
   * [[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_1718:simplified_ipv4_zeroconf_protocol_as_pta.pdf |Simplified protocol as PTA}}. [[http://www.prismmodelchecker.org/casestudies/molecules.php |Biochemical Reactions as CTMC]].
-**Reference books**
+**Reference Books**
   * Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen and Jiri Srba, "Reactive Systems. Modelling, Specification and Verification", Cambridge University Press, 2007. ISBN: 9780521875462 – [[http://www.cambridge.org/us/knowledge/isbn/item1174475/?site_locale=en_US|Website]]
   * Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, ISBN: 9780262026499
+**Reading Books**
+  * Vidyadhar G. Kulkarni, "Modeling and Analysis of Stochastic Systems, Third Edition", Chapman & Hall/CRC, 2016, ISBN-13: 978-1498756617
   * Michael Huth, Mark Ryan, “Logic in Computer Science: Modelling and Reasoning about Systems”, Cambridge University Press. ISBN: 9780521543101.
   * Glynn Winskel, "Formal Semantics of Programming Languages", The MIT Press, ISBN: 9780262731034.
 </WRAP>
 ----
 ===== Projects =====
 <WRAP box round center 95%>
 **Project(s) to be sent the day before the written test:**
-  - TBA
+  - {{ :didattica:magistrale:rtpsv:ay_1718:rpsv1718_project.pdf |Project 2017-18}}
 </WRAP>
@@ Line 135: / Line 139: @@
   - Appello VI - Written Test on Tuesday 25/09/2018 at 3.00pm, Room TBA
   - Appello VII - Written Test on Tuesday 05/02/2019 at 3.00pm, Room TBA
-  - Appello VIII - Written Test on Tuesday 19/02/2019 at 3.00pm, Room TBA
+  - Appello VIII - Written Test on Wednesday 20/02/2019 at 11.00am, Room TBA
 **Exam rules**
-The exam consists of a written test, containing open-answer and/or closed-answer questions, together with one project, realised with a model checking tool (see section "Projects" above). The project must be sent the day before the written test to which the student is registered (see section "Instructions for Sending Projects" below). During the exercise sessions throughout the course samples of the written test questions will be presented with solutions. The written test will last 2 hours and during the test students can consult a hand-written A4 paper of their production for reference.
+The exam consists of a written test, containing open-answer and/or closed-answer questions, together with one project, realised with a model checking tool (see section "Projects" above). The project must be sent the day before the written test to which the student is registered (see section "Instructions for Sending Projects" below). 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.
 **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.
-Please note that any student who did not send the project the day before the written test **will be excluded** from the written test. In case of re-trying of the written test the project must be re-sent.
+Please note that any student who did not send the project the day before the written test **may be excluded** from the written test. In case of re-trying of the written test the project must be re-sent.
 **Instructions for Sending Projects**