2009 Fiscal Year Final Research Report

Visual model checking approach of high level Petri-net and its application to dynamic biological pathway model

Research Project

Project/Area Number	20700265
Research Category	Grant-in-Aid for Young Scientists (B)
Allocation Type	Single-year Grants
Research Field	Bioinformatics/Life informatics
Research Institution	The University of Tokyo
Principal Investigator	NAGASAKI Masao The University of Tokyo, 医科学研究所, 助教 (90396862)
Project Period (FY)	2008 – 2009
Keywords	ペトリネット / オントロジー / 視覚的デバッグ / モデル検査 / OWL / HFPNe / 細胞分化
Research Abstract	The pathway modeling and simulation architecture named (Hybrid Functional Petri net: HFPNe) has been developed and implemented. In this research, a model checking concept is introduced to the HFPNe. A simulation model of C. elegans cell fate determination is created using HFPNe and the reasonable rule of the cell fate determination is selected by using the model checking approach. Furthermore, an algorithm to extract the active sub-pathways from a given HFPNe model and the trajectory of these sub-pathways is developed. The applicability is demonstrated using the circadian clock simulation model with HFPNe.