{"id":7405,"date":"2024-06-14T22:49:18","date_gmt":"2024-06-14T14:49:18","guid":{"rendered":"http:\/\/tsinghualogic.net\/JRC\/?page_id=7405"},"modified":"2024-07-12T10:04:27","modified_gmt":"2024-07-12T02:04:27","slug":"modal-%ce%bc-calculus","status":"publish","type":"page","link":"http:\/\/tsinghualogic.net\/JRC\/modal-%ce%bc-calculus\/","title":{"rendered":"Modal \u03bc-calculus"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-page\" data-elementor-id=\"7405\" class=\"elementor elementor-7405\" data-elementor-settings=\"[]\">\n\t\t\t\t\t\t\t<div class=\"elementor-section-wrap\">\n\t\t\t\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-03b15e6 elementor-section-content-middle elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"03b15e6\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-66 elementor-top-column elementor-element elementor-element-417c3e7\" data-id=\"417c3e7\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-a083358 elementor-widget elementor-widget-text-editor\" data-id=\"a083358\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<style>\/*! elementor - v3.5.6 - 28-02-2022 *\/\n.elementor-widget-text-editor.elementor-drop-cap-view-stacked .elementor-drop-cap{background-color:#818a91;color:#fff}.elementor-widget-text-editor.elementor-drop-cap-view-framed .elementor-drop-cap{color:#818a91;border:3px solid;background-color:transparent}.elementor-widget-text-editor:not(.elementor-drop-cap-view-default) .elementor-drop-cap{margin-top:8px}.elementor-widget-text-editor:not(.elementor-drop-cap-view-default) .elementor-drop-cap-letter{width:1em;height:1em}.elementor-widget-text-editor .elementor-drop-cap{float:left;text-align:center;line-height:1;font-size:50px}.elementor-widget-text-editor .elementor-drop-cap-letter{display:inline-block}<\/style>\t\t\t\t<ul><li><strong>Time<\/strong>: 2:20 PM-4:55 PM, 8th July-12th July<\/li><li><strong>Location<\/strong>: Room 3104, Teaching Building No.3, Tsinghua University<\/li><li><strong>Lecturer<\/strong>: Yde Venema (University of Amsterdam)<\/li><li><strong>Teaching Assistants<\/strong>: Xi Yang (x-yang23@mails.tsinghua.edu.cn), Zhaorui Hu, Yichen Zhao (zhao-yc23@mails.tsinghua.edu.cn)<\/li><li><strong>On-campus course name and course number<\/strong>: \u4eba\u5de5\u667a\u80fd\u7684\u903b\u8f91\u57fa\u7840\uff0800692441-90\uff09<\/li><\/ul>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t<div class=\"elementor-column elementor-col-33 elementor-top-column elementor-element elementor-element-9ed4748\" data-id=\"9ed4748\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-d4c43c0 elementor-widget elementor-widget-text-editor\" data-id=\"d4c43c0\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t<p><img decoding=\"async\" loading=\"lazy\" class=\"aligncenter wp-image-7407 size-full\" src=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/06\/download-1-e1718377020828.jpg\" alt=\"\" width=\"221\" height=\"217\" srcset=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/06\/download-1-e1718377020828.jpg 221w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/06\/download-1-e1718377020828-200x196.jpg 200w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/06\/download-1-e1718377020828-80x80.jpg 80w\" sizes=\"(max-width: 221px) 100vw, 221px\" \/><\/p><p style=\"text-align: center;\"><a href=\"https:\/\/theory.amsterdam\/author\/yde-venema\/\">Yde Venema<\/a><\/p><p style=\"text-align: center;\">\u00a0<\/p>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-f701e7a elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"f701e7a\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-b074916\" data-id=\"b074916\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-c9c4f47 elementor-widget elementor-widget-heading\" data-id=\"c9c4f47\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<style>\/*! elementor - v3.5.6 - 28-02-2022 *\/\n.elementor-heading-title{padding:0;margin:0;line-height:1}.elementor-widget-heading .elementor-heading-title[class*=elementor-size-]>a{color:inherit;font-size:inherit;line-height:inherit}.elementor-widget-heading .elementor-heading-title.elementor-size-small{font-size:15px}.elementor-widget-heading .elementor-heading-title.elementor-size-medium{font-size:19px}.elementor-widget-heading .elementor-heading-title.elementor-size-large{font-size:29px}.elementor-widget-heading .elementor-heading-title.elementor-size-xl{font-size:39px}.elementor-widget-heading .elementor-heading-title.elementor-size-xxl{font-size:59px}<\/style><h3 class=\"elementor-heading-title elementor-size-default\">Syllabus<\/h3>\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-d079d83 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"d079d83\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-481e012\" data-id=\"481e012\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-8b61877 elementor-widget elementor-widget-text-editor\" data-id=\"8b61877\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t<div><strong>Prerequisites<\/strong>: basics of modal logic (syntax and semantics of polymodal logic, bisimulations)<\/div><div>\u00a0<\/div><div><strong>Course content<\/strong>:<\/div><ol start=\"1\" data-editing-info=\"{&quot;orderedStyleType&quot;:1,&quot;unorderedStyleType&quot;:1}\" data-listchain=\"__List_Chain_43\"><li><div>Introduction: modal fixpoint logics and their game semantics; syntax of the modal mu-calculus<\/div><\/li><li><div>Game semantics of the modal mu-calculus; bisimulation invariance &amp; tree model property<\/div><\/li><li><div>Fixpoint theory and compositional semantics of the modal mu-calculus<\/div><\/li><li><div>Some model theory; finite model property &amp; preservation theorems<\/div><\/li><li><div>Tableau games and the decidability of the satisfiability problem.<\/div><\/li><\/ol>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-d36beb0 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"d36beb0\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-b07146d\" data-id=\"b07146d\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-50097fa elementor-widget elementor-widget-heading\" data-id=\"50097fa\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h3 class=\"elementor-heading-title elementor-size-default\">Notes and Exercises<\/h3>\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-b7f4c29 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"b7f4c29\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-9da4dba\" data-id=\"9da4dba\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-e7b472f elementor-widget elementor-widget-text-editor\" data-id=\"e7b472f\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t<p>Note: <a href=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/07\/modal-mu-calculus.pdf\">modal mu-calculus<\/a>, <a href=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/07\/tsinghua-notes-vs2.pdf\">tsinghua-notes-vs2<\/a><\/p>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-7ad2788 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"7ad2788\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-47fa906\" data-id=\"47fa906\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-b5d4398 elementor-widget elementor-widget-text-editor\" data-id=\"b5d4398\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t<p>Day 1: <a href=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/07\/homework_1-1.pdf\">homework_1<\/a><\/p><p>Day 2: <a href=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/07\/homework_2.pdf\">homework_2<\/a><\/p><p>Day 3: <a href=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/07\/homework3.pdf\">homework3<\/a><\/p><p>Day 4: <a href=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/07\/homework4.pdf\">homework4<\/a><\/p><p>\u00a0<\/p>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t","protected":false},"excerpt":{"rendered":"<p>Time: 2:20 PM-4:55 PM, 8th July-12th July Location: Roo [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7405"}],"collection":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/comments?post=7405"}],"version-history":[{"count":18,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7405\/revisions"}],"predecessor-version":[{"id":7518,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7405\/revisions\/7518"}],"wp:attachment":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/media?parent=7405"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}