Quantitative Model Checking

We have graded the first practical assignment sheet and uploaded our feedback.

To streamline the work on the second practical assignment sheet, we offer you the option to resort to sample solutions to exercises P1.1 and P1.2. You find them in the dCMS under Materials now. This might come in handy in case your own solution had major flaws or was incomplete.

Note that PCTL formulas correctly solving what was asked for in P1.2 can differ significantly from those appearing in the sample solution, depending on the exact modeling (e.g. how many steps were used to model a round in the game etc.).

HeHo

Next week will feature no lecture (again) due to Thursday being a public holiday. Instead, we are (again) arranging office hours for the discussion of lecture contents. Meet Gabriel (i) on Monday, May 26, 2 pm to 4 pm, and/or (ii) on Wednesday, May 28, 2 pm to 4 pm in room 533 of E1 3. Besides, you are free to write emails to dengler@depend.uni-saarland.de anytime.

HeHo

The material of this week is available in dCMS since yesterday, including tutorial sheet and a second assignment. (We will stop announcing material availabilty from now on.)

Next week will feature no lecture due to Thursday being a public holiday. Instead, we are arranging office hours for the discussion of lecture contents. Meet Gabriel (i) on Tuesday, April 29, 2 pm to 4 pm, and/or (ii) on Friday, May 2, 2 pm to 4 pm in room 533 of E1 3. Besides, you are free to write emails to dengler@depend.uni-saarland.de anytime.

We will soon start with hands-on work using the probabilistic model checker PRISM.  It is recommended to get it installed from https://www.prismmodelchecker.org/download.php, and you are invited to play around with it, e.g. by following the tutorial in https://www.prismmodelchecker.org/tutorial/die.php, but this is not essential for the tasks currently in focus.

HeHo