研究課題
基盤研究(C)
グラフ変換の過程を解析するために、ノードの抽象化に基づいてグラフをマルチセットによって近似し、個々の抽象ノードに対応する具体ノードの数が、グラフ変換の各操作により、どのように変化するか(増減するか)を解析するcardinality analysisに関する研究を行った。まず最初に、様相論理式とグラフの変換操作に対する最弱前条件を定式化し、論理式を満たすノードの数が操作の実行によって減少するための十分条件を与えることにより、リスト処理を行う具体的なプログラムの停止性を示した。次に、cardinality analysisを一般化するために、自然数の全体に無限大を追加したmin-plus代数上で様相論理式を解釈する意味論について研究を行った。この意味論のもとでは、論理式を満たすノードの数は、大域的様相を含むある様相論理式の解釈として表すことができる。この意味論を用いると、論理式を満たすノードの数だけでなく、たとえばノードからノードへの最短経路の長さなど、様々な数値的な尺度を様相論理式によって表現できる。この意味論の有用性を示すために、min-plus代数上の様相μ計算のモデル検査アルゴリズムを考案し実装した。そして、操作を実行する前の最弱前条件の解釈と実行後の論理式の解釈がmin-plus上で等しくなるように、論理式と操作の最弱前条件を再定義し、最弱前条件の解釈が論理式の解釈より小さくなるための十分条件を定式化した。min-plus代数は整礎であるので、この方法を用いて、cardinalityだけでなく、様々な尺度による停止性解析および活性解析が可能となった。以上に加えて、停止性解析および活性解析の一般的な手法である遷移述語抽象化の効率化と高精度化を行った。また、グラフ構造とその変換操作の表現力を向上させるために、階層的な様相論理の定式化を行った。
すべて 2008 2007 2006 2005
すべて 雑誌論文 (24件) (うち査読あり 16件) 学会発表 (6件)
PPL2008, JSSST 1
ページ: 216-230
The Tenth Workshop on Programming and Programming Languages(PPL 2008), Japanese Society on Software Science and Technology
IPSJ Transactions on Programming Vol.48,No.SIG10
ページ: 114-137
日本応用数理学会論文誌 Vol.17,No.4
ページ: 559-576
応用数理 Vol.17,No.4
ページ: 8-15
IPSJ Transactions on Programming Vol.48, No.SIG 10(PRO 33)
Also in IPSJ Digital Courier Vol.3
ページ: 380-4〓
電子情報通信学会論文誌 D-I Vol.j89-D,No.4
ページ: 642-650
コンピュータソフトウェア Vol.23,No.3
ページ: 147-157
情報処理学会論文誌 Vol.47,No.4
ページ: 1118-1126
日本ソフトウェア科学会第23回大会 1
ページ: 4-31-7
ページ: 5-31-10
ページ: 3-21-7
ページ: 1-2
第三回システム検証の科学技術シンポジウム 1
ページ: 27-28
日本応用数理学会2006年度年会講演予稿集 1
ページ: 8-11
Computer Software Vol.23, No.3
JSSST 2006, Lecture Notes 5C-3
ページ: 1-10
TABLEAUX 2005, Lecture Notes in Artificial Intelligence Vol.3702
ページ: 277-291
日本ソフトウェア科学会第22回大会 1
ページ: 5-21-5
コンピュータソフトウェア Vol.22,No.3
ページ: 154-166
JSSST 2005, Lecture Notes 5A-3
ページ: 1-5
Computer Software Vol.22, No.3
