| Project/Area Number |
14658088
|
|---|
| Research Category |
Grant-in-Aid for Exploratory Research
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
|
|---|
| Project Period (FY) |
2002 – 2006
|
| Project Status |
Completed (Fiscal Year 2004)
|
| Budget Amount *help |
¥2,300,000 (Direct Cost: ¥2,300,000)
Fiscal Year 2004: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2003: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2002: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | セル・オートマトン / ハイブリッド・システム / 分子コンピューティング / システム生物学 / グラフ書き換え / 様相理論 / 多重集合書き換え / 様相論理 |
|---|
| Research Abstract |
昨年度より、グラフ書き換え系、特にグラフの構造が変化せず、各々のノードの状態だけが変化するシステムを、時相論理を用いて解析する方法に関する研究を進めている。このようなシステムには、いわゆるセル・オートマトンも含まれる。昨年度は、時相論理を用いてセル・オートマトンを解析する方法を定式化し、実際に一次元のセル・オートマトンや分散アルゴリズムの解析を試みた。今年度は、以上の方法を発展させるために、以下の二つの方向の研究を進めた。
一つは、二次元のセル・オートマトンの解析を行うために、上下左右の4方向の様相を持つ時相論理である4CTL (computation tree logic)の定式化とその充足可能性判定方法を開発した。4CTLの充足可能性判定は決定不能であるため、Presburger算術を用いた近似的な判定方法を定式化した。そして、二次元のセル・オートマトンの例として、分子コンピューティングにおけるタイリングの解析を行った。
もう一つは、セル・オートマトンのハイブリッド化と、その解析方法に関する研究を行った。セル・オートマトンのハイブリッド化とは、各セルに時間とともに変化する連続パラメータを導入することを意味する。解析のための時相論理の方も、連続パラメータに対処するために拡張しなければならない。本研究では、時相論理を包含する論理として、ガード付きフラグメント(guarded fragment)とその充足可能性判定に関する研究を進めた。また、ハイブリッド化されたセル・オートマトンの例として、簡単なニューラル・ネットワークの解析を行った。
|
