コンピュータサイエンスにおける様相論理(コンピュータサイエンスニオケルヨウソウロンリ)

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

モデル検査やプログラム検証のツールを使っていると、 CTL や不動点といった言葉の背後に広がる理論の存在を感じる瞬間があります。その理論体系を正面から学ぶための日本語の専門書が本書です。著者は鹿島亮氏、 2022 年に森北出版から刊行されました。基本となる様相論理 K から出発し、コンピュータサイエンスで重要な CTL (計算木論理) 、様相ミュー計算、 PDL (命題動的論理) へと進み、さらに PDL と関係が深くプログラム検証で活躍するホーア論理までを一冊で扱います。

際立っているのは証明への態度です。各論理について定義と基本定理を示すだけでなく、多くの教科書で難解さゆえに省略されがちな証明体系の完全性、計算可能性、そして様相ミュー計算に対するゲーム意味論の妥当性といった結果の証明まで掲載しており、「わかりやすく、かつ厳密に」という方針が細部まで貫かれています。天下り的に結果を受け入れるのではなく、理論の土台を自分の手で確かめたい読者のための本といえます。

第 1 章に命題論理の準備が置かれているため、出発点はそこまで高くありませんが、数学的な証明を続けて読む体力は必須で、水準としては情報系の学部上級から大学院に相当します。形式検証を研究テーマにする学生、検証ツールの理論的裏付けを求めるエンジニア、論理学からコンピュータサイエンスへ越境したい数学系の読者が、それぞれの目的で深く潜れる一冊です。