内容説明
基本となる様相論理Kから始め，コンピュータサイエンス（計算機科学）において重要である，CTL（計算木論理），様相ミュー計算，PDL（命題動的論理）について，その数学的な基礎をわかりやすく，かつ厳密に説明する．
また，様相論理ではないもののPDLとの関係が深く，プログラム検証を行う際に活躍するホーア論理についても詳しく解説する．
各論理については，定義や基本的な定理はもちろん，証明が難解で省略されがちな「証明体系の完全性」「計算可能性」「様相ミュー計算のゲーム意味論の妥当性」の証明も掲載しており，本書一冊で基礎を徹底的に学ぶことができる．
目次
第1章 準備：命題論理
第2章 K
第3章 CTL（計算木論理）
第4章 様相ミュー計算
第5章 PDL（命題動的論理）
第6章 ホーア論理
感想・レビュー
※以下の感想・レビューは、株式会社ブックウォーカーの提供する「読書メーター」によるものです。
Q
0
命題論理を復習した後、様相論理を簡潔に説明し、最後にホーア論理に導く本。ほぼ数式だけで解説がなされるので、自分のような数式アレルギーには厳しい。自分にとっては理論よりもモデル検査で検査を体験した方が理解が進むと感じた。TLA+はその意味では素晴しいツールだった。2022/03/10
