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