このページは 2012 年度のソフトウェアモデル論(A1)のページです。
講義スライド(第15回)を載せました。(2013/01/18)
レポートその13を載せました。(2013/01/11)
講義スライド(第14回)を載せました。(2013/01/11)
演習問題を載せました。(2013/01/09)
開講しました。(2012/09/28)
| 担当： | 桑原 寛明 (情報システム学科) |
| 連絡先： | kuwabara @ cs.ritsumei.ac.jp ，クリエーションコア 2F 共同研究室 1 |
| 時間： | 金曜 5,6 時限 (13:00-14:30) |
| 教室： | F201 |
| 教科書： | 講義資料を配布 |
評価方法や講義内容、参考書についてはシラバスを参照してください。
講義直前にドラフト版を WebCT で公開します。 正式版は講義終了後に公開します。
| スライド | テキストの範囲 | 概要 | |||
| 第1回 | (2012/09/28) | 2 章 | 導入、数学的準備 | レポートその1 | |
| 第2回 | (2012/10/05) | 3.1, 3.2, 3.3 節 | 有限オートマトン(DFA, NFA) | レポートその2 | |
| 第3回 | (2012/10/12) | 3.4, 3.5 節 | DFA と NFA の等価性、正規表現 | レポートその3 | |
| 第4回 | (2012/10/19) | 3.6 節 | 正規表現から NFA への変換 | レポートその4 | |
| 第5回 | (2012/10/26) | 3.7, 3.8 節 | DFA から正規表現への変換、反復補題 | レポートその5 | |
| 第6回 | (2012/11/02) | 別紙 2.1 節 | チューリング機械、計算 | レポートその6 | |
| 第7回 | (2012/11/09) | 別紙 2.2 節 | チューリング機械のコード化 | レポートその7 | |
| 第8回 | (2012/11/16) | 別紙 2.4 節 | 万能チューリング機械、計算可能性、停止性判定 | レポートその8 | |
| 第9回 | (2012/11/23) | 5.1, 5.2, 5.3, 5.4 節 | 命題、論理式、論理的帰結 | レポートその9 | |
| 第10回 | (2012/11/30) | 5.5, 5.6 節 | 証明系、自然演繹 | レポートその10 | |
| 第11回 | (2012/12/07) | 5.7, 5.8 節 | 自然演繹の健全性、完全性 | レポートその11 | |
| 第12回 | (2012/12/21) | 6.1, 6.2 節 | モデル検査、Kripke 構造 | レポートなし | |
| 第13回 | (2012/12/22) | 6.3.1 節 | CTL | レポートその12 | |
| 第14回 | (2013/01/11) | 6.4 節 | モデル検査アルゴリズム | レポートその13 | |
| 第15回 | (2012/01/18) | 6.6, 6.7 節 | 並行プログラムのモデル検査 | レポートなし |
締切を過ぎたレポートの略解を順次 WebCT に掲載します。 必要に応じて参照してください。 別解もありえるのでもし疑問があれば訊いてください。
Copyright(C) since 2012
KUWABARA Hiroaki.
All rights reserved.