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

开发并实现了一种路径建模与仿真体系结构（Hybrid Functional Petri net: HFPNe）。在本研究中，将模型检验的概念引入到HFPNe中。利用HFPNe建立了秀丽隐杆线虫细胞命运决定的仿真模型，并利用模型检验方法选择了细胞命运决定的合理规则。在此基础上，提出了一种从给定HFPNe模型中提取活动子路径及其运动轨迹的算法。利用HFPNe的生物钟仿真模型证明了该方法的适用性。

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.