Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
didattica:magistrale:rsv:ay_1617:main [2017/06/06 16:41] luca [Lectures] |
didattica:magistrale:rsv:ay_1617:main [2020/09/17 16:55] (current) |
||
|---|---|---|---|
| Line 81: | Line 81: | ||
| ===== Lectures ===== | ===== Lectures ===== | ||
| <WRAP round 95% center box> | <WRAP round 95% center box> | ||
| - | * Tue 21/03/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=b6983b5b714e23dec4be991c4d1b32ed|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=1d556bb6a838dddcb71ad6d724445743|Download Lecture]] | + | - Tue 21/03/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=b6983b5b714e23dec4be991c4d1b32ed|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=1d556bb6a838dddcb71ad6d724445743|Download Lecture]] |
| - | * Thu 23/03/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=0cf3ef13bee7496702f6a2770d82cb2a|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=3f5cb29c841c51ba6266575e72c0a178|Download Lecture]] | + | - Thu 23/03/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=0cf3ef13bee7496702f6a2770d82cb2a|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=3f5cb29c841c51ba6266575e72c0a178|Download Lecture]] |
| - | * Tue 28/03/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=c331b6b237504d94efe07b0baa0ac3d5|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=797022d74e50b921d343ad096e7aa9e7|Download Lecture]] - {{ :didattica:magistrale:rsv:ay_1617:gcltopgtots_beverage_machine.pdf |Exercise Translation GCL to PG to TS Beverage Machine}} | + | - Tue 28/03/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=c331b6b237504d94efe07b0baa0ac3d5|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=797022d74e50b921d343ad096e7aa9e7|Download Lecture]] - {{ :didattica:magistrale:rsv:ay_1617:gcltopgtots_beverage_machine.pdf |Exercise Translation GCL to PG to TS Beverage Machine}} |
| - | * Thu 30/03/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=3a683fafaf94aff95caf55638d209cf5|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=38e144f30e5340374bae471e82651543|Download Lecture]] | + | - Thu 30/03/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=3a683fafaf94aff95caf55638d209cf5|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=38e144f30e5340374bae471e82651543|Download Lecture]] |
| - | * Tue 04/04/2017 The lecture is cancelled due to an unexpected commitment of the teacher. | + | - Thu 06/04/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=e464489174b020637fdb2d7de7829575|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=f51e6b838a620f443bccbd70782689f3|Download Lecture]] |
| - | * Thu 06/04/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=e464489174b020637fdb2d7de7829575|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=f51e6b838a620f443bccbd70782689f3|Download Lecture]] | + | - Tue 11/04/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=59e839af1aa7d3e7d5f439b8f76f67b5|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=4e2fcdb28fd0c1bead3ec6dabb0e6711|Download Lecture]], {{ :didattica:magistrale:rsv:ay_1617:luca_2.tesei_13-04-2017_13-06-41.pdf |Whiteboard Slides}} |
| - | * Tue 11/04/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=59e839af1aa7d3e7d5f439b8f76f67b5|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=4e2fcdb28fd0c1bead3ec6dabb0e6711|Download Lecture]], {{ :didattica:magistrale:rsv:ay_1617:luca_2.tesei_13-04-2017_13-06-41.pdf |Whiteboard Slides}} | + | - Thu 13/04/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=891313cb20a3ab5ddbccf398479266f2|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=672ed1bb755be9b9a382736a788e35bd|Download Lecture]], {{ :didattica:magistrale:rsv:ay_1617:luca.tesei_13-04-2017_13-06-41.pdf |Witheboard Slides}} |
| - | * Thu 13/04/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=891313cb20a3ab5ddbccf398479266f2|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=672ed1bb755be9b9a382736a788e35bd|Download Lecture]], {{ :didattica:magistrale:rsv:ay_1617:luca.tesei_13-04-2017_13-06-41.pdf |Witheboard Slides}} | + | - Thu 27/04/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=dc12b4b7ca374dbb829f1c8893e61240|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=8839e96e201025a860ab8a717e6d66c9|Download Lecture]], [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-01.pdf|Slide1]], [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-02.pdf|Slide2]], [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-03.pdf|Slide3]], [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-04.pdf|Slide4]] |
| - | * Thu 27/04/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=dc12b4b7ca374dbb829f1c8893e61240|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=8839e96e201025a860ab8a717e6d66c9|Download Lecture]], [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-01.pdf|Slide1]], [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-02.pdf|Slide2]], [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-03.pdf|Slide3]], [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-04.pdf|Slide4]] | + | - Tue 02/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=4b060b6c6c37060d609dd2ebd7386e37|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=3b44a857a840cd46b039c41b11fa569e|Download Lecture]] - Unfortunately the screen was not shared in the first part of the lecture. To follow the slides refer to: [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-02.pdf|Slide2 (from slide 15 on)]] and [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-03.pdf|Slide3]] |
| - | * Tue 02/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=4b060b6c6c37060d609dd2ebd7386e37|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=3b44a857a840cd46b039c41b11fa569e|Download Lecture]] - Unfortunately the screen was not shared in the first part of the lecture. To follow the slides refer to: [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-02.pdf|Slide2 (from slide 15 on)]] and [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-03.pdf|Slide3]] | + | - Thu 04/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=bc0064b71e93b912f389edae3a7e10a1|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=de73f9945ae2006fa2e70ea596753e59|Download Lecture]] |
| - | * Thu 04/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=bc0064b71e93b912f389edae3a7e10a1|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=de73f9945ae2006fa2e70ea596753e59|Download Lecture]] | + | - Tue 09/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=85590410b6fa5639bb53d3aefec9d83c|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=cf4fda96effabdf4076f337980845fcc|Download Lecture]] |
| - | * Tue 09/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=85590410b6fa5639bb53d3aefec9d83c|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=cf4fda96effabdf4076f337980845fcc|Download Lecture]] | + | - Thu 11/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=f6c83dd3dff5c87835d667fdae0a23ee|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=d1d43b45a8e514df92a5a866e5b21d97|Download Lecture]] |
| - | * Thu 11/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=f6c83dd3dff5c87835d667fdae0a23ee|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=d1d43b45a8e514df92a5a866e5b21d97|Download Lecture]] | + | - Tue 16/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=eb110fc9865de5782492eb1c1ebb2eb7|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=2d626a19b2e7241a17025a4093476502|Download Lecture]] |
| - | * Tue 16/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=eb110fc9865de5782492eb1c1ebb2eb7|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=2d626a19b2e7241a17025a4093476502|Download Lecture]] | + | - Tue 23/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=93663be0a8d0d7089c97c97e3b692075|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=fdb81e81440f2f03677c7386e0f6bffc|Download Lecture]] |
| - | * Tue 23/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=93663be0a8d0d7089c97c97e3b692075|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=fdb81e81440f2f03677c7386e0f6bffc|Download Lecture]] | + | - Thu 25/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=13452e3529f8542816dc9da5c1b1916b|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=5283c225a493637b0623abd24c2f04ea|Download Lecture]] |
| - | * Thu 25/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=13452e3529f8542816dc9da5c1b1916b|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=5283c225a493637b0623abd24c2f04ea|Download Lecture]] | + | - Tue 30/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=5142490141f0f3bcc2a14b0cb3e663b2|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=484abcb0a06cfbc7663a10aff1cb8d02|Download Lecture]] |
| - | * Tue 30/05/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=5142490141f0f3bcc2a14b0cb3e663b2|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=484abcb0a06cfbc7663a10aff1cb8d02|Download Lecture]] | + | - Thu 01/06/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=4afe4da81946e5eb73c339fa4d348079|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=7c70073f415e5816b8f405691cc2bc63|Download Lecture]] |
| - | * Thu 01/06/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=4afe4da81946e5eb73c339fa4d348079|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=7c70073f415e5816b8f405691cc2bc63|Download Lecture]] | + | - Tue 06/06/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=92287385d48880ea61311814ea023ef0|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=a0e39dd9eda035ddf0d4c0239a330a59|Download Lecture]] |
| - | * Tue 06/06/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=92287385d48880ea61311814ea023ef0|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=a0e39dd9eda035ddf0d4c0239a330a59|Download Lecture]] | + | - Thu 08/06/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=c88861d08b5b76acc9f3baa63197a212|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=0aad219f47f88a970081df6e32a858fd|Download Lecture]], [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-2013-05.pdf|Slide 5 SPIN]], [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-2013-06.pdf|Slide 6 SPIN]] |
| + | - Tue 13/06/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=d20f4905c9e9ff97325188f963cf101e|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=51e5bf8221f11eec526570f524f64d4e|Download Lecture]] | ||
| + | - Thu 15/06/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=6a0e391ac0a727ef0d5957b451a4a8de|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=e6d91d9156d7714fcddfabeda709dfa3|Download Lecture]], {{ :didattica:magistrale:rsv:ay_1617:luca.tesei_15-06-2017_11-16-42.pdf |Sketch of the project components}} | ||
| </WRAP> | </WRAP> | ||
| ---- | ---- | ||
| Line 145: | Line 147: | ||
| * {{ :didattica:magistrale:rsv:ay_1617:ltl._expressing_fairness.pdf |Expressing Fairness in LTL}} | * {{ :didattica:magistrale:rsv:ay_1617:ltl._expressing_fairness.pdf |Expressing Fairness in LTL}} | ||
| * {{ :didattica:magistrale:rsv:ay_1617:ltl._general_picture_of_model_checking_with_buchi_automata.pdf |General Picture of LTL Model Checking with Buchi Automata}} | * {{ :didattica:magistrale:rsv:ay_1617:ltl._general_picture_of_model_checking_with_buchi_automata.pdf |General Picture of LTL Model Checking with Buchi Automata}} | ||
| - | |||
| - | //Exercises on Linear Temporal Logic// | ||
| - | |||
| - | /* * {{:didattica:magistrale:rsv:ay_1516:exercise-sheet.pdf|LTL exercises}} | ||
| - | */ | ||
| //Computational Tree Logic// | //Computational Tree Logic// | ||
| * {{ :didattica:magistrale:rsv:ay_1617:ctl._syntax_semantics_equivalences_and_normal_forms.pdf |CTL: Syntax, Semantics, Equivalence and Normal Forms}} | * {{ :didattica:magistrale:rsv:ay_1617:ctl._syntax_semantics_equivalences_and_normal_forms.pdf |CTL: Syntax, Semantics, Equivalence and Normal Forms}} | ||
| + | * {{ :didattica:magistrale:rsv:ay_1617:ctl_vs_ltl.pdf |CTL vs LTL}} | ||
| + | * {{ :didattica:magistrale:rsv:ay_1617:ctl_model_checking.pdf |CTL Model Checking}} | ||
| + | * {{ :didattica:magistrale:rsv:ay_1617:ctl_with_fairness.pdf |CTL with Fairness}} | ||
| - | //Tools and practical applications// | + | //Exercises on NFA, NBA, LTL and CTL// |
| + | |||
| + | * {{ :didattica:magistrale:rsv:ay_1617:exercises_bad_prefixes_nfa.pdf |Exercises NFA, Bad prefixes and NBA}} | ||
| + | * {{ :didattica:magistrale:rsv:ay_1617:exercises_ltl.pdf |Exercises LTL}} | ||
| + | * {{ :didattica:magistrale:rsv:ay_1617:exercises_ctl.pdf |Exercises CTL}} | ||
| /* | /* | ||
| Line 178: | Line 182: | ||
| ===== Projects ===== | ===== Projects ===== | ||
| <WRAP box round center 95%> | <WRAP box round center 95%> | ||
| - | **Projects to be sent the day before the written test:** | + | **Project (only one this year) to be sent the day before the written test:** |
| - | - TBD | + | - {{ :didattica:magistrale:rsv:ay_1617:rsv16-17_project.pdf |Text of the project}} |
| - | - TBD | + | |
| - | - ... | + | |
| </WRAP> | </WRAP> | ||
| Line 188: | Line 191: | ||
| <WRAP box round center 95%> | <WRAP box round center 95%> | ||
| **Exam Dates A.Y. 2016/2017** | **Exam Dates A.Y. 2016/2017** | ||
| - | - Appello I - Written Test on Thursday 29/06/2017 11.00 - 13.00, Room TBA (look at ESSE3) | + | - Appello I - Written Test on Thursday 29/06/2017 11.00 - 13.00, Room AB3 - {{ :didattica:magistrale:rsv:ay_1617:rsv1617appelloi.pdf | Text of the test}} |
| - | - Appello II - Written Test on Wednesday 12/07/2017 11.00 - 13.00, Room TBA (look at ESSE3) | + | - Appello II - Written Test on Wednesday 12/07/2017 11.00 - 13.00, Room AB3 - {{ :didattica:magistrale:rsv:ay_1617:rsv1617appelloii.pdf |Text of the test}}, {{ :didattica:magistrale:rsv:ay_1617:rsv1617appelloii_with_solutions.pdf |Text of the test with Solutions}} |
| - | - Appello III - Written Test on Monday 24/07/2017 11.00 - 13.00, Room TBA (look at ESSE3) | + | - Appello III - Written Test on Monday 24/07/2017 11.00 - 13.00, Room AB3 |
| - | - Appello IV - Written Test on Thursday 14/09/2017 11.00 - 13.00, Room TBA (look at ESSE3) | + | - Appello IV - Written Test on Thursday 14/09/2017 11.00 - 13.00, Room AB3 |
| - | - Appello V - Written Test on Tuesday 26/09/2017 11.00 - 13.00, Room TBA (look at ESSE3) | + | - Appello V - Written Test on Tuesday 26/09/2017 11.00 - 13.00, Room AB3 |
| - | - Appello VI - Written Test on Thursday 01/02/2018 11.00 - 13.00, Room TBA (look at ESSE3) | + | - Appello VI - Written Test on Thursday 01/02/2018 11.00 - 13.00, Room AB3 |
| - | - Appello VII - Written Test on Thursday 15/02/2018 11.00 - 13.00, Room TBA (look at ESSE3) | + | - Appello VII - Written Test on Thursday 15/02/2018 11.00 - 13.00, Room AB3 |
| **Exam rules** | **Exam rules** | ||
