UPPAAL TIGA

UPPAAL TIGAはUPPAAL [BDL04]の拡張であり、それは到達可能性および安全性特性に関して時限ゲームオートマトンに基づいてゲームを解決するための第1の効率的なオンザフライアルゴリズムを実装しています。
長い間、時限ゲームが決定可能であることが知られているが、今までは、解析のための効率的かつ真にオンザフライアルゴリズムの欠如がありました。
UPPAAL TIGAは、対応するサーバーとユーザーフレンドリーなグラフィカルなインターフェイス、およびコマンドライン検証を提供します。
私たちは[CDFLL05]提案アルゴリズムは、有限状態システムの線形時間モデルチェックのために劉＆スモルカ[LS98]によって提案されたオンザフライアルゴリズムの象徴拡張したものです。オンザフライであり、象徴的なアルゴリズムは、全状態空間を探索したずっと前に終了することができます。
また、アルゴリズムの各ステップは、基礎となるデータ構造としていわゆるゾーンを使用することによって効率的に行われます。当社のツールは、さまざまな基本的な象徴的アルゴリズムの最適化、ならびに（到達可能性のゲームのための）時間最適入賞戦略を取得するためのメソッドを実装します。
このリリースの新機能：