コンピュータサイエンスにおける様相論理

基本となる様相論理 K から始め,コンピュータサイエンス (計算機科学) において重要である,CTL (計算木論理) ,様相ミュー計算,PDL (命題動的論理) について,その数学的な基礎をわかりやすく,かつ厳密に説明する. また,様相論理ではないものの PDL との関係が深く,プログラム検証を行う際に活躍するホーア論理についても詳しく解説する. 各論理については,定義や基本的な定理はもちろん,証明が難解で省略されがちな「証明体系の完全性」「計算可能性」「様相ミュー計算のゲーム意味論の妥当性」の証明も掲載しており,本書一冊で基礎を徹底的に学ぶことができる. 第 1 章 準備:命題論理 第 2 章 K 第 3 章 CTL (計算木論理) 第 4 章 様相ミュー計算 第 5 章 PDL (命題動的論理) 第 6 章 ホーア論理