{"id":314,"date":"2015-05-26T17:15:56","date_gmt":"2015-05-26T15:15:56","guid":{"rendered":"http:\/\/logica.dmi.unisa.it\/tacl\/?p=314"},"modified":"2015-10-23T14:09:07","modified_gmt":"2015-10-23T12:09:07","slug":"tacl-school-course-by-luke-ong","status":"publish","type":"post","link":"http:\/\/logica.dipmat.unisa.it\/tacl\/tacl-school-course-by-luke-ong\/","title":{"rendered":"TACL school: course by Luke Ong"},"content":{"rendered":"<p><img loading=\"lazy\" decoding=\"async\" class=\" size-medium wp-image-152 alignleft\" src=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/2014\/12\/lukeong-199x300.jpg\" alt=\"Luke Ong\" width=\"199\" height=\"300\" srcset=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/2014\/12\/lukeong-199x300.jpg 199w, http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/2014\/12\/lukeong.jpg 341w\" sizes=\"auto, (max-width: 199px) 100vw, 199px\" \/><br \/>\n<strong>Title<\/strong>: &#8220;Automata, Logic and Games for Higher-Order Model Checking&#8221;<\/p>\n<p><strong>Course description<\/strong>:\u00a0In Part 1 of the course, we introduce the mathematical theory\u00a0underpinning the model checking of computing systems. The main\u00a0ingredients are:<\/p>\n<ul>\n<li>Automata on infinite trees as a computational model of state-based systems.<\/li>\n<li>Logical systems, such as the modal mu-calculus and monadic\u00a0second-order logic, for describing correctness properties.<\/li>\n<li>Two-person games as a conceptual basis for understanding the\u00a0interactions between a system and its environment.<\/li>\n<\/ul>\n<p>Some topics: decidability of the MSO theory of the full binary tree,\u00a0and its consequences; connections between parity games, modal\u00a0mu-calculus, and alternating parity tree automata, and the sense in\u00a0which they are equivalent.<\/p>\n<p>Building on these foundations, we discuss, in Part 2, recent\u00a0developments in high-order model checking, the model checking of\u00a0infinite trees generated by higher-order recursion schemes (or\u00a0equivalently lambda-Y calculus). Some topics: decidability of\u00a0higher-order model checking with respect to modal mu-calculus, and\u00a0compositional model checking of higher-type B\u00f6hm trees.<\/p>\n<p>&nbsp;<\/p>\n<p><strong>Lecture notes 1<\/strong>:\u00a0<a href=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/2015\/05\/AutomataLogicGames2015.pdf\">Automata Logic Games 2015<\/a><\/p>\n<p><strong>Lecture notes 2<\/strong>:\u00a0<a href=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/2015\/05\/LICS15-Higher-Order_Model_Checking.pdf\">Higher-Order Model Checking: An Overview<\/a><\/p>\n<p><strong>Slides and more on<\/strong>\u00a0<a href=\"http:\/\/www.cs.ox.ac.uk\/people\/luke.ong\/personal\/TACL15\">Luke Ong&#8217;s webpage of the course<\/a><\/p>\n<p>&nbsp;<br \/>\nLecture 1 video<\/p>\n<div style=\"width: 640px;\" class=\"wp-video\"><!--[if lt IE 9]><script>document.createElement('video');<\/script><![endif]-->\n<video class=\"wp-video-shortcode\" id=\"video-314-1\" width=\"640\" height=\"360\" preload=\"metadata\" controls=\"controls\"><source type=\"video\/mp4\" src=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-1.mp4?_=1\" \/><a href=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-1.mp4\">http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-1.mp4<\/a><\/video><\/div>\n<p>Lecture 2 video<\/p>\n<div style=\"width: 640px;\" class=\"wp-video\"><video class=\"wp-video-shortcode\" id=\"video-314-2\" width=\"640\" height=\"360\" preload=\"metadata\" controls=\"controls\"><source type=\"video\/mp4\" src=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-2.mp4?_=2\" \/><a href=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-2.mp4\">http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-2.mp4<\/a><\/video><\/div>\n<p>Lecture 3 video<\/p>\n<div style=\"width: 640px;\" class=\"wp-video\"><video class=\"wp-video-shortcode\" id=\"video-314-3\" width=\"640\" height=\"360\" preload=\"metadata\" controls=\"controls\"><source type=\"video\/mp4\" src=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-3.mp4?_=3\" \/><a href=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-3.mp4\">http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-3.mp4<\/a><\/video><\/div>\n<p>Lecture 4 video<\/p>\n<div style=\"width: 640px;\" class=\"wp-video\"><video class=\"wp-video-shortcode\" id=\"video-314-4\" width=\"640\" height=\"360\" preload=\"metadata\" controls=\"controls\"><source type=\"video\/mp4\" src=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-4.mp4?_=4\" \/><a href=\"http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-4.mp4\">http:\/\/logica.dmi.unisa.it\/tacl\/wp-content\/uploads\/video\/Ong-lecture-4.mp4<\/a><\/video><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Title: &#8220;Automata, Logic and Games for Higher-Order Model Checking&#8221; Course description:\u00a0In Part 1 of the course, we introduce the mathematical theory\u00a0underpinning the model checking of computing systems. The main\u00a0ingredients are: Automata on infinite trees as a computational model of state-based systems. Logical systems, such as the modal mu-calculus and monadic\u00a0second-order logic, for describing correctness properties. [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[8,7],"tags":[],"class_list":["post-314","post","type-post","status-publish","format-standard","hentry","category-course-descriptions","category-tacl-school"],"_links":{"self":[{"href":"http:\/\/logica.dipmat.unisa.it\/tacl\/wp-json\/wp\/v2\/posts\/314","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/logica.dipmat.unisa.it\/tacl\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/logica.dipmat.unisa.it\/tacl\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/logica.dipmat.unisa.it\/tacl\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/logica.dipmat.unisa.it\/tacl\/wp-json\/wp\/v2\/comments?post=314"}],"version-history":[{"count":7,"href":"http:\/\/logica.dipmat.unisa.it\/tacl\/wp-json\/wp\/v2\/posts\/314\/revisions"}],"predecessor-version":[{"id":576,"href":"http:\/\/logica.dipmat.unisa.it\/tacl\/wp-json\/wp\/v2\/posts\/314\/revisions\/576"}],"wp:attachment":[{"href":"http:\/\/logica.dipmat.unisa.it\/tacl\/wp-json\/wp\/v2\/media?parent=314"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/logica.dipmat.unisa.it\/tacl\/wp-json\/wp\/v2\/categories?post=314"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/logica.dipmat.unisa.it\/tacl\/wp-json\/wp\/v2\/tags?post=314"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}