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

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

『コンピュータサイエンスにおける様相論理』 (鹿島 亮 著、森北出版、2022 年 1 月刊) は、コンピュータサイエンスで使われる様相論理の数学的な基礎を説明した専門書です。版元の紹介文は、基本となる様相論理 K から始めて、CTL (計算木論理)、様相ミュー計算、PDL (命題動的論理) をわかりやすく、かつ厳密に説明し、様相論理ではないものの PDL と関係が深く、プログラム検証で使われるホーア論理も詳しく解説すると案内しています。刊行時の著者紹介によれば、鹿島 亮は東京工業大学准教授で、学位は博士 (理学) です。

第 1 章「準備: 命題論理」から第 6 章「ホーア論理」までの全 6 章

目次は第 1 章「準備: 命題論理」、第 2 章「K」、第 3 章「CTL (計算木論理)」、第 4 章「様相ミュー計算」、第 5 章「PDL (命題動的論理)」、第 6 章「ホーア論理」の全 6 章です。紹介文によれば、各論理について定義と基本的な定理に加えて、証明が難しく省略されることの多い「証明体系の完全性」「計算可能性」「様相ミュー計算のゲーム意味論の妥当性」の証明も掲載しています。国立国会図書館の書誌には、文献と索引があることが記されています。

可能世界の意味論と、CTL、様相ミュー計算

様相論理は、命題論理に、必ず成り立つ、成り立つ可能性がある、といった様相を表す演算子を加えた論理です。意味論ではふつう、状態 (可能世界) の集まりと、ある状態から別の状態へ移れるという関係を組にした構造を考え、必然をすべての移り先で成り立つこと、可能をどこかの移り先で成り立つことと読みます。K は、この読み方のもとで常に正しい式だけを集めた最も基本的な様相論理です。状態と移り先の関係を、プログラムやシステムの状態の遷移と見なすと、コンピュータサイエンスとの接点が生まれます。CTL は、ある状態から先に分かれていく実行の道筋について、すべての道筋についてか、ある道筋についてかの区別と、次の状態で、いつか、ずっと、という時間の言い方を組み合わせて性質を書く時相論理で、システムが仕様を満たすかを機械的に調べるモデル検査で使われてきました。様相ミュー計算は、最小不動点と最大不動点の演算子によっていつか成り立つ、ずっと成り立つ、のような繰り返しを含む性質を表す論理で、CTL の式もこの形に書き直せます。

PDL とホーア論理、プログラムの正しさを論理で書く

PDL は、プログラムそのものを様相の演算子の中に書き込み、このプログラムを実行して停止したあとには必ずある性質が成り立つ、といった主張を論理式として扱う体系です。ホーア論理は、実行前の条件、プログラム、実行後の条件の 3 つ組で正しさを述べ、代入や繰り返しなどの構文ごとの規則から証明を組み立てます。PDL の式は、ホーア論理の 3 つ組と同じ内容を表すことができます。紹介文も、ホーア論理を PDL と関係が深い論理として紹介しています。証明体系の完全性は、意味論の上で正しい式がすべて証明体系の中で証明できるという性質で、計算可能性は、ある式が正しいかどうかを機械的に判定できるかを問うものです。

本書は様相論理 K から CTL、様相ミュー計算、PDL、ホーア論理までを、第 1 章「準備: 命題論理」から第 6 章「ホーア論理」までの全 6 章に収めています。