PAT (model checker) とは

PAT(Process Analysis Toolkit)は、リアルタイムのシステムとその他の可能なドメインを構成、シミュレート、推論するための自己完結型のフレームワークです。ユーザーフレンドリーなインターフェイス、特長のモデルエディタ、アニメーションシミュレータが付属しています。最も重要なことに、PATは、デッドロックフリーネス、ダイバージェンスフリーネス、到達可能性、公平性を前提としたLTLプロパティ、リファインメントチェック、確率モデルチェックなど、さまざまなプロパティを扱うさまざまなモデルチェック手法を実装しています。良好な性能を達成するために、高度な最適化技術がPATに実装されている。部分順序削減、対称性減少、プロセスカウンタ抽象化。現在までに、PATには41の国と地域の302の組織から1350人の登録ユーザーがいます。