ÿþ<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns:mv="http://macVmlSchemaUri" xmlns="http://www.w3.org/TR/REC-html40"> <head> <meta name=Title content="02246: Model Checking"> <meta name=Keywords content=""> <meta http-equiv=Content-Type content="text/html; charset=unicode"> <meta name=ProgId content=Word.Document> <meta name=Generator content="Microsoft Word 14"> <meta name=Originator content="Microsoft Word 14"> <link rel=File-List href="index_files/filelist.xml"> <title>02246: Model Checking</title> <!--[if gte mso 9]><xml> <o:DocumentProperties> <o:Author>Flemming Nielson</o:Author> <o:LastAuthor>Flemming Nielson</o:LastAuthor> <o:Revision>24</o:Revision> <o:TotalTime>45</o:TotalTime> <o:Created>2011-07-14T10:02:00Z</o:Created> <o:LastSaved>2011-11-08T11:45:00Z</o:LastSaved> <o:Pages>1</o:Pages> <o:Words>412</o:Words> <o:Characters>2355</o:Characters> <o:Company>DTU Informatics</o:Company> <o:Lines>19</o:Lines> <o:Paragraphs>5</o:Paragraphs> <o:CharactersWithSpaces>2762</o:CharactersWithSpaces> <o:Version>14.0</o:Version> </o:DocumentProperties> <o:OfficeDocumentSettings> <o:AllowPNG/> </o:OfficeDocumentSettings> </xml><![endif]--> <link rel=themeData href="index_files/themedata.xml"> <!--[if gte mso 9]><xml> <w:WordDocument> <w:Zoom>150</w:Zoom> <w:SpellingState>Clean</w:SpellingState> <w:GrammarState>Clean</w:GrammarState> <w:TrackMoves/> <w:TrackFormatting/> <w:ValidateAgainstSchemas/> <w:SaveIfXMLInvalid>false</w:SaveIfXMLInvalid> <w:IgnoreMixedContent>false</w:IgnoreMixedContent> <w:AlwaysShowPlaceholderText>false</w:AlwaysShowPlaceholderText> <w:DoNotPromoteQF/> <w:LidThemeOther>EN-US</w:LidThemeOther> <w:LidThemeAsian>X-NONE</w:LidThemeAsian> <w:LidThemeComplexScript>X-NONE</w:LidThemeComplexScript> <w:Compatibility> <w:SplitPgBreakAndParaMark/> </w:Compatibility> <m:mathPr> <m:mathFont m:val="Cambria Math"/> <m:brkBin m:val="before"/> <m:brkBinSub m:val="&#45;-"/> <m:smallFrac m:val="off"/> <m:dispDef/> <m:lMargin m:val="0"/> <m:rMargin m:val="0"/> <m:defJc m:val="centerGroup"/> <m:wrapIndent m:val="1440"/> <m:intLim m:val="subSup"/> <m:naryLim m:val="undOvr"/> </m:mathPr></w:WordDocument> </xml><![endif]--><!--[if gte mso 9]><xml> <w:LatentStyles DefLockedState="false" DefUnhideWhenUsed="true" DefSemiHidden="true" DefQFormat="false" DefPriority="99" LatentStyleCount="276"> <w:LsdException Locked="false" Priority="0" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Normal"/> <w:LsdException Locked="false" Priority="9" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="heading 1"/> <w:LsdException Locked="false" Priority="9" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="heading 2"/> <w:LsdException Locked="false" Priority="9" QFormat="true" Name="heading 3"/> <w:LsdException Locked="false" Priority="9" QFormat="true" Name="heading 4"/> <w:LsdException Locked="false" Priority="9" QFormat="true" Name="heading 5"/> <w:LsdException Locked="false" Priority="9" QFormat="true" Name="heading 6"/> <w:LsdException Locked="false" Priority="9" QFormat="true" Name="heading 7"/> <w:LsdException Locked="false" Priority="9" QFormat="true" Name="heading 8"/> <w:LsdException Locked="false" Priority="9" QFormat="true" Name="heading 9"/> <w:LsdException Locked="false" Priority="39" Name="toc 1"/> <w:LsdException Locked="false" Priority="39" Name="toc 2"/> <w:LsdException Locked="false" Priority="39" Name="toc 3"/> <w:LsdException Locked="false" Priority="39" Name="toc 4"/> <w:LsdException Locked="false" Priority="39" Name="toc 5"/> <w:LsdException Locked="false" Priority="39" Name="toc 6"/> <w:LsdException Locked="false" Priority="39" Name="toc 7"/> <w:LsdException Locked="false" Priority="39" Name="toc 8"/> <w:LsdException Locked="false" Priority="39" Name="toc 9"/> <w:LsdException Locked="false" Priority="35" QFormat="true" Name="caption"/> <w:LsdException Locked="false" Priority="10" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Title"/> <w:LsdException Locked="false" Priority="1" Name="Default Paragraph Font"/> <w:LsdException Locked="false" Priority="11" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Subtitle"/> <w:LsdException Locked="false" Priority="22" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Strong"/> <w:LsdException Locked="false" Priority="20" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Emphasis"/> <w:LsdException Locked="false" Priority="59" SemiHidden="false" UnhideWhenUsed="false" Name="Table Grid"/> <w:LsdException Locked="false" UnhideWhenUsed="false" Name="Placeholder Text"/> <w:LsdException Locked="false" Priority="1" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="No Spacing"/> <w:LsdException Locked="false" Priority="60" SemiHidden="false" UnhideWhenUsed="false" Name="Light Shading"/> <w:LsdException Locked="false" Priority="61" SemiHidden="false" UnhideWhenUsed="false" Name="Light List"/> <w:LsdException Locked="false" Priority="62" SemiHidden="false" UnhideWhenUsed="false" Name="Light Grid"/> <w:LsdException Locked="false" Priority="63" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 1"/> <w:LsdException Locked="false" Priority="64" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 2"/> <w:LsdException Locked="false" Priority="65" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 1"/> <w:LsdException Locked="false" Priority="66" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 2"/> <w:LsdException Locked="false" Priority="67" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 1"/> <w:LsdException Locked="false" Priority="68" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 2"/> <w:LsdException Locked="false" Priority="69" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 3"/> <w:LsdException Locked="false" Priority="70" SemiHidden="false" UnhideWhenUsed="false" Name="Dark List"/> <w:LsdException Locked="false" Priority="71" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Shading"/> <w:LsdException Locked="false" Priority="72" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful List"/> <w:LsdException Locked="false" Priority="73" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Grid"/> <w:LsdException Locked="false" Priority="60" SemiHidden="false" UnhideWhenUsed="false" Name="Light Shading Accent 1"/> <w:LsdException Locked="false" Priority="61" SemiHidden="false" UnhideWhenUsed="false" Name="Light List Accent 1"/> <w:LsdException Locked="false" Priority="62" SemiHidden="false" UnhideWhenUsed="false" Name="Light Grid Accent 1"/> <w:LsdException Locked="false" Priority="63" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 1 Accent 1"/> <w:LsdException Locked="false" Priority="64" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 2 Accent 1"/> <w:LsdException Locked="false" Priority="65" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 1 Accent 1"/> <w:LsdException Locked="false" UnhideWhenUsed="false" Name="Revision"/> <w:LsdException Locked="false" Priority="34" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="List Paragraph"/> <w:LsdException Locked="false" Priority="29" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Quote"/> <w:LsdException Locked="false" Priority="30" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Intense Quote"/> <w:LsdException Locked="false" Priority="66" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 2 Accent 1"/> <w:LsdException Locked="false" Priority="67" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 1 Accent 1"/> <w:LsdException Locked="false" Priority="68" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 2 Accent 1"/> <w:LsdException Locked="false" Priority="69" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 3 Accent 1"/> <w:LsdException Locked="false" Priority="70" SemiHidden="false" UnhideWhenUsed="false" Name="Dark List Accent 1"/> <w:LsdException Locked="false" Priority="71" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Shading Accent 1"/> <w:LsdException Locked="false" Priority="72" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful List Accent 1"/> <w:LsdException Locked="false" Priority="73" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Grid Accent 1"/> <w:LsdException Locked="false" Priority="60" SemiHidden="false" UnhideWhenUsed="false" Name="Light Shading Accent 2"/> <w:LsdException Locked="false" Priority="61" SemiHidden="false" UnhideWhenUsed="false" Name="Light List Accent 2"/> <w:LsdException Locked="false" Priority="62" SemiHidden="false" UnhideWhenUsed="false" Name="Light Grid Accent 2"/> <w:LsdException Locked="false" Priority="63" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 1 Accent 2"/> <w:LsdException Locked="false" Priority="64" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 2 Accent 2"/> <w:LsdException Locked="false" Priority="65" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 1 Accent 2"/> <w:LsdException Locked="false" Priority="66" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 2 Accent 2"/> <w:LsdException Locked="false" Priority="67" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 1 Accent 2"/> <w:LsdException Locked="false" Priority="68" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 2 Accent 2"/> <w:LsdException Locked="false" Priority="69" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 3 Accent 2"/> <w:LsdException Locked="false" Priority="70" SemiHidden="false" UnhideWhenUsed="false" Name="Dark List Accent 2"/> <w:LsdException Locked="false" Priority="71" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Shading Accent 2"/> <w:LsdException Locked="false" Priority="72" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful List Accent 2"/> <w:LsdException Locked="false" Priority="73" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Grid Accent 2"/> <w:LsdException Locked="false" Priority="60" SemiHidden="false" UnhideWhenUsed="false" Name="Light Shading Accent 3"/> <w:LsdException Locked="false" Priority="61" SemiHidden="false" UnhideWhenUsed="false" Name="Light List Accent 3"/> <w:LsdException Locked="false" Priority="62" SemiHidden="false" UnhideWhenUsed="false" Name="Light Grid Accent 3"/> <w:LsdException Locked="false" Priority="63" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 1 Accent 3"/> <w:LsdException Locked="false" Priority="64" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 2 Accent 3"/> <w:LsdException Locked="false" Priority="65" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 1 Accent 3"/> <w:LsdException Locked="false" Priority="66" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 2 Accent 3"/> <w:LsdException Locked="false" Priority="67" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 1 Accent 3"/> <w:LsdException Locked="false" Priority="68" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 2 Accent 3"/> <w:LsdException Locked="false" Priority="69" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 3 Accent 3"/> <w:LsdException Locked="false" Priority="70" SemiHidden="false" UnhideWhenUsed="false" Name="Dark List Accent 3"/> <w:LsdException Locked="false" Priority="71" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Shading Accent 3"/> <w:LsdException Locked="false" Priority="72" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful List Accent 3"/> <w:LsdException Locked="false" Priority="73" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Grid Accent 3"/> <w:LsdException Locked="false" Priority="60" SemiHidden="false" UnhideWhenUsed="false" Name="Light Shading Accent 4"/> <w:LsdException Locked="false" Priority="61" SemiHidden="false" UnhideWhenUsed="false" Name="Light List Accent 4"/> <w:LsdException Locked="false" Priority="62" SemiHidden="false" UnhideWhenUsed="false" Name="Light Grid Accent 4"/> <w:LsdException Locked="false" Priority="63" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 1 Accent 4"/> <w:LsdException Locked="false" Priority="64" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 2 Accent 4"/> <w:LsdException Locked="false" Priority="65" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 1 Accent 4"/> <w:LsdException Locked="false" Priority="66" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 2 Accent 4"/> <w:LsdException Locked="false" Priority="67" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 1 Accent 4"/> <w:LsdException Locked="false" Priority="68" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 2 Accent 4"/> <w:LsdException Locked="false" Priority="69" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 3 Accent 4"/> <w:LsdException Locked="false" Priority="70" SemiHidden="false" UnhideWhenUsed="false" Name="Dark List Accent 4"/> <w:LsdException Locked="false" Priority="71" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Shading Accent 4"/> <w:LsdException Locked="false" Priority="72" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful List Accent 4"/> <w:LsdException Locked="false" Priority="73" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Grid Accent 4"/> <w:LsdException Locked="false" Priority="60" SemiHidden="false" UnhideWhenUsed="false" Name="Light Shading Accent 5"/> <w:LsdException Locked="false" Priority="61" SemiHidden="false" UnhideWhenUsed="false" Name="Light List Accent 5"/> <w:LsdException Locked="false" Priority="62" SemiHidden="false" UnhideWhenUsed="false" Name="Light Grid Accent 5"/> <w:LsdException Locked="false" Priority="63" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 1 Accent 5"/> <w:LsdException Locked="false" Priority="64" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 2 Accent 5"/> <w:LsdException Locked="false" Priority="65" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 1 Accent 5"/> <w:LsdException Locked="false" Priority="66" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 2 Accent 5"/> <w:LsdException Locked="false" Priority="67" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 1 Accent 5"/> <w:LsdException Locked="false" Priority="68" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 2 Accent 5"/> <w:LsdException Locked="false" Priority="69" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 3 Accent 5"/> <w:LsdException Locked="false" Priority="70" SemiHidden="false" UnhideWhenUsed="false" Name="Dark List Accent 5"/> <w:LsdException Locked="false" Priority="71" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Shading Accent 5"/> <w:LsdException Locked="false" Priority="72" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful List Accent 5"/> <w:LsdException Locked="false" Priority="73" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Grid Accent 5"/> <w:LsdException Locked="false" Priority="60" SemiHidden="false" UnhideWhenUsed="false" Name="Light Shading Accent 6"/> <w:LsdException Locked="false" Priority="61" SemiHidden="false" UnhideWhenUsed="false" Name="Light List Accent 6"/> <w:LsdException Locked="false" Priority="62" SemiHidden="false" UnhideWhenUsed="false" Name="Light Grid Accent 6"/> <w:LsdException Locked="false" Priority="63" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 1 Accent 6"/> <w:LsdException Locked="false" Priority="64" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Shading 2 Accent 6"/> <w:LsdException Locked="false" Priority="65" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 1 Accent 6"/> <w:LsdException Locked="false" Priority="66" SemiHidden="false" UnhideWhenUsed="false" Name="Medium List 2 Accent 6"/> <w:LsdException Locked="false" Priority="67" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 1 Accent 6"/> <w:LsdException Locked="false" Priority="68" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 2 Accent 6"/> <w:LsdException Locked="false" Priority="69" SemiHidden="false" UnhideWhenUsed="false" Name="Medium Grid 3 Accent 6"/> <w:LsdException Locked="false" Priority="70" SemiHidden="false" UnhideWhenUsed="false" Name="Dark List Accent 6"/> <w:LsdException Locked="false" Priority="71" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Shading Accent 6"/> <w:LsdException Locked="false" Priority="72" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful List Accent 6"/> <w:LsdException Locked="false" Priority="73" SemiHidden="false" UnhideWhenUsed="false" Name="Colorful Grid Accent 6"/> <w:LsdException Locked="false" Priority="19" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Subtle Emphasis"/> <w:LsdException Locked="false" Priority="21" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Intense Emphasis"/> <w:LsdException Locked="false" Priority="31" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Subtle Reference"/> <w:LsdException Locked="false" Priority="32" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Intense Reference"/> <w:LsdException Locked="false" Priority="33" SemiHidden="false" UnhideWhenUsed="false" QFormat="true" Name="Book Title"/> <w:LsdException Locked="false" Priority="37" Name="Bibliography"/> <w:LsdException Locked="false" Priority="39" QFormat="true" Name="TOC Heading"/> </w:LatentStyles> </xml><![endif]--> <style> <!-- /* Font Definitions */ @font-face {font-family:"Courier New"; panose-1:2 7 3 9 2 2 5 2 4 4; mso-font-charset:0; mso-generic-font-family:auto; mso-font-pitch:variable; mso-font-signature:3 0 0 0 1 0;} @font-face {font-family:Times; panose-1:2 0 5 0 0 0 0 0 0 0; mso-font-charset:0; mso-generic-font-family:auto; mso-font-pitch:variable; mso-font-signature:3 0 0 0 1 0;} @font-face {font-family:Wingdings; panose-1:5 0 0 0 0 0 0 0 0 0; mso-font-charset:2; mso-generic-font-family:auto; mso-font-pitch:variable; mso-font-signature:0 268435456 0 0 -2147483648 0;} @font-face {font-family:"-ÿ3ÿ fg"; panose-1:0 0 0 0 0 0 0 0 0 0; mso-font-charset:128; mso-generic-font-family:roman; mso-font-format:other; mso-font-pitch:fixed; mso-font-signature:1 134676480 16 0 131072 0;} @font-face {font-family:"-ÿ3ÿ fg"; panose-1:0 0 0 0 0 0 0 0 0 0; mso-font-charset:128; mso-generic-font-family:roman; mso-font-format:other; mso-font-pitch:fixed; mso-font-signature:1 134676480 16 0 131072 0;} /* Style Definitions */ p.MsoNormal, li.MsoNormal, div.MsoNormal {mso-style-unhide:no; mso-style-qformat:yes; mso-style-parent:""; margin:0cm; margin-bottom:.0001pt; mso-pagination:widow-orphan; font-size:10.0pt; font-family:Times; mso-fareast-font-family:"-ÿ3ÿ fg"; mso-fareast-theme-font:minor-fareast; mso-bidi-font-family:"Times New Roman"; mso-bidi-theme-font:minor-bidi;} h1 {mso-style-priority:9; mso-style-unhide:no; mso-style-qformat:yes; mso-style-link:"Heading 1 Char"; mso-margin-top-alt:auto; margin-right:0cm; mso-margin-bottom-alt:auto; margin-left:0cm; mso-pagination:widow-orphan; mso-outline-level:1; font-size:24.0pt; font-family:Times; mso-fareast-font-family:"-ÿ3ÿ fg"; mso-fareast-theme-font:minor-fareast; mso-bidi-font-family:"Times New Roman"; mso-bidi-theme-font:minor-bidi; font-weight:bold;} h2 {mso-style-priority:9; mso-style-unhide:no; mso-style-qformat:yes; mso-style-link:"Heading 2 Char"; mso-margin-top-alt:auto; margin-right:0cm; mso-margin-bottom-alt:auto; margin-left:0cm; mso-pagination:widow-orphan; mso-outline-level:2; font-size:18.0pt; font-family:Times; mso-fareast-font-family:"-ÿ3ÿ fg"; mso-fareast-theme-font:minor-fareast; mso-bidi-font-family:"Times New Roman"; mso-bidi-theme-font:minor-bidi; font-weight:bold;} a:link, span.MsoHyperlink {mso-style-noshow:yes; mso-style-priority:99; color:blue; text-decoration:underline; text-underline:single;} a:visited, span.MsoHyperlinkFollowed {mso-style-noshow:yes; mso-style-priority:99; color:purple; text-decoration:underline; text-underline:single;} p {mso-style-noshow:yes; mso-style-priority:99; mso-margin-top-alt:auto; margin-right:0cm; mso-margin-bottom-alt:auto; margin-left:0cm; mso-pagination:widow-orphan; font-size:10.0pt; font-family:Times; mso-fareast-font-family:"-ÿ3ÿ fg"; mso-fareast-theme-font:minor-fareast; mso-bidi-font-family:"Times New Roman";} span.Heading1Char {mso-style-name:"Heading 1 Char"; mso-style-priority:9; mso-style-unhide:no; mso-style-locked:yes; mso-style-link:"Heading 1"; mso-ansi-font-size:16.0pt; mso-bidi-font-size:16.0pt; font-family:Calibri; mso-ascii-font-family:Calibri; mso-ascii-theme-font:major-latin; mso-fareast-font-family:"-ÿ3ÿ ´0·0Ã0¯0"; mso-fareast-theme-font:major-fareast; mso-hansi-font-family:Calibri; mso-hansi-theme-font:major-latin; mso-bidi-font-family:"Times New Roman"; mso-bidi-theme-font:major-bidi; color:#345A8A; mso-themecolor:accent1; mso-themeshade:181; font-weight:bold;} span.Heading2Char {mso-style-name:"Heading 2 Char"; mso-style-noshow:yes; mso-style-priority:9; mso-style-unhide:no; mso-style-locked:yes; mso-style-link:"Heading 2"; mso-ansi-font-size:13.0pt; mso-bidi-font-size:13.0pt; font-family:Calibri; mso-ascii-font-family:Calibri; mso-ascii-theme-font:major-latin; mso-fareast-font-family:"-ÿ3ÿ ´0·0Ã0¯0"; mso-fareast-theme-font:major-fareast; mso-hansi-font-family:Calibri; mso-hansi-theme-font:major-latin; mso-bidi-font-family:"Times New Roman"; mso-bidi-theme-font:major-bidi; color:#4F81BD; mso-themecolor:accent1; font-weight:bold;} span.SpellE {mso-style-name:""; mso-spl-e:yes;} span.GramE {mso-style-name:""; mso-gram-e:yes;} .MsoChpDefault {mso-style-type:export-only; mso-default-props:yes; font-size:10.0pt; mso-ansi-font-size:10.0pt; mso-bidi-font-size:10.0pt;} @page WordSection1 {size:612.0pt 792.0pt; margin:72.0pt 90.0pt 72.0pt 90.0pt; mso-header-margin:35.4pt; mso-footer-margin:35.4pt; mso-paper-source:0;} div.WordSection1 {page:WordSection1;} /* List Definitions */ @list l0 {mso-list-id:1468664698; mso-list-template-ids:-134950348;} @list l0:level1 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:36.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l0:level2 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:72.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l0:level3 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:108.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l0:level4 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:144.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l0:level5 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:180.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l0:level6 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:216.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l0:level7 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:252.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l0:level8 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:288.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l0:level9 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:324.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l1 {mso-list-id:1575966614; mso-list-template-ids:-543903850;} @list l1:level1 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:36.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l1:level2 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:72.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l1:level3 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:108.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l1:level4 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:144.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l1:level5 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:180.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l1:level6 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:216.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l1:level7 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:252.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l1:level8 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:288.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l1:level9 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:324.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l2 {mso-list-id:1883521337; mso-list-template-ids:-573259066;} @list l2:level1 {mso-level-number-format:bullet; mso-level-text:·ð; mso-level-tab-stop:36.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Symbol;} @list l2:level2 {mso-level-number-format:bullet; mso-level-text:o; mso-level-tab-stop:72.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:"Courier New";} @list l2:level3 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:108.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Wingdings;} @list l2:level4 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:144.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Wingdings;} @list l2:level5 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:180.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Wingdings;} @list l2:level6 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:216.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Wingdings;} @list l2:level7 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:252.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Wingdings;} @list l2:level8 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:288.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Wingdings;} @list l2:level9 {mso-level-number-format:bullet; mso-level-text:§ð; mso-level-tab-stop:324.0pt; mso-level-number-position:left; text-indent:-18.0pt; mso-ansi-font-size:10.0pt; font-family:Wingdings;} ol {margin-bottom:0cm;} ul {margin-bottom:0cm;} --> </style> <!--[if gte mso 10]> <style> /* Style Definitions */ table.MsoNormalTable {mso-style-name:"Table Normal"; mso-tstyle-rowband-size:0; mso-tstyle-colband-size:0; mso-style-noshow:yes; mso-style-priority:99; mso-style-parent:""; mso-padding-alt:0cm 5.4pt 0cm 5.4pt; mso-para-margin:0cm; mso-para-margin-bottom:.0001pt; mso-pagination:widow-orphan; font-size:10.0pt; font-family:"Times New Roman";} </style> <![endif]--><!--[if gte mso 9]><xml> <o:shapedefaults v:ext="edit" spidmax="1027"/> </xml><![endif]--><!--[if gte mso 9]><xml> <o:shapelayout v:ext="edit"> <o:idmap v:ext="edit" data="1"/> </o:shapelayout></xml><![endif]--> </head> <body bgcolor=white lang=EN-US link=blue vlink=purple style='tab-interval:36.0pt'> <div class=WordSection1> <h1><span style='mso-fareast-font-family:"Times New Roman";mso-bidi-font-family: "Times New Roman"'>02246: Model Checking<o:p></o:p></span></h1> <h2><span style='mso-fareast-font-family:"Times New Roman";mso-bidi-font-family: "Times New Roman"'>Dates<o:p></o:p></span></h2> <p><span style='font-size:12.0pt'>The course spans the period 29<sup>th</sup> August 2011  2<sup>nd</sup> December 2011. <o:p></o:p></span></p> <p><span style='font-size:12.0pt'>Lectures and tutorials take place in <b>building 322, room 033 </b>every <b>Tuesday, from 13:00</b>. <o:p></o:p></span></p> <p><span style='font-size:12.0pt'>Oral exams will take place on Monday December 19<sup>th</sup> and Tuesday December 20<sup>th</sup>; the external examiner is Thomas Hildebrandt.<o:p></o:p></span></p> <h2><span style='mso-fareast-font-family:"Times New Roman";mso-bidi-font-family: "Times New Roman"'>Lecturers<o:p></o:p></span></h2> <p class=MsoNormal><span style='font-size:12.0pt;mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'><a href="http://www2.imm.dtu.dk/~nielson/">Flemming Nielson</a>, <a href="http://www2.imm.dtu.dk/~lizh/">Lijun Zhang</a>. <o:p></o:p></span></p> <h2><span style='mso-fareast-font-family:"Times New Roman";mso-bidi-font-family: "Times New Roman"'>Textbooks and Course Materials<o:p></o:p></span></h2> <ul type=disc> <li class=MsoNormalCxSpFirst style='mso-margin-top-alt:auto;mso-margin-bottom-alt: auto;mso-add-space:auto;mso-list:l2 level1 lfo3;tab-stops:list 36.0pt'><span style='font-size:12.0pt;mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>[BK08] <span class=SpellE>Christel</span> <span class=SpellE>Baier</span> and <span class=SpellE>Joost</span>-Pieter <span class=SpellE>Katoen</span>, Principles of Model Checking, MIT Press. <o:p></o:p></span></li> </ul> <p class=MsoNormalCxSpMiddle style='mso-margin-top-alt:auto;mso-margin-bottom-alt: auto;margin-left:36.0pt;mso-add-space:auto'><span style='font-size:12.0pt; mso-fareast-font-family:"Times New Roman";mso-bidi-font-family:"Times New Roman"'>You can purchase the book <a href="http://www.polyteknisk.dk/home/dtu/soege_resultat?q=02246&amp;booklist_search=1&amp;booklist_id=20">here, from the university <span class=GramE>book store</span>.</a> <o:p></o:p></span></p> <p class=MsoNormal style='mso-margin-top-alt:auto;mso-margin-bottom-alt:auto; margin-left:36.0pt'><span style='font-size:12.0pt;mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'><a href="http://mitpress.mit.edu/books/chapters/026202649Xerrata.pdf">Please find errata for the book here.</a> <o:p></o:p></span></p> <ul type=disc> <li class=MsoNormal style='mso-margin-top-alt:auto;mso-margin-bottom-alt:auto; mso-list:l2 level1 lfo3;tab-stops:list 36.0pt'><span style='font-size: 12.0pt;mso-fareast-font-family:"Times New Roman";mso-bidi-font-family: "Times New Roman"'>The course handouts will be made available for cash purchase at the Reception at DTU Informatics in building 305; they may be used as a substitute for [BK08] but we do recommend buying the book rather than the handout. <o:p></o:p></span></li> </ul> <h2><span style='mso-fareast-font-family:"Times New Roman";mso-bidi-font-family: "Times New Roman"'>Course Schedule (subject to changes)<o:p></o:p></span></h2> <table class=MsoNormalTable border=1 cellpadding=0 width=581 style='width:581.35pt; mso-cellspacing:1.5pt;mso-yfti-tbllook:1184;mso-padding-alt:0cm 5.4pt 0cm 5.4pt'> <tr style='mso-yfti-irow:0;mso-yfti-firstrow:yes;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal align=center style='text-align:center'><b><span style='mso-fareast-font-family:"Times New Roman";mso-bidi-font-family:"Times New Roman"'>Date<o:p></o:p></span></b></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal align=center style='text-align:center'><b><span style='mso-fareast-font-family:"Times New Roman";mso-bidi-font-family:"Times New Roman"'>Topic<o:p></o:p></span></b></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal align=center style='text-align:center'><b><span style='mso-fareast-font-family:"Times New Roman";mso-bidi-font-family:"Times New Roman"'>Reading Material<o:p></o:p></span></b></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal align=center style='text-align:center'><b><span style='mso-fareast-font-family:"Times New Roman";mso-bidi-font-family:"Times New Roman"'>Supplementary Material (on Campus Net)<o:p></o:p></span></b></p> </td> </tr> <tr style='mso-yfti-irow:1;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>August 30<sup>th</sup><o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Introduction to the course. <o:p></o:p></span></p> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Overview of model checking and software validation.<o:p></o:p></span></p> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Installing (or using) PRISM.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Mandatory Assignment Part 0: Background and Getting Started.<o:p></o:p></span></p> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Slides Lect1 and Exe1.<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:2;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>September 6<sup>th</sup> <o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Transition Systems.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Sections 2, 2.1, 2.2.1 and 2.2.6 of [BK08].<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Mandatory Assignment Part 1: Discrete <span class=SpellE>Modelling</span> and Verification.<o:p></o:p></span></p> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Slides Lect2 and Exe2.<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:3;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>September 13<sup>th</sup> <o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Computation Tree Logic (CTL).<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Sections 6, 6.1, 6.2 of [BK08].<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Slides Lect3 and Exe3.<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:4;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>September 20<sup>th</sup> <o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>CTL Model Checking.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Sections 6.4, a bit of 6.8 of [BK08].<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Slides Lect4 and Exe4.<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:5;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>September 27<sup>th</sup> <o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>CTL Model Checking.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Sections 6.4, a bit of 6.8 of [BK08].<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Slides Lect5 and Exe5.<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:6;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>October 4<sup>th</sup><o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span class=SpellE><span style='mso-fareast-font-family: "Times New Roman";mso-bidi-font-family:"Times New Roman"'>Bisimulation</span></span><span style='mso-fareast-font-family:"Times New Roman";mso-bidi-font-family:"Times New Roman"'>.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Sections 7, 7.1.1, 7.2 of [BK08].<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Slides Lect6 and Exe6.<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:7;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>October 11<sup>th</sup> <o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Introduction to Markov chains.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Sections 10, 10.1 of [BK08]<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Slides Lect7 and Exe 7.<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:8;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman";background:yellow;mso-highlight:yellow'>October <span class=GramE>14<sup>th</sup><span style="mso-spacerun:yes">  </span>08:00</span><o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman";background:yellow;mso-highlight:yellow'>HAND IN FIRST MANDATORY ASSIGNMENT<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman";background:yellow;mso-highlight:yellow'>.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman";background:yellow;mso-highlight:yellow'>.<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:9;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>October 25<sup>th</sup> <o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Probabilistic CTL, transient and steady state distributions.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Sections 10.1.1, 10.2 of [BK08]<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Slides Lect8 and Exe8<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:10;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>November 1<sup>st</sup> <o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>The Qualitative Fragment of PCTL.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Section 10.2.2 of [BK08]<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Slides Lect9 and Exe9<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:11;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>November 8<sup>th</sup> <o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>PCTL Model Checking.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Sections 10.1.1, 10.2.1 of [BK08]<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Slides Lect10 and Exe10<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:12;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>November 15<sup>th</sup> <o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Probabilistic <span class=SpellE>Bisimulation</span>.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Section 10.4.2 of [BK08]<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Slides Lect11 and Exe11<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:13;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>November <span class=GramE>22<sup>nd</sup><span style="mso-spacerun:yes">  </span></span><o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Work on the second mandatory assignment.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>.<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:14;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman";background:yellow;mso-highlight:yellow'>November 28<sup>th</sup> 08:00<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman";background:yellow;mso-highlight:yellow'>HAND IN SECOND MANDATORY ASSIGNMENT<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman";background:yellow;mso-highlight:yellow'>.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman";background:yellow;mso-highlight:yellow'>.<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:15;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>November 29<sup>th</sup> <o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Beyond CTL and PCTL.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>.<o:p></o:p></span></p> </td> </tr> <tr style='mso-yfti-irow:16;mso-yfti-lastrow:yes;height:9.7pt'> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>December <span class=GramE>19<sup>th</sup> <span style="mso-spacerun:yes"> </span>and</span> 20<sup>th</sup> <span style="mso-spacerun:yes"> </span><o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>Oral exam.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>.<o:p></o:p></span></p> </td> <td style='padding:.75pt .75pt .75pt .75pt;height:9.7pt'> <p class=MsoNormal><span style='mso-fareast-font-family:"Times New Roman"; mso-bidi-font-family:"Times New Roman"'>.<o:p></o:p></span></p> </td> </tr> </table> <h2><span style='mso-fareast-font-family:"Times New Roman";mso-bidi-font-family: "Times New Roman"'><a href="details.html">Motivation for the Course</a><o:p></o:p></span></h2> </div> </body> </html>