[Back to Teaching]
計算機言語論 (2014年度,前半・蓮尾担当分)
概要
- 夏学期 月曜3限 13:00 - 14:30
- 化学東館 236 号室
- 理学部情報科学科 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回ハンドアウトで指定)
不正行為には厳正に対処します.(たとえば法学部ならば一発退学)
「不正行為」の定義について,小林直樹先生のページから抜粋:
レポートは,自分で考えたこと,調べたことを,自分の言葉でまとめること.レポートをまとめるにあたって,参考にした文献があれば,レポート中の各個所について参考文献へのレファレンスを挿入するとともに,レポートの最後に参考文献リストをつけること.また,文献の一部をそのまま引用する場合には,引用部分を明確にするために引用符とレファレンスをつけること(レポートの最後に参考文献として載せるだけでは不十分).参考文献から図や写真,プログラム等を引用する場合も同様.
以上が守られない場合には,提出されたレポートは盗作と判断され,深刻な結果に至る可能性があります.
なお,何をもって盗作と判断されるかを知る上で,例えばインディアナ大学のこちらのページ に目を通すことをお勧めします.理解を確認するためのクイズを解くことができます.
スケジュール
- 2014.4.7 (Mon)
蓮尾・小林先生両方共海外出張のため休講.
- 2014.4.14 (Mon)
時相論理式モデル検査とωオートマトンのイントロダクションののち,Vardi の論文の冒頭(オートマトンの理論の復習).Section 2.1 の終わりまで.
ハンドアウト
レポート解答
- 2014.4.21
(Mon)
Vardi, Prop. 8 まで.
ハンドアウト
レポート解答
- 2014. 4.28 (Mon)
Vardi, Section 2.4 まで終わって,Demri & Gastin の LTL syntax まで解説した.
ハンドアウト
レポート解答
- 2014.5.12 (Mon)
Demri & Gastin, p.13 の第1段落まで.次は Fig. 1.3 から.
ハンドアウト
レポート解答
- 2014.5.19 (Mon)
理学部交歓会のため,午後は講義なし
- 2014.5.26 (Mon)
Demri & Gastin, LTL formula から Buechi automaton への翻訳をやった.
次回は Vardi で alternating automaton.
ハンドアウト
レポート解答
- 2014.6.2 (Mon)
Vardi の教科書で alternating automaton を解説ののち,LTL formula からの翻訳の概略を説明.
ハンドアウト
レポート解答
- 2014.6.9 (Mon)
この回以降小林先生ご担当.
- 2014.6.16 (Mon)
- 2014.6.23 (Mon)
- 2014.6.30 (Mon)
- 2014.7.7 (Mon)
- 2014.7.14 (Mon)
- 2014.7.18 (Mon)