{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T01:10:11Z","timestamp":1768093811667,"version":"3.49.0"},"reference-count":15,"publisher":"Oxford University Press (OUP)","issue":"5","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,3,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>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.<\/jats:p>\n               <jats:p>Availability and implementation: MIRACH 1.0 was developed using Java and thus executable on any platform installed with JDK 6.0 (not JRE 6.0) or later. MIRACH 1.0, along with its source codes, documentation and examples are available at http:\/\/sourceforge.net\/projects\/mirach\/ under the LGPLv3 license.<\/jats:p>\n               <jats:p>Contact: \u00a0masao@ims.u-tokyo.ac.jp<\/jats:p>\n               <jats:p>Supplementary information: \u00a0Supplementary data are available at Bioinformatics online.<\/jats:p>","DOI":"10.1093\/bioinformatics\/btq727","type":"journal-article","created":{"date-parts":[[2011,1,6]],"date-time":"2011-01-06T01:42:09Z","timestamp":1294278129000},"page":"734-735","source":"Crossref","is-referenced-by-count":8,"title":["MIRACH: efficient model checker for quantitative biological pathway models"],"prefix":"10.1093","volume":"27","author":[{"given":"Chuan Hock","family":"Koh","sequence":"first","affiliation":[{"name":"1 NUS Graduate School for Integrative Sciences and Engineering, Singapore 117597, 2School of Computing, National University of Singapore, Computing Drive, Singapore 117417 and 3Human Genome Center, Institute of Medical Science, University of Tokyo, 4-6-1 Shirokanedai, Minato-ku, Tokyo 108-8639, Japan"},{"name":"1 NUS Graduate School for Integrative Sciences and Engineering, Singapore 117597, 2School of Computing, National University of Singapore, Computing Drive, Singapore 117417 and 3Human Genome Center, Institute of Medical Science, University of Tokyo, 4-6-1 Shirokanedai, Minato-ku, Tokyo 108-8639, Japan"},{"name":"1 NUS Graduate School for Integrative Sciences and Engineering, Singapore 117597, 2School of Computing, National University of Singapore, Computing Drive, Singapore 117417 and 3Human Genome Center, Institute of Medical Science, University of Tokyo, 4-6-1 Shirokanedai, Minato-ku, Tokyo 108-8639, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masao","family":"Nagasaki","sequence":"additional","affiliation":[{"name":"1 NUS Graduate School for Integrative Sciences and Engineering, Singapore 117597, 2School of Computing, National University of Singapore, Computing Drive, Singapore 117417 and 3Human Genome Center, Institute of Medical Science, University of Tokyo, 4-6-1 Shirokanedai, Minato-ku, Tokyo 108-8639, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ayumu","family":"Saito","sequence":"additional","affiliation":[{"name":"1 NUS Graduate School for Integrative Sciences and Engineering, Singapore 117597, 2School of Computing, National University of Singapore, Computing Drive, Singapore 117417 and 3Human Genome Center, Institute of Medical Science, University of Tokyo, 4-6-1 Shirokanedai, Minato-ku, Tokyo 108-8639, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chen","family":"Li","sequence":"additional","affiliation":[{"name":"1 NUS Graduate School for Integrative Sciences and Engineering, Singapore 117597, 2School of Computing, National University of Singapore, Computing Drive, Singapore 117417 and 3Human Genome Center, Institute of Medical Science, University of Tokyo, 4-6-1 Shirokanedai, Minato-ku, Tokyo 108-8639, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Limsoon","family":"Wong","sequence":"additional","affiliation":[{"name":"1 NUS Graduate School for Integrative Sciences and Engineering, Singapore 117597, 2School of Computing, National University of Singapore, Computing Drive, Singapore 117417 and 3Human Genome Center, Institute of Medical Science, University of Tokyo, 4-6-1 Shirokanedai, Minato-ku, Tokyo 108-8639, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Satoru","family":"Miyano","sequence":"additional","affiliation":[{"name":"1 NUS Graduate School for Integrative Sciences and Engineering, Singapore 117597, 2School of Computing, National University of Singapore, Computing Drive, Singapore 117417 and 3Human Genome Center, Institute of Medical Science, University of Tokyo, 4-6-1 Shirokanedai, Minato-ku, Tokyo 108-8639, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2011,1,5]]},"reference":[{"issue":"Suppl. 1","key":"2023012511572946600_B1","doi-asserted-by":"crossref","first-page":"i19","DOI":"10.1093\/bioinformatics\/bti1048","article-title":"Validation of qualitative models of genetic regulatory networks by model checking : analysis of the nutritional stress response in Escherichia coli","volume":"21","author":"Batt","year":"2005","journal-title":"Bioinformatics"},{"key":"2023012511572946600_B2","doi-asserted-by":"crossref","first-page":"i603","DOI":"10.1093\/bioinformatics\/btq387","article-title":"Efficient parameter search for qualitative models of regulatory networks using symbolic model checking","volume":"26","author":"Batt","year":"2010","journal-title":"Bioinformatics"},{"key":"2023012511572946600_B3","first-page":"231","article-title":"Statistical model checking in BioLab: applications to the automated analysis of T-cell receptor signaling pathway","volume-title":"Proceedings of the 6th International Conference CMSB 2008, Rostock, Germany","author":"Clarke","year":"2008"},{"key":"2023012511572946600_B4","article-title":"A Monte Carlo model checker for probabilistic LTL with numerical constraints","volume-title":"Technical Report TR-2008-282","author":"Donaldson","year":"2008"},{"key":"2023012511572946600_B5","first-page":"269","article-title":"A model checking approach to the parameter estimation of biochemical pathways","volume-title":"Proceedings of the 6th International Conference CMSB 2008, Rostock, Germany","author":"Donaldson","year":"2008"},{"key":"2023012511572946600_B6","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/j.tcs.2007.11.013","article-title":"Probabilistic model checking of complex biological pathways","volume":"391","author":"Heath","year":"2008","journal-title":"Theor. Comput. Sci."},{"key":"2023012511572946600_B7","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1093\/bioinformatics\/btg015","article-title":"The systems biology markup language (SBML): a medium for representation and exchange of biochemical network models","volume":"19","author":"Hucka","year":"2003","journal-title":"Bioinformatics"},{"key":"2023012511572946600_B8","doi-asserted-by":"crossref","first-page":"1794","DOI":"10.1093\/bioinformatics\/btq276","article-title":"DA 1.0: parameter estimation of biological pathway using data assimilation approach","volume":"26","author":"Koh","year":"2010","journal-title":"Bioinformatics"},{"key":"2023012511572946600_B9","doi-asserted-by":"crossref","first-page":"5818","DOI":"10.1073\/pnas.97.11.5818","article-title":"Scaffold proteins may biphasically affect the levels of mitogen-activated protein kinase signaling and reduce its threshold properties","volume":"97","author":"Levchenko","year":"2000","journal-title":"Proc. Natl Acad. Sci. USA"},{"key":"2023012511572946600_B10","doi-asserted-by":"crossref","first-page":"0002","DOI":"10.3233\/ISB-2010-0415","article-title":"Cell illustrator 4.0: a computational platform for systems biology","volume":"10","author":"Nagasaki","year":"2010","journal-title":"In Silico Biol."},{"key":"2023012511572946600_B11","first-page":"100","article-title":"Cell fate simulation model of gustatory neurons with microRNAs double-negative feedback loop by hybrid functional petri net with extension","volume":"17","author":"Saito","year":"2006","journal-title":"Genome Inform."},{"key":"2023012511572946600_B12","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1214\/aoms\/1177731118","article-title":"Sequential tests of statistical hypotheses","volume":"16","author":"Wald","year":"1945","journal-title":"Ann. Math. Stat."},{"key":"2023012511572946600_B13","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1080\/01621459.1927.10502953","article-title":"Probable inference, the law of succession, and statistical inference","volume":"22","author":"Wilson","year":"1927","journal-title":"J. Am. Stat. Assoc."},{"key":"2023012511572946600_B14","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/11609773_10","article-title":"Error control for probabilistic model checking","volume":"3855","author":"Younes","year":"2006","journal-title":"Lect. Notes Comput. Sci."},{"key":"2023012511572946600_B15","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","article-title":"Numerical vs statistical probabilistic model checking","volume":"8","author":"Younes","year":"2006","journal-title":"Int. J. Software Tools Technol Tran."}],"container-title":["Bioinformatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/bioinformatics\/article-pdf\/27\/5\/734\/48867392\/bioinformatics_27_5_734.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/bioinformatics\/article-pdf\/27\/5\/734\/48867392\/bioinformatics_27_5_734.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,25]],"date-time":"2023-01-25T12:42:11Z","timestamp":1674650531000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/bioinformatics\/article\/27\/5\/734\/1746120"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,5]]},"references-count":15,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2011,3,1]]}},"URL":"https:\/\/doi.org\/10.1093\/bioinformatics\/btq727","relation":{},"ISSN":["1367-4811","1367-4803"],"issn-type":[{"value":"1367-4811","type":"electronic"},{"value":"1367-4803","type":"print"}],"subject":[],"published-other":{"date-parts":[[2011,3,1]]},"published":{"date-parts":[[2011,1,5]]}}}