PRISM モデルチェッカー

PRISMは確率モデルチェッカーであり、確率的な動作を示すシステムのモデリングと分析のための形式検証ソフトウェアツールです。 ^[1] PRISMはパーカーの博士研究の一環として2002年頃に導入され、現在も活発に開発が進められています（2024年現在）。

このようなシステムの原因の1つは、BluetoothやFireWireなどの通信プロトコル、またはCrowdsやOnionルーティングなどのセキュリティプロトコルにおけるランダム化の使用です。確率的動作は、機器の故障、信頼性の低いセンサーやアクチュエータ、予測できない通信遅延などにより、他の多くのコンピュータシステムでも発生します。PRISMは、ロボット計画からコンピュータネットワークのパフォーマンス分析、生化学反応ネットワークまで、さまざまなアプリケーションの分析に使用されています。^[2]

PRISMは、離散時間マルコフ連鎖、連続時間マルコフ連鎖、マルコフ決定過程、時間オートマトン形式の確率的拡張など、さまざまな種類の確率モデルを分析するために使用できます。また、部分観測可能性と認識論的不確実性の概念を備えた確率モデルもサポートしています。これらのモデルに対して検証されるプロパティは、 PCTLなどの時相論理の確率的拡張で表現されます。PRISMの関連ツールであるPRISM-games ^[3]は、確率的ゲームの分析を提供します。

PRISMの開発はオックスフォード大学が主導しています。このプロジェクトはもともとバーミンガム大学で始まりました。このツールはオープンソースソフトウェアであり、 GNU General Public Licenseの下でリリースされています。PRISMは2013年と2014年にGoogle Summer of Codeプログラムに選ばれました。このツールとその開発者は、2024 ETAPS Test-of-Time Tool AwardやHVC 2016 Awardなど、いくつかの賞を受賞しています。

PRISM 確率モデル チェッカーは、PRISM 確率論理プログラミング システム (1990 年代後半に Sato 氏と共同研究者によって導入された PRogramming In Statistical Modelling) とは無関係のようです。

• PRISMウェブサイト
• PRISMゲームウェブサイト
• GitHub 上の PRISM