ハイブリッド・セル・オートマトンを用いた生物系と化学系の解析と検証

2002 年度 実績報告書

• 研究課題/領域番号: 14658088
• 研究機関: 東京大学
• 研究代表者: 萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
• キーワード: セル・オートマトン / ハイブリッド・システム / 分子コンピューティング / システム生物学 / グラフ書き換え / 様相論理 / 多重集合書き換え

研究概要

本年度は、ハイブリッド・セル・オートマトンの定式化に関する検討を進めた。その結果、セルをノード、セル間の隣接関係をエッジとするグラフに対する書き換え系としてセル・オートマトンを定式化することにより、グラフ書き換え系の枠組が利用できることを認識した。グラフを状態とする状態遷移系であるグラフ書き換え系は、ペトリネットや多重集合書き換え系の自然な発展となっており、セルの動的な生成や消滅、セルのトポロジーの動的な変化にも対応できる。
さらに、グラフ書き換え系の検証を行うため、様相μ計算を基に、時相と空相の二種類の様相を持つ様相論理を提案した。空相はグラフの結合関係、時相はグラフの時間変化を表現する。様相論理式によってグラフ書き換え規則を形式化し、書き換え系の性質を検証するための推論規則を与えた。最後に、グラフの表現に関して様相論理の本質的な限界について検討し、様相論理の表現力を高めるために状態量化を導入することを提案した。
次年度においては、グラフ書き換え系に連続変数を付加したハイブリッド・グラフ書き換え系の定式化を行う計画である。
一方、ハイブリッド系(ハイブリッド・システム)としては、時間付き多重集合書き換え系(TMSRS)に関する研究を引き続き行った。これまでに、TMSRSに対する到達可能性・有界性・被覆性の決定可能性について、以下が成り立つことを示した。「不変制約を含むTMSRSについて、到達可能性・有界性・被覆性はいずれも決定不能。また、不変制約を含まないTMSRSについて、到達可能性は決定不能。有界性・被覆性はいずれも決定可能。」さらに、「不変制約に出現するクロック変数の多重度が書き換えにおいて有界な場合は、有界性・被覆性がいずれも決定可能となる」ことを示した。これにより、時間オートマトンにおける到達可能性の決定可能性を導くことができる。

研究成果

• [文献書誌] Mitsuharu Yamamoto, Jean-Marie Cottin, Masami Hagiya: "Decidability of Safety Properties of Timed Multiset Rewriting"FTRTFT'02, Formal Techniques in Real-Time and Fault Tolerant Systems, 7th International Symposium, FTRTFT 2002. LNCS Vol.2469. 165-183 (2002)
• [文献書誌] 萩谷昌己: "グラフ書き換えと時空間様相論理"情報処理学会プログラミング研究会. (2003)
• [文献書誌] Masami Hagiya, et al.: "Verification of Authentication Protocols Based on the Binding Relation"Software Security -Theories and Systems. LNCS Vol.2609. (2003)
• [文献書誌] Masami Hagiya, Azuma Ohichi: "DNA Computing, 8th International Meeting on DNA-Based Computers, DNA8, Sapporo, Japan, June 2002, Revised Papers, LNCS Vol.2568"Springer. 338 (2003)