U hebt geen rechten om deze pagina te bewerken, want:
De gevraagde handeling is voorbehouden aan gepriviligeerde gebruikers. (groep gebruikers)
Vrije tekst:
[[Categorie:Vakwerkplaatsingangen]]{{QL/Inhoud}} [[Categorie:Public]] __NOTOC__ == New website for 2014 == Starting 2014, this course will use OpenCourseware. Please surf to http://www.ocw.cs.ru.nl/NWI-IMC033. <font color="grey"> == <font color="grey">Introduction</font> == More complex systems require more complete methods to check whether they satisfy their requirements. It becomes too risky to provide systems to customers based on only a few test runs. This course introduces several variants of model checking, a fully automated method to verify whether a model of (computer) system behaviour satisfies its requirements, expressed in a suitable logic. In particular, we will look at probabilistic logics and other quantitative logics. The models used are variants of Markov chains. Quantitative logics have the advantage that they do not just provide the answer “true” or “false”; a typical outcome is a (real) number that gives more exact information about the degree of satisfaction. As model checking is fully automatic, requiring no complex knowledge of proof strategies or biases of simulation tools, it is the method of choice for industry-scale verification. While the basics of model checking are about 25 years old, we will reach the forefront of research in discussing the newest extensions. == <font color="grey">Objectives</font> == *Ability to express requirements and create models of (computer) system behaviour, as far as it fits in the taught formalisms. *Know the possibilities and limitations of model checking for quantitative models. *Know examples of model checking algorithms for quantitative models. *You know about a variety of quantitative logics and their model checking algorithms. In particular, temporal logic; probabilistic logic; stochastic logic; discounting. (Depending on time, I may also include a real-time logic and a logic with rewards.) *You can demonstrate that you could write (the mathematical logic part of) a simple model checker. It is not a goal of this course to introduce you to the several optimisation methods like BDDs or symbolic model checking, that are used in practice to handle large models. Nor is it a goal of the course to solve the linear equation systems etc. because you should have learnt that already in your Linear Algebra course. == <font color="grey">Schedule</font> == {| border="1" |- ! Wk ! Date ! Time ! Topic ! Slides ! Literature |- valign="top" | rowspan="2" align="right" | 6 | Tue, Feb 5 | align="right" | 13.45 | Global overview; refreshers in probability theory, labelled transition systems, CTL model checking | align="center" | [[Media:QL-1-LTS-and-probabilities.pdf|2013]] | rowspan="2" | [http://dx.doi.org/10.1145/5397.5399 Clarke, Emerson, Sistla 1986]<br /> [http://dx.doi.org/10.1007/BFb0025774 (1982)] |- valign="top" | bgcolor="lightgrey" | Wed, Feb 6 | align="right" bgcolor="lightgrey" | 15.45 | bgcolor="lightgrey" | exercises | bgcolor="lightgrey" align="center" | [[Media:QL-1-LTS-and-probabilities-exercises.pdf|2013]] |- valign="top" | align="right" | 7 | Wed, Feb 13 | align="right" | 15.45 | Discrete-time Markov chains | align="center" | [[Media:QL-2-Markovchains.pdf|2013]] | rowspan="6" | [http://dx.doi.org/10.1007/BF01211866 Hansson, Jonsson 1994] |- valign="top" | rowspan="2" align="right" | 8 | bgcolor="lightgrey" | Tue, Feb 19 | align="right" bgcolor="lightgrey" | 13.45 | bgcolor="lightgrey" | exercises | align="center" bgcolor="lightgrey" | [[Media:QL-2-Markovchains-exercises.pdf|2013]] |- valign="top" | Wed, Feb 20 | align="right" | 15.45 | Probabilistic CTL | align="center" | [[Media:QL-3-PCTL.pdf|2013]] |- valign="top" | rowspan="2" align="right" | 9 | bgcolor="lightgrey" | Tue, Feb 26 | align="right" bgcolor="lightgrey" | 13.45 | bgcolor="lightgrey" | exercises | align="center" bgcolor="lightgrey" | [[Media:QL-3-PCTL-exercises.pdf|2013]] |- valign="top" | Wed, Feb 27 | align="right" | 15.45 | PCTL model checking on Markov chains | align="center" | [[Media:QL-4-DTMC-Modelchecking.pdf|2013]] |- valign="top" | rowspan="2" align="right" | 10 | bgcolor="lightgrey" | Tue, Mar 5 | align="right" bgcolor="lightgrey" | 13.45 | bgcolor="lightgrey" | exercises | align="center" bgcolor="lightgrey" | [[Media:QL-4-PCTL-exercises.pdf|2013]] |- valign="top" | Wed, Mar 6 | align="right" | 15.45 | [http://www.mrmc-tool.org/ MRMC, the Markov reward model checker] | align="center" | [[Media:QL-5-MRMC.pdf|2013]] |- valign="top" | rowspan="2" align="right" | 11 | bgcolor="lightgrey" | Tue, Mar 12 | align="right" bgcolor="lightgrey" | 13.45 | bgcolor="lightgrey" | exercises on MRMC. I would be happy if some of you could install it on their laptops. | bgcolor="lightgrey" | |- valign="top" | Wed, Mar 13 | align="right" | 15.45 | Markov decision processes | align="center" | [[Media:QL-6-Markov-decision-process.pdf|2013]] | rowspan="4" | [http://dx.doi.org/10.1007/s004460050046 Baier, Kwiatkowska 1998] |- valign="top" | rowspan="2" align="right" | 12 | bgcolor="lightgrey" | Tue, Mar 19 | align="right" bgcolor="lightgrey" | 13.45 | bgcolor="lightgrey" | exercises | align="center" bgcolor="lightgrey" | [[Media:QL-6-MDP-exercises.pdf|2013]] |- valign="top" | Wed, Mar 20 | colspan="3" align="center" | <font color="grey">Lecture cancelled—I am ill</font> |- valign="top" | rowspan="2" align="right" | 13 | bgcolor="lightgrey" | Tue, Mar 26 | align="right" bgcolor="lightgrey" | 13.45 | rowspan="2" valign="middle" | PCTL model checking on MDPs | rowspan="2" align="center" valign="middle" | [[Media:QL-7-MDP-modelchecking.pdf|2013]] |- valign="top" | Wed, Mar 27 | align="right" | 15.45 |- valign="top" | rowspan="2" align="right" | 16 | bgcolor="lightgrey" | Tue, Apr 16 | align="right" bgcolor="lightgrey" | 13.45 | bgcolor="lightgrey" | exercises on [http://www.prismmodelchecker.org/ the model checker PRISM]. I would be happy if some of you can install it on their laptop. | bgcolor="lightgrey" | |- valign="top" | Wed, Apr 17 | align="right" | 15.45 | Continuous-time Markov chains | align="center" | [[Media:QL-8-CTMC.pdf|2013]]<br /> [http://doc.utwente.nl/66254/ 2013] <!-- [[Media:Uranium-Actinium-decay.pdf]] --> |- valign="top" | rowspan="2" align="right" | 17 | bgcolor="lightgrey" | Tue, Apr 23 | bgcolor="lightgrey" align="right" | 13.45 | bgcolor="lightgrey" | exercises | bgcolor="lightgrey" align="center" | [[Media:QL-8-CTMC-exercises.pdf|2013]] |- valign="top" | Wed, Apr 24 | align="right" | 15.45 | CTMCs, continued, and Continuous Stochastic Logic <small>(including multiple until)</small> | align="center" | [[Media:QL-9-CSL.pdf|2013]] | rowspan="6" | [http://dx.doi.org/10.1109/TSE.2003.1205180 Baier, Haverkort, Hermanns, Katoen 2003] |- valign="top" | rowspan="2" align="right" | 19 | bgcolor="lightgrey" | Tue, May 7 | bgcolor="lightgrey" align="right" | 10.45 | bgcolor="lightgrey" | exercises | bgcolor="lightgrey" align="center" | [[Media:QL-9-CSL-exercises.pdf|2013]] |- valign="top" | Wed, May 8 | colspan="3" align="center" | <font color="grey">No lecture—I am absent</font> |- valign="top" | rowspan="2" align="right" | 20 | bgcolor="lightgrey" | Tue, May 14 | bgcolor="lightgrey" align="right" | 13.45 | bgcolor="lightgrey" | repetition? | bgcolor="lightgrey" | |- valign="top" | Wed, May 15 | align="right" | 15.45 | CSL model checking <small>(without multiple until)</small> | align="center" | [[Media:QL-10-CSL-model-checking.pdf|2013]]<!-- and perhaps [[Media:QL-9-CSL-until.pdf|2012]] --> |- valign="top" | rowspan="2" align="right" | 21 | bgcolor="lightgrey" | Tue, May 21 | bgcolor="lightgrey" align="right" | 13.45 | bgcolor="lightgrey" | exercises | align="center" bgcolor="lightgrey" | [[Media:QL-10-CSL-model-checking-exercises.pdf|2013]] |- valign="top" | Wed, May 22 | align="right" | 15.45 | [http://www.mrmc-tool.org/ MRMC] as a model checker for CTMCs | align="center" | [[Media:QL-11-MRMC-for-CTMCs.pdf|2013]] |- valign="top" | rowspan="2" align="right" | 22 | bgcolor="lightgrey" | Tue, May 28 | bgcolor="lightgrey" align="right" | 13.45 | bgcolor="lightgrey" | exercises | bgcolor="lightgrey" | Problems 2 and 3<br>from last week |- valign="top" | Wed, May 29 | align="right" | 15.45 | Discounted CTL | align="center" | [[Media:QL-8-DCTL.pdf|2012]] | rowspan="4" | [http://dx.doi.org/10.1016/j.tcs.2005.07.033 Alfaro, Faella, Henzinger, Majumdar, Stoelinga 2005] |- valign="top" | rowspan="2" align="right" | 23 | bgcolor="lightgrey" | Tue, June 4 | bgcolor="lightgrey" align="right" | 13.45 | bgcolor="lightgrey" | exercises | align="center" bgcolor="lightgrey" | [[Media:QL-8-DCTL-exercises.pdf|2013]] |- valign="top" | Wed, June 5 | align="right" | 15.45 | DCTL model checking | (p. 161sq. of<br />the article) |- valign="top" | rowspan="2" align="right" | 24 | bgcolor="lightgrey" | Tue, June 11 | align="right" bgcolor="lightgrey" | 13.45 | bgcolor="lightgrey" | exercises | bgcolor="lightgrey" | |- valign="top" | Wed, June 12 | align="right" | 15.45 | Outlook into bisimulation<!-- and [http://www.prismmodelchecker.org/lectures/pmc/19-symbolic.pdf symbolic model checking]? --> | align="center" | [[Media:QL-7-Lumping.pdf|2013]] | rowspan="2" | [http://dx.doi.org/10.1016/S0020-0190(03)00343-0 Derisavi, Hermanns, Sanders 2003] |- valign="top" | rowspan="2" align="right" | 25 | bgcolor="lightgrey" | Tue, June 18 | align="right" bgcolor="lightgrey" | 13.45 | bgcolor="lightgrey" | exercises | align="center" bgcolor="lightgrey" | [[Media:QL-7-Lumping-exercises.pdf|2013]]<!-- <br /> [[Media:QL-StoCharts-exercises.pdf|2012]] --> |- valign="top" | Wed, June 19 | align="right" | 15.45 | Recapitulation, questions |- valign="top" bgcolor="#ffaaaa" | align="right" | 27 | Tue, July 2 | align="right" | <s>8.30</s><br />10.30 | Examination |} == <font color="grey">Evaluation</font> == Written exam on July 2. == <font color="grey">Extra information</font> == Students are encouraged to express their own interest, so that the programme can be adapted. ---- [[Gebruiker:David Jansen|David N. Jansen]]</font>
Samenvatting:
Dit is een kleine bewerking Deze pagina volgen
Annuleren
