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

2003 Fiscal Year Annual Research Report

• Project/Area Number: 14658088
• Research Institution: The University of Tokyo
• Principal Investigator: 萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
• Keywords: セル・オートマトン / ハイブリッド・システム / 分子コンピューティング / システム生物学 / グラフ書き換え / 様相論理 / 多重集合書き換え

Research Abstract

昨年度より、時相論理を用いてグラフ書き換え系の解析を行う方法について考察している。本年度はその簡単な場合として、グラフの構造が変化せず、各々のノードの状態だけが変化するシステムを、時相論理を用いて解析する方法を定式化した。このようなシステムには、いわゆるセル・オートマトンも含まれる。
我々は従来研究において、時相論理を用いて、互いにポインタで繋がれたセルから成るリンク構造を抽象化する方法を提案した。セルはあらかじめ指定された時相論理式の真偽の組み合わせを表す抽象セルによって抽象化され、リンク構造全体は抽象セルの集合によって抽象化される。
本年度は、従来の方法を発展させ、時相論理を用いてセル・オートマトンを解析する方法を定式化した。従来研究の場合と違って、すべてのセルが同期して状態を遷移させるので、各抽象セルの次状態を計算することにより、抽象化されたリンク構造の次状態が求まる。この新しい状態を再び抽象化するために、抽象セルの分裂と融合の操作を導入した。以上の方法により、実際に一次元(および二次元)のセル・オートマトンの簡単なものを解析することができた。
また、本研究では、本方法のベースとなっている時相論理である2方向CTL(computation tree logic)とその充足可能性判定方法の定式化も行った。これは、CTLに対するタブロー法を拡張し、2方向の様相に対処できるようにしたものである。ただし、素朴な実現方法を用いると速やかに指数爆発が起きてしまうので、BDD(binary decision diagram)を用いた実装方法について考察した。

Research Products

• [Publications] 萩谷昌己, 高橋孝一, 山本光晴, 佐藤貴洋: "時相論理による抽象化を用いたセル・オートマトンの解析"日本ソフトウェア科学会第20回大会. (2003)
• [Publications] Masami Hagiya, et al.: "Analysis of Synchronous and Asynchronous Cellular Automata using Abstraction by Temporal Logic"FLOPS2004:The Seventh Functional and Logic Programming Symposium, Lecture Notes in Computer Science. 2998. 7-21 (2004)
• [Publications] Akihiko Tozawa, Masami Hagiya: "XML Schema Containment Checking based on Semi-implicit Techniques"and Application of Automata, 8th International Conference, CIAA 2003, Lecture Notes in Computer Science. 2759. 213-225 (2003)