| 研究概要 |
本年度は、前年度の成果を発展させて、以下の研究を行った。
(1)ハイブリッドシステムのサブセットとして面白いモデルである、確率時間オートマトンがある。我々は、確率時間オートマトンと確率時間時相論理との関係や演繹的な検証手法を開発した。これにより、確率時間時相論理式が確率時間オートマトンの双模倣関係により、保存されることを明らかにした。さらに、確率時間オートマトンを一般化したモデル上に、確率時間時相論理の演繹的証明系を構築した。それらの成果を論文誌や国際会議で発表した。
(山根智:離散確率分布を持つリアルタイムシステムの確率時間双模倣関係と確率時間時相論理式の保存",情報処理学会論文誌,Vol.45,No.5,pp.1367-1375,2004.
山根智:"離散確率分布を持つリアルタイムシステムの確率時間時相論理式の演繹的検証手法",情報処理学会論文誌,Vol.45,No.6,pp.1652-1662,2004)
(2)ハイブリッドシステムを確率で拡張したモデル及び非線形な微分方式で拡張したモデルに対して、記号的検証手法や近似的な検証手法を開発した。これらのシステムを実装して、実用性を実証した。現在、研究会で報告しており、国際会議へ投稿中であり、論文誌への投稿を準備している。微分方程式の解析に検証コストを要するので、大規模システムの検証は困難であった。今度はより強力な抽象化技術の開発が望まれる。
(陸田陽介、山根 智:"確率線形ハイブリッドオートマトンの記号的到達可能性解析手法"、電子情報通信学会研究報告CAS2004,pp.7-12,2004
山崎貴史、山根 智:"非線形ハイブリッドオートマトンの近似解析による到達可能性解析検証手法"、電子情報通信学会研究報告CAS2004,pp.13-17,2004)
|
