述語抽象化とその洗練による確率時間オートマトンの到達可能性解析手法

摘要

本論文では，まず確率時間オートマトンについて定義を行う．そして，その上での効率的な安全性検証手法を提案する．提案手法により，組込システムのようなリアルタイム動作，確率動作を持つシステムに対する，効率的な自動検証が可能となる．検証の効率化には，述語抽象化とその洗練による手法を用いる．