Loading article…
『モデル検査の原理』は、コンピュータサイエンスの一分野であるモデル検査に関する教科書です。モデル検査とは、機械が仕様要件を満たしているかどうかを判定する問題を自動化するものです。本書はクリステル・バイアーとヨースト＝ピーター・カトエンによって執筆され、2008年にMIT Pressから出版されました。
序論と第1章では、モデル検査の分野について概説します。モデル検査とは、機械やプロセスのモデルを分析し、望ましい特性が成り立つかどうかを確認する手法です。例えば、自動販売機は「残高が0ユーロを下回ることは決してない」という特性を満たすかもしれません。ビデオゲームは「プレイヤーのライフが0になったらゲームオーバー」というルールを強制するかもしれません。自動販売機とビデオゲームはどちらも遷移システムとしてモデル化できます。モデル検査とは、こうした要件を数学的な言語で記述し、モデルが要件を満たしていることを証明したり、モデルに欠陥がある場合は反例を発見したりするプロセスです。
第2章では、並行システムに適したモデルの作成に焦点を当てます。並行システムでは、アルゴリズム（命令セット）の複数の部分が、異なるマシンまたはマシンの一部によって同時に実行されます。
第3章では、遷移システムが満たす可能性のあるルールの種類、すなわち線形時間特性について考察します。 「デッドロック状態は発生しない」などの安全性特性は、「望ましくない結果は決して発生しない」という形式をとります。 「共有リソースは、それを要求するコンポーネントに対して必ず最終的に利用可能になる」などの活性特性は、「望ましい結果が最終的に発生する」という形式をとります。「信号機の色は決して変化しなくなることはない」などの公平性特性は、前提条件、つまり他の特性を推論するための仮定として使用できます。
第4章では、正規言語とω正規言語の特性、およびそれらの言語をモデル化するブッチオートマトンなどの理論的な機械について解説します。また、特性を検証したり反例を見つけたりするためのモデル検査アルゴリズムも紹介します。
第5章と第6章では、特性を表現する2種類の論理式である線形時相論理（LTL）と計算木論理（CTL）について解説します。LTLは、「モノポリーのすべてのプレイヤーは『Go』を無限回通過する」など、システム内の経路に関する要件を符号化します。一方、CTLは、「どの位置からでも、すべてのプレイヤーは最終的に『Go』に到達できる」など、システム内の状態に関する要件を符号化します。また、これら2つの文法を組み合わせたCTL*論理式も定義します。さらに、これらの論理式をモデル検査するためのアルゴリズムも示します。
第7章では、双模倣などの遷移システムを比較する形式的な方法を探求します。第8章では、モデルの特性を検証するために必要な計算量を削減することを目的とした部分順序削減について解説します。第9章と第10章では、クロック速度（時間付きオートマトン）や確率（マルコフ連鎖に基づく確率的オートマトン）の追加など、これまで検討してきた論理体系とオートマトンへの拡張について解説します。
『コンピュータジャーナル』に寄稿したフランソワ・ラルーシニ氏は、この本を研究者、講師、学生、エンジニアに推薦し、「印象的」と評した。ラルーシニ氏は、この教科書は包括的で分かりやすく書かれており、重要な概念に関する多くの例、演習、動機付けとなるアイデアが含まれていると評価した。「統一されたフレームワーク」に基づき、最初の7章では古典的な理論を扱い、最後の3章ではモデル検査の拡張について解説している。[ 1 ]
ACM Computing Reviews誌で、ガブリエル・チオバヌ氏は、この教科書は上級学部生または大学院生向けのコースで使用でき、研究者にも役立つだろうと述べた。チオバヌ氏は「明快で直感的」な説明を称賛し、「モデル検査研究における基本概念、深い理論的結果、および高度なトピックを網羅する教育的アプローチが高く評価されるべきだ」と述べた。[ 2 ]
2014年、この本はBook Citation Index （BKCI）が監視する学術文献の中で最も引用された5冊のうちの1冊だった。[ 3 ]
{{citation}}: CS1 maint: 無題の定期刊行物 (リンク)