| 研究課題/領域番号 |
22300005
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
住井 英二郎 東北大学, 情報科学研究科, 准教授 (00333550)
|
|---|
| 研究期間 (年度) |
2010-04-01 – 2015-03-31
|
| キーワード | 環境双模倣 / 高階プログラム等価性証明 / 並行・分散プロセス計算 / プログラム意味論 / プログラム理論 |
|---|
| 研究概要 |
理論計算機科学のトップコンファレンスの一つであるLogic in Computer Science（ACM・IEEE共催）において、名前制限ではなく名前生成を備えた分散計算における環境双模倣に関する査読つきフルペーパー（仏からの大学院博士後期課程留学生との共著）が採録・発表された。当該論文では、Milnerのπ計算など標準的な並行プロセス計算では等価であると考えられてきた名前制限と名前生成が、passivation（計算ないし計算機の移動・失敗・複製等を抽象化・定式化した概念）のある分散プロセス計算の下では一致しないことを示すとともに、住井らの環境双模倣に基づき、名前生成を持つ分散プロセス計算における健全かつ完全なプロセス等価性証明手法を初めて与えた。また、素朴には等価であるかのように思われるが、passivationの下では双模倣的にならないプロセスの組の例をいくつか挙げ、失敗・複製のありうる分散計算におけるプロセス等価性の難しさを示した。そのようなプロセスに対する等価性として双模倣は細かすぎる(too fine)と考え、より荒い（coarseな）mayかつmust検査等価性(testing equivalence)に基づく考察も行った。これらは並行・分散計算の理論への自明でない貢献であり、並行・分散システムをはじめとする情報システムの信頼性・安全性を向上させる数理論理学的アプローチ（形式手法）につながる成果である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
「研究実績の概要」の通り、高い学術的成果を挙げている。
|
| 今後の研究の推進方策 |
引き続き、研究計画の通り、環境双模倣理論の対象言語の拡大および実用的アルゴリズムの開発を目指す。
|
