確率システムの安全仕様の合成

本論文では、確率的環境においてエージェントが安全仕様を満たすことの重要性に着目し、従来の手法の制限を乗り越える新たなアプローチを提案しています。既存の方法では、安全な時間的仕様を確率回避制約に制限しているため、より表現力豊かな方法が求められています。この研究では、確率計算木論理（PCTL）を用いて、安全なPCTL仕様の合成に関する理論的枠組みを開発し、CPCTLという新たなフラグメントを定義しました。また、これに基づいてより一般的な時間的特性に対処するための新しい価値反復アルゴリズムを提案し、その健全性と完全性を証明しています。これにより、確率システムにおける安全性をより包括的に表現できるようになります。