2006 Fiscal Year Annual Research Report
| Project/Area Number |
18500003
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
高橋 孝一 (独)産業技術総合研究所, システム検証センター, 副研究センター長 (40357372)
|
|---|
| Keywords | シェイプ解析 / 静的解析 / 停止性解析 / モデル検査 / 様相論理 |
|---|
| Research Abstract |
cardinality analysisに関しては、様相論理式・とグラフの変換操作・(x:=y,x:=y.f,x.f:=yのいずれかの形)に対して、局所的最弱前条件(local weakest precondition)wp(・,・)の定式化を行った。この定式化を用いて、論理式・を満たすノードの数が減少するための十分条件を与えた。すなわち、様相論理式[o](wp(・,・)・・)および・o・(wp(・,・・)・・)が成り立つとき、・を満たすノードの数が真に減少する。この十分条件を用いて、リスト処理を行う具体的なプログラムの停止性を示した。
また、グラフ構造とその変換操作の表現力を向上させるために、階層的な様相論理の定式化を行った。この様相論理の枠組のもとでは、階層的なグラフ構造(グラフの中にグラフを入れ子として含むことのできる構造)とその変換操作を自然に表現することができる。各変換操作に対する最弱前条件の定式化も行った。
停止性解析および活性解析に関しては、遷移述語抽象化に対する既存手法の効率化と高精度化を、その実装も含めて行った。効率化に関しては、遷移述語をノードとする有向グラフを強連結成分に分解し、内側の強連結成分から順に解析を行うことにより、全体の解析の効率を大幅に向上させることができた。
以上に加えて、cardinality analysisを一般化するため、様相論理式をmin-plus代数を用いて解釈する方法を着想し、次年度の主たる研究テーマとする計画を立てた。この解釈のもとでは、様相論理式を満たすノードの数だけでなく、たとえばノードからノードへの最短経路の長さなども様相論理式によって表現できるため、cardinalityだけでなく、さまざまな尺度による停止性解析および活性解析が可能になる。
|
Research Products
(10 results)
