◇	担当教員：関　浩之（せき　ひろゆき）
◇	単位数：２ ◇選択･必修：選択 ◇開講時期：�V期 月曜1限、木曜２限 ◇講義室：L2

◇ 授業目的：
コンピュータの能力の本質をさぐるための種々の計算モデルを紹介する。この分野の話題は多いが、
信頼性の高いソフトウェア設計検証技術の基礎を学ぶことも念頭に置き、以下の内容に話題を絞っ
て講義を行う。

◇ 授業内容：
まず、最も基本的なモデルである有限状態系に着目し、モデル検査法について説明する。モデル検
査法は与えられたシステムの振舞いを自動解析する手法であり、いくつかの優れた検証ツールが開
発されている。ここではその原理を説明する。
次に、より能力の高い無限状態系について、「コンピュータで問題を解くときの、問題の難しさを
はかる尺度はあるのだろうか」という観点から、重要な考え方であるNP完全性などについて説明す
る。現代暗号との関連についても触れる。
また、無限状態系において、データを系列から木構造に拡張することにより得られるモデルである
項書換え系について説明する。また、最近注目されているXMLのスキーマモデルである木オートマ
トンについても紹介する。
授業は以下の予定に沿って進める。

１．有限状態系のモデル検査法
システムモデル（Kripke構造）、時相論理、モデル検査法。
２．無限状態系における計算量理論
NP完全性の定義、Cookの定理、還元による証明法、クラスco-NPとPSPACE、
ランダム計算モデル。
３．項型計算モデル
項書換え系、合流性、停止性、書換え戦略、木オートマトンと正則保存性。

◇	教科書　：
教科書は指定しない。内容をまとめた資料を配布する。
◇	参考書　：
授業中に紹介する。
◇ 履修条件：
アルゴリズムとデータ構造（アルゴリズム概論）、有限オートマトンとチューリング機械（計算理論I）、
命題論理 （人工知能基礎論）についての基礎知識があることが望ましい。希望があれば、授業期間中に
チューリング機械に関する補講を行う。
◇ 成績評価：
試験（70〜80％）および 課題レポート（20〜30％）により評価する。
◇ オフィスアワー：
（B501）月曜５限・金曜５限。変更等はWWWの授業ページ参照。