空間の概念を持つコスト付き確率時間オートマトンの記号的検証手法

摘要

近年，無線センサネットワークがさまざまな分野において注目を集めている．また，組込みシステムの高機能化に伴い，それらのシステムに対する検証手法の需要が高まっている．本研究では，空間の概念を持つコスト付き確率時間オートマトン（SP~2TA）を用いて，無線センサネットワークをモデル化し，SP~2TAにおける到達可能性解析手法を開発する．