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

高层Petri网可视化模型检验方法及其在动态生物通路模型中的应用

• 批准号: 20700265
• 负责人: NAGASAKI Masao
• 金额: $ 2.66万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2008
• 资助国家: 日本
• 起止时间: 2008 至 2009
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20700265/
• 关键词: ペトリネット; オントロジー; 視覚的デバッグ; モデル検査; OWL; HFPNe; 細胞分化; ASTD

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.

已经开发和实施了名为“混合功能性培养皿：HFPNE）的途径建模和仿真体系结构”。在这项研究中，将模型检查概念引入HFPNE。使用HFPNE创建了秀丽隐杆线虫细胞命运测定的模拟模型，并使用模型检查方法选择细胞命运确定的合理规则。此外，开发了一种从给定的HFPNE模型中提取活性子轨道的算法，并开发了这些子座道的轨迹。使用带有HFPNE的昼夜节律时钟仿真模型来证明适用性。

项目成果

A computational platform for systems biology

系统生物学计算平台

• 发表时间: 2009
• 期刊: Cell Illustrator 4. 0 10
• 作者: Nagasaki;M.;Saito A.;Jeong E;Li C.;Kojima;K;Ikeda;E.;Miyano;S
• 通讯作者: S

Rule-based reasoning for system dynamics in cell systems

细胞系统中系统动力学的基于规则的推理

• 发表时间: 2008
• 期刊: Genome Informatics 20
• 作者: Jeong;E. Nagasaki;M.;MiYano;S.
• 通讯作者: S.

Systematic reconstruction of TRANSPATH data into Cell System Markup Language

• DOI: 10.1186/1752-0509-2-53
• 发表时间: 2008-06-23
• 期刊: BMC SYSTEMS BIOLOGY
• 作者: Nagasaki, Masao;Saito, Ayumu;Miyano, Satoru
• 通讯作者: Miyano, Satoru

Simulation-based model checking approach to cell fate pecification during Caenorhabditis elegans vulval development by hybrid functional Petri net with extension

基于仿真的模型检查方法，通过具有可扩展性的混合功能 Petri 网，对秀丽隐杆线虫外阴发育过程中的细胞命运进行指定

• 发表时间: 2009
• 期刊: BMC Systems Biology 3
• 作者: Li;C. *;Nagasaki;M. *;Ueno;K.;Miyano;S.
• 通讯作者: S.

Simulation-based model checking approach to cell fate specification during Caenorhabditis elegans vulval development by hybrid function Petri net with

基于仿真的模型检查方法，通过混合函数 Petri 网对秀丽隐杆线虫外阴发育过程中的细胞命运规范进行检查

• 发表时间: 2009
• 期刊: BMC Systems Biology 3:42(online journal)
• 作者: Chen Li^*;Nagasaki M^*;Ueno K;Miyano S (equal contributor)
• 通讯作者: Miyano S (equal contributor)