「リアクティブシステムの仕様検証」の枠組みを用いて、線形時相論理により遺伝子ネットワークの振る舞いをモデル化し、与えられた生物学的性質を満たすかどうかを検証する枠組みの拡張について研究を行った。この手法では可能な振る舞い集合の中に、特定の性質を満たす振る舞いが存在するか、あるいはすべての振る舞いが特定の性質を満たすか、といった性質が検証可能である。一方で、環境からの生体システムへの入力については、システム自身がコントロールすることができるという前提のもとにモデル化されており、外部入力の扱いが十分になされているとは言い難かった。また、遺伝子発現のプロセスにおいても、単純な一遺伝子一タンパク質の考え方に基づいていた。そこで本課題では、これらの複雑な仕組みに対応できるよう本手法を適切に拡張することを目的としている。
今年度においては、一遺伝子から様々なタンパク質が産生される仕組みである選択的スプライシングという現象について、我々の時間論理による遺伝子ネットワークの振る舞いのモデル化手法でその現象を記述し解析する枠組みを開発した。この枠組みをDrosophila melanogasterの性決定ネットワークの解析に適用し、遺伝子Sxl初期プロモータのレベルの高低により、ネットワークが性特有のスプライシングパターンに固定されることを形式的に検証することに成功した。
|