MIRACH: Efficient model checker for quantitative biological pathway models

Chuan Hock Koh; Masao Nagasaki; Ayumu Saito; Chen Li; Limsoon Wong; Satoru Miyano

doi:10.1093/bioinformatics/btq727

MIRACH: Efficient model checker for quantitative biological pathway models

Chuan Hock Koh, Masao Nagasaki, Ayumu Saito, Chen Li, Limsoon Wong, Satoru Miyano

Tohoku Medical Megabank Organization (ToMMo)

Research output: Contribution to journal › Article › peer-review

6 Citations (Scopus)

Abstract

Summary: Model checking is playing an increasingly important role in systems biology as larger and more complex biological pathways are being modeled. In this article we report the release of an efficient model checker MIRACH 1.0, which supports any model written in popular formats such as CSML and SBML. MIRACH is integrated with a Petri-net-based simulation engine, enabling efficient online (on-the-fly) checking. In our experiment, by using Levchenko et al. model, we reveal that timesaving gains by using MIRACH easily surpass 400% compared with its offline-based counterpart.

Original language	English
Article number	btq727
Pages (from-to)	734-735
Number of pages	2
Journal	Bioinformatics
Volume	27
Issue number	5
DOIs	https://doi.org/10.1093/bioinformatics/btq727
Publication status	Published - 2011 Mar

ASJC Scopus subject areas

Statistics and Probability
Biochemistry
Molecular Biology
Computer Science Applications
Computational Theory and Mathematics
Computational Mathematics

Access to Document

10.1093/bioinformatics/btq727

Cite this

@article{fd8c3038bfb14de8a0b822264920c222,

title = "MIRACH: Efficient model checker for quantitative biological pathway models",

abstract = "Summary: Model checking is playing an increasingly important role in systems biology as larger and more complex biological pathways are being modeled. In this article we report the release of an efficient model checker MIRACH 1.0, which supports any model written in popular formats such as CSML and SBML. MIRACH is integrated with a Petri-net-based simulation engine, enabling efficient online (on-the-fly) checking. In our experiment, by using Levchenko et al. model, we reveal that timesaving gains by using MIRACH easily surpass 400% compared with its offline-based counterpart.",

author = "Koh, {Chuan Hock} and Masao Nagasaki and Ayumu Saito and Chen Li and Limsoon Wong and Satoru Miyano",

note = "Funding Information: Funding: Singapore National Research Foundation grant NRF-G-CRP-2997-04-082(d) (to L.W. and C.H.K., in parts); National University of Singapore NGS scholarship (to C.H.K., in parts).",

year = "2011",

month = mar,

doi = "10.1093/bioinformatics/btq727",

language = "English",

volume = "27",

pages = "734--735",

journal = "Bioinformatics",

issn = "1367-4803",

publisher = "Oxford University Press",

number = "5",

}

TY - JOUR

T1 - MIRACH

T2 - Efficient model checker for quantitative biological pathway models

AU - Koh, Chuan Hock

AU - Nagasaki, Masao

AU - Saito, Ayumu

AU - Li, Chen

AU - Wong, Limsoon

AU - Miyano, Satoru

N1 - Funding Information: Funding: Singapore National Research Foundation grant NRF-G-CRP-2997-04-082(d) (to L.W. and C.H.K., in parts); National University of Singapore NGS scholarship (to C.H.K., in parts).

PY - 2011/3

Y1 - 2011/3

N2 - Summary: Model checking is playing an increasingly important role in systems biology as larger and more complex biological pathways are being modeled. In this article we report the release of an efficient model checker MIRACH 1.0, which supports any model written in popular formats such as CSML and SBML. MIRACH is integrated with a Petri-net-based simulation engine, enabling efficient online (on-the-fly) checking. In our experiment, by using Levchenko et al. model, we reveal that timesaving gains by using MIRACH easily surpass 400% compared with its offline-based counterpart.

AB - Summary: Model checking is playing an increasingly important role in systems biology as larger and more complex biological pathways are being modeled. In this article we report the release of an efficient model checker MIRACH 1.0, which supports any model written in popular formats such as CSML and SBML. MIRACH is integrated with a Petri-net-based simulation engine, enabling efficient online (on-the-fly) checking. In our experiment, by using Levchenko et al. model, we reveal that timesaving gains by using MIRACH easily surpass 400% compared with its offline-based counterpart.

UR - http://www.scopus.com/inward/record.url?scp=79951991634&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79951991634&partnerID=8YFLogxK

U2 - 10.1093/bioinformatics/btq727

DO - 10.1093/bioinformatics/btq727

M3 - Article

C2 - 21208986

AN - SCOPUS:79951991634

SN - 1367-4803

VL - 27

SP - 734

EP - 735

JO - Bioinformatics

JF - Bioinformatics

IS - 5

M1 - btq727

ER -

MIRACH: Efficient model checker for quantitative biological pathway models

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this