2010 Fiscal Year Annual Research Report
| Project/Area Number |
22300005
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 東北大学, 大学院・情報科学研究科, 准教授 (00333550)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
寺内 多智弘 東北大学, 大学院・情報科学研究科, 助教 (70447150)
|
|---|
| Keywords | プログラム理論 / 環境双模倣 / プロセス計算 / 並行分散システム / 形式的手法 |
|---|
| Research Abstract |
位置(location)の概念があり、かつ、実行中のプログラムを送受信することができる「高階分散プロセス計算」(higher-order distributed process calculus)において、システムの様々な性質の基礎となるプロセス等価性(process equivalence)を検証する「環境双模倣」(environmental bisimulation)の理論を構築した。より具体的には、実行中のプロセスを停止し値として扱う、「受動化」(passivation)と呼ばれる抽象的操作により拡張された「高階π計算」(higher-order pi-calculus)を対象に環境双模倣を定義し、その健全性(soundness)を数理論理学的に証明した。ただし、証明する過程において、「観察者の知識を表す環境(environment)に含まれるプロセスは、名前制限(name restriction)やプロセス受信(process input)を行うことができない」という条件を課す必要が生じた。この成果をETAPS2011(ソフトウェアの理論と実践に関する欧州合同会議)中のFoSSaCS 2011(ソフトウェア科学と計算構造の基礎に関する第14回国際会議)に投稿、査読(全投稿論文100本中30本採択)を経て発表した。また、仏INRIA(国立情報学自動制御研究所)ローヌ・アルプ拠点においても同研究に関する発表・議論を行った。
|
