| 研究課題/領域番号 |
18500003
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
萩谷 昌己 東京大学, 大学院・ 情報理工学系研究科, 教授 (30156252)
|
|---|
| 研究分担者 |
高橋 孝一 (独)産業技術総合研究所, システム検証センター, 副研究センター長 (40357372)
|
|---|
| 研究期間 (年度) |
2006 – 2007
|
| 研究課題ステータス |
完了 (2007年度)
|
| 配分額 *注記 |
3,980千円 (直接経費: 3,500千円、間接経費: 480千円)
2007年度: 2,080千円 (直接経費: 1,600千円、間接経費: 480千円)
2006年度: 1,900千円 (直接経費: 1,900千円)
|
|---|
| キーワード | シェイプ解析 / 静的解析 / 停止性解析 / モデル検査 / 様相論理 |
|---|
| 研究概要 |
グラフ変換の過程を解析するために、ノードの抽象化に基づいてグラフをマルチセットによって近似し、個々の抽象ノードに対応する具体ノードの数が、グラフ変換の各操作により、どのように変化するか(増減するか)を解析するcardinality analysisに関する研究を行った。まず最初に、様相論理式とグラフの変換操作に対する最弱前条件を定式化し、論理式を満たすノードの数が操作の実行によって減少するための十分条件を与えることにより、リスト処理を行う具体的なプログラムの停止性を示した。次に、cardinality analysisを一般化するために、自然数の全体に無限大を追加したmin-plus代数上で様相論理式を解釈する意味論について研究を行った。この意味論のもとでは、論理式を満たすノードの数は、大域的様相を含むある様相論理式の解釈として表すことができる。この意味論を用いると、論理式を満たすノードの数だけでなく、たとえばノードからノードへの最短経路の長さなど、様々な数値的な尺度を様相論理式によって表現できる。この意味論の有用性を示すために、min-plus代数上の様相μ計算のモデル検査アルゴリズムを考案し実装した。そして、操作を実行する前の最弱前条件の解釈と実行後の論理式の解釈がmin-plus上で等しくなるように、論理式と操作の最弱前条件を再定義し、最弱前条件の解釈が論理式の解釈より小さくなるための十分条件を定式化した。min-plus代数は整礎であるので、この方法を用いて、cardinalityだけでなく、様々な尺度による停止性解析および活性解析が可能となった。以上に加えて、停止性解析および活性解析の一般的な手法である遷移述語抽象化の効率化と高精度化を行った。また、グラフ構造とその変換操作の表現力を向上させるために、階層的な様相論理の定式化を行った。
|
