Ichiro Hasuo

• Department of Computer Science
• University of Tokyo
• ichiro [at] is.s.u-tokyo.ac.jp

• English
• Japanese
• Dutch
• Chinese

• Home
• Contact
• Research
• Cv
• Papers
• Talks
• Teaching

[Back to Teaching]

計算機言語論 (2015年度，前半・蓮尾担当分)

概要

• Sセメスター 月曜3限 13:00 - 14:45
• 理学部7号館 007号室
• 理学部情報科学科 4年生 選択必修 時間割コード： 0510055
• 講義は日本語で行う．

担当教員，講義の内容

• 前半： 蓮尾 一郎 講師 (理学部情報科学科)，オートマトンによる時相論理式モデル検査
• 後半： 小林 直樹 教授 (理学部情報科学科)，木オートマトンと高階モデル検査

講義の方法

教科書と，各回に配布するハンドアウトに基づき，板書で行う．

• 口頭説明は(おそらく)日本語，板書は英語．(どうせみんな英語で卒論書くのだ)
• 各回の内容は，前回の講義時に配布するハンドアウトの中で予告する．予習が推奨される．(ぜひ，少なくとも，電車の中でざっと眺めてきてください)
• 時々出題するレポート課題(下参照)は，復習問題が1つ，予習問題が1つ．

教科書・ハンドアウト

このページで配布する資料は，すべて学内のみからアクセス可能．

• 教科書: 次の2つを用いる．
  • Moshe Y. Vardi: An Automata-Theoretic Approach to Linear Temporal Logic. Banff Higher Order Workshop 1995: 238-266
  • S. Demri and P. Gastin. Specification and Verification using Temporal Logics. In Modern applications of automata theory, IISc Research Monographs 2, chapter 15, pages 457-494. World Scientific, 2012.
• 毎回のハンドアウト: 下の「スケジュール」の項を参照．

評価(前半・蓮尾担当分に関して)

以下の要素により，総合的に判断する．

• 毎回のレポート課題
• 出席確認を兼ねる．
• 毎週，講義開始前に直接提出．講義開始後は一切受け取らない．
• A4用紙に手書きか，出力したものを提出．
• レポート課題は，ハンドアウトの中で指定．
• 想定ワークロード: 講義時間の他に，予習・復習・レポートで1.5時間から3時間．
• 期末レポート （第6回ハンドアウトで指定）

不正行為には厳正に対処します．(たとえば法学部ならば一発退学) 「不正行為」の定義について，小林直樹先生のページから抜粋:

レポートは，自分で考えたこと，調べたことを，自分の言葉でまとめること．レポートをまとめるにあたって，参考にした文献があれば，レポート中の各個所について参考文献へのレファレンスを挿入するとともに，レポートの最後に参考文献リストをつけること．また，文献の一部をそのまま引用する場合には，引用部分を明確にするために引用符とレファレンスをつけること（レポートの最後に参考文献として載せるだけでは不十分）．参考文献から図や写真，プログラム等を引用する場合も同様．

以上が守られない場合には，提出されたレポートは盗作と判断され，深刻な結果に至る可能性があります．

なお，何をもって盗作と判断されるかを知る上で，例えばインディアナ大学のこちらのページ に目を通すことをお勧めします．理解を確認するためのクイズを解くことができます．

スケジュール

• 2015.4.6 (Mon) オートマトン的モデル検査のイントロ．Buechi オートマトンと，その受理言語を定義しました．クイズ： Buechi オートマトンの emptiness check のアルゴリズムとは？
  次回は Vardi の教科書を最初からやります．有限語のオートマトンの復習は 形式言語理論のウェブページを参考にしてください．
  講義の後半，14:00 以降は演習IIIの説明会（小林研・蓮尾研）でした． ハンドアウト レポート解答
• 2015.4.13 (Mon) 蓮尾出張のため休講．
• 2015.4.20 (Mon) Vardi, Proposition 6 のアイデアまで（比較的ゆっくり）やりました． 配布ハンドアウトのレポート課題，2番はキャンセルです． ハンドアウト レポート解答
• 2015.4.27 (Mon) Vardi, Section 2.4 まで．次回は Demri & Gastin の最初から． ハンドアウト （講義中にレポート課題を追加しました．この pdf は改訂済みのもの） レポート解答
• 2015.5.11 (Mon) Demri & Gastion の Section 1.3.2 まで．それと，alternation のイントロ．次回は Vardi の Section 2.5 からやります． ハンドアウト レポート解答
• 2015.5.18 (Mon) Vardi の LTL formula から ABA への翻訳を定義しました．次回はその correctness proof から． ハンドアウト レポート解答
• 2015.5.25 (Mon) 理学部交歓会のため，午後は講義なし
• 2015.6.1 (Mon) 蓮尾担当分最終回． ハンドアウト レポート解答
• 2015.6.8 (Mon) この回以降小林先生ご担当．
• 2015.6.15 (Mon)
• 2015.6.22 (Mon)
• 2015.6.29 (Mon)
• 2015.7.6 (Mon)
• 2015.7.13 (Mon)