平均利得時間論理とそれを用いた検証・最適化手法

摘要

ソフトウェアの形式検証では，イベント生起順序などの制約に関する定性的性質がしばしば注目されてきた．しかしながら，性能に関する定量的性質の検証だけでなく，定量的性能解析や最適化などの手法も求められている．本研究では，平均コストやイベント生起頻度に関する定量的性質を記述可能な平均利得式を導入することによって，LTLを拡張した平均利得線形時相論理LTL mp を提案する．また，その効率的なモデル検査，充足可能性判定，最適化手法を与える．