{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T02:12:40Z","timestamp":1768097560147,"version":"3.49.0"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"1","content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["BMC Syst Biol"],"published-print":{"date-parts":[[2009,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:sec><jats:title>Background<\/jats:title><jats:p>Model checking approaches were applied to biological pathway validations around 2003. Recently, Fisher<jats:italic>et al<\/jats:italic>. have proved the importance of model checking approach by inferring new regulation of signaling crosstalk in<jats:italic>C. elegans<\/jats:italic>and confirming the regulation with biological experiments. They took a discrete and state-based approach to explore all possible states of the system underlying vulval precursor cell (VPC) fate specification for desired properties. However, since both discrete and continuous features appear to be an indispensable part of biological processes, it is more appropriate to use quantitative models to capture the dynamics of biological systems. Our key motivation of this paper is to establish a quantitative methodology to model and analyze<jats:italic>in silico<\/jats:italic>models incorporating the use of model checking approach.<\/jats:p><\/jats:sec><jats:sec><jats:title>Results<\/jats:title><jats:p>A novel method of modeling and simulating biological systems with the use of model checking approach is proposed based on hybrid functional Petri net with extension (HFPNe) as the framework dealing with both discrete and continuous events. Firstly, we construct a quantitative VPC fate model with 1761 components by using HFPNe. Secondly, we employ two major biological fate determination rules \u2013 Rule I and Rule II \u2013 to VPC fate model. We then conduct 10,000 simulations for each of 48 sets of different genotypes, investigate variations of cell fate patterns under each genotype, and validate the two rules by comparing three simulation targets consisting of fate patterns obtained from<jats:italic>in silico<\/jats:italic>and<jats:italic>in vivo<\/jats:italic>experiments. In particular, an evaluation was successfully done by using our VPC fate model to investigate one target derived from biological experiments involving hybrid lineage observations. However, the understandings of hybrid lineages are hard to make on a discrete model because the hybrid lineage occurs when the system comes close to certain thresholds as discussed by Sternberg and Horvitz in 1986. Our simulation results suggest that: Rule I that cannot be applied with qualitative based model checking, is more reasonable than Rule II owing to the high coverage of predicted fate patterns (except for the genotype of<jats:italic>lin-15ko; lin-12ko<\/jats:italic>double mutants). More insights are also suggested.<\/jats:p><\/jats:sec><jats:sec><jats:title>Conclusion<\/jats:title><jats:p>The quantitative simulation-based model checking approach is a useful means to provide us valuable biological insights and better understandings of biological systems and observation data that may be hard to capture with the qualitative one.<\/jats:p><\/jats:sec>","DOI":"10.1186\/1752-0509-3-42","type":"journal-article","created":{"date-parts":[[2009,4,28]],"date-time":"2009-04-28T06:27:45Z","timestamp":1240900065000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":35,"title":["Simulation-based model checking approach to cell fate specification during Caenorhabditis elegans vulval development by hybrid functional Petri net with extension"],"prefix":"10.1186","volume":"3","author":[{"given":"Chen","family":"Li","sequence":"first","affiliation":[]},{"given":"Masao","family":"Nagasaki","sequence":"additional","affiliation":[]},{"given":"Kazuko","family":"Ueno","sequence":"additional","affiliation":[]},{"given":"Satoru","family":"Miyano","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,4,27]]},"reference":[{"key":"310_CR1","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled DA: Model Checking. 1999, The MIT Press"},{"key":"310_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and Software Verification: Model-Checking Techniques and Tools","author":"B B\u00e9rard","year":"2001","unstructured":"B\u00e9rard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P, McKenzie P: Systems and Software Verification: Model-Checking Techniques and Tools. 2001, Springer"},{"key":"310_CR3","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logic of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke EM, Emerson EA: Design and synthesis of synchronization skeletons using branching time temporal logic. Logic of Programs. 1982, 52-71. New York: Springer Berlin\/Heidelberg"},{"key":"310_CR4","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume":"137","author":"JP Queille","year":"1982","unstructured":"Queille JP, Sifakis J: Specification and verification of concurrent systems in CESAR. Lecture Notes in Computer Science. 1982, 137: 337-351.","journal-title":"Lecture Notes in Computer Science"},{"key":"310_CR5","first-page":"149","volume-title":"Proceedings of CMSB 2003 (Computational Methods in Systems Biology)","author":"N Chabrier","year":"2003","unstructured":"Chabrier N, Fages F: Symbolic model checking of biochemical networks. Proceedings of CMSB 2003 (Computational Methods in Systems Biology). 2003, 149-162. Italy: Springer Berlin\/Heidelberg"},{"issue":"3","key":"310_CR6","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1385\/CBB:38:3:271","volume":"38","author":"M Antoniotti","year":"2003","unstructured":"Antoniotti M, Policriti A, Ugel N, Mishra B: Model building and model checking for biochemical processes. Cell Biochem Biophys. 2003, 38 (3): 271-286.","journal-title":"Cell Biochem Biophys"},{"issue":"Suppl 1","key":"310_CR7","doi-asserted-by":"publisher","first-page":"i19","DOI":"10.1093\/bioinformatics\/bti1048","volume":"21","author":"G Batt","year":"2005","unstructured":"Batt G, Ropers D, de Jong H, Geiselmann J, Mateescu R, Page M, Schneider D: Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in Escherichia coli. Bioinformatics. 2005, 21 (Suppl 1): i19-i28.","journal-title":"Bioinformatics"},{"key":"310_CR8","first-page":"179","volume-title":"Proceedings of CMSB 2005 (Computational Methods in Systems Biology)","author":"M Calder","year":"2005","unstructured":"Calder M, Vyshemirsky V, Gilbert D, Orton R: Analysis of signalling pathways using the prism model checker. Proceedings of CMSB 2005 (Computational Methods in Systems Biology). Edited by: Plotkin G. 2005, 179-190. University of Edinburgh"},{"issue":"5","key":"310_CR9","doi-asserted-by":"publisher","first-page":"e92","DOI":"10.1371\/journal.pcbi.0030092","volume":"3","author":"J Fisher","year":"2007","unstructured":"Fisher J, Piterman N, Hajnal A, Henzinger TA: Predictive modeling of signaling crosstalk during C. elegans vulval development. PLoS Comput Biol. 2007, 3 (5): e92-","journal-title":"PLoS Comput Biol"},{"issue":"3","key":"310_CR10","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2007.11.013","volume":"391","author":"J Heath","year":"2008","unstructured":"Heath J, Kwiatkowska M, Norman G, Parker D, Tymchyshyn O: Probabilistic model checking of complex biological pathways. Theor Comput Sci. 2008, 391 (3): 239-257.","journal-title":"Theor Comput Sci"},{"issue":"4","key":"310_CR11","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/1364644.1364651","volume":"35","author":"MZ Kwiatkowska","year":"2008","unstructured":"Kwiatkowska MZ, Norman G, Parker D: Using probabilistic model checking in systems biology. SIGMETRICS Performance Evaluation Review. 2008, 35 (4): 14-21.","journal-title":"SIGMETRICS Performance Evaluation Review"},{"issue":"16","key":"310_CR12","doi-asserted-by":"publisher","first-page":"i227","DOI":"10.1093\/bioinformatics\/btn275","volume":"24","author":"PT Monteiro","year":"2008","unstructured":"Monteiro PT, Ropers D, Mateescu R, Freitas AT, de Jong H: Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics. 2008, 24 (16): i227-i233.","journal-title":"Bioinformatics"},{"key":"310_CR13","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur R, Henzinger TA: Reactive modules. Formal Methods in System Design. 1999, 15: 7-48.","journal-title":"Formal Methods in System Design"},{"key":"310_CR14","first-page":"459","volume-title":"Pac Symp Biocomput","author":"A Regev","year":"2001","unstructured":"Regev A, Silverman W, Shapiro E: Representation and simulation of biochemical processes using the pi-calculus process algebra. Pac Symp Biocomput. 2001, 459-470."},{"issue":"2","key":"310_CR15","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1042\/bj20021824","volume":"373","author":"M Hatakeyama","year":"2003","unstructured":"Hatakeyama M, Kimura S, Naka T, Kawasaki T, Yumoto N, Ichikawa M, Kim JH, Saito K, Saeki M, Shirouzu M, Yokoyama S, Konagaya A: A computational model on the modulation of mitogen-activated protein kinase (MAPK) and Akt pathways in heregulin-induced ErbB signalling. Biochem J. 2003, 373 (2): 451-463.","journal-title":"Biochem J"},{"issue":"3","key":"310_CR16","first-page":"389","volume":"3","author":"H Matsuno","year":"2003","unstructured":"Matsuno H, Tanaka Y, Aoshima H, Doi A, Matsui M, Miyano S: Biopathways representation and simulation on hybrid functional Petri net. In Silico Biol. 2003, 3 (3): 389-404.","journal-title":"In Silico Biol"},{"key":"310_CR17","volume-title":"Bioinformatics Technologies","author":"M Nagasaki","year":"2005","unstructured":"Nagasaki M, Doi A, Matsuno H, Miyano S: Computational modeling of biological processes with Petri net based architecture. Bioinformatics Technologies. Edited by: Chen YP. 2005, Springer Berlin Heidelberg"},{"issue":"1","key":"310_CR18","first-page":"180","volume":"15","author":"M Nagasaki","year":"2004","unstructured":"Nagasaki M, Doi A, Matsuno H, Miyano S: A versatile Petri net based architecture for modeling and simulation of complex biological processes. Genome Inform. 2004, 15 (1): 180-197.","journal-title":"Genome Inform"},{"issue":"Pt 6","key":"310_CR19","doi-asserted-by":"publisher","first-page":"1513","DOI":"10.1042\/bst0311513","volume":"31","author":"JW Pinney","year":"2003","unstructured":"Pinney JW, Westhead DR, McConkey GA: Petri net representations in systems biology. Biochem Soc Trans. 2003, 31 (Pt 6): 1513-1515.","journal-title":"Biochem Soc Trans"},{"issue":"11","key":"310_CR20","doi-asserted-by":"publisher","first-page":"3166","DOI":"10.1093\/ietfec\/e89-a.11.3166","volume":"E89-A","author":"H Matsuno","year":"2006","unstructured":"Matsuno H, Li C, Miyano S: Petri net based descriptions for systematic understanding of biological pathways. IEICE Trans Fundamentals. 2006, E89-A (11): 3166-3174.","journal-title":"IEICE Trans Fundamentals"},{"issue":"1","key":"310_CR21","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/s12038-007-0011-6","volume":"32","author":"C Li","year":"2007","unstructured":"Li C, Ge QW, Nakata M, Matsuno H, Miyano S: Modelling and simulation of signal transductions in an apoptosis pathway by using timed Petri nets. J Biosci. 2007, 32 (1): 113-127.","journal-title":"J Biosci"},{"issue":"4","key":"310_CR22","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1093\/bib\/bbm029","volume":"8","author":"C Chaouiya","year":"2007","unstructured":"Chaouiya C: Petri net modelling of biological networks. Brief Bioinform. 2007, 8 (4): 210-219.","journal-title":"Brief Bioinform"},{"key":"310_CR23","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1002\/9780470253489.ch7","volume-title":"Analysis of Biological Networks","author":"I Koch","year":"2008","unstructured":"Koch I, Heiner M: Petri nets. Analysis of Biological Networks. Edited by: Junker BH, Schreiber F. 2008, 139-180. A Wiley Interscience Publication"},{"key":"310_CR24","unstructured":"Cell Illustrator. http:\/\/www.cellillustrator.com\/"},{"key":"310_CR25","unstructured":"Cell Illustrator Online. , http:\/\/cionline.hgc.jp\/"},{"issue":"3","key":"310_CR26","first-page":"181","volume":"2","author":"M Nagasaki","year":"2003","unstructured":"Nagasaki M, Doi A, Matsuno H, Miyano S: Genomic Object Net: I. A platform for modelling and simulating biopathways. Appl Bioinformatics. 2003, 2 (3): 181-184.","journal-title":"Appl Bioinformatics"},{"issue":"3","key":"310_CR27","doi-asserted-by":"crossref","first-page":"271","DOI":"10.3233\/ISB-00133","volume":"4","author":"A Doi","year":"2004","unstructured":"Doi A, Fujita S, Matsuno H, Nagasaki M, Miyano S: Constructing biological pathway models with hybrid functional Petri nets. In Silico Biol. 2004, 4 (3): 271-291.","journal-title":"In Silico Biol"},{"issue":"3","key":"310_CR28","first-page":"185","volume":"2","author":"A Doi","year":"2003","unstructured":"Doi A, Nagasaki M, Fujita S, Matsuno H, Miyano S: Abstract Genomic Object Net: II. modelling biopathways by hybrid functional Petri net with extension. Appl Bioinformatics. 2003, 2 (3): 185-188.","journal-title":"Appl Bioinformatics"},{"key":"310_CR29","first-page":"341","volume-title":"Pac Symp Biocomput","author":"H Matsuno","year":"2000","unstructured":"Matsuno H, Doi A, Nagasaki M, Miyano S: Hybrid Petri net representation of gene regulatory network. Pac Symp Biocomput. 2000, 341-352."},{"key":"310_CR30","first-page":"152","volume-title":"Pac Symp Biocomput","author":"H Matsuno","year":"2003","unstructured":"Matsuno H, Murakami R, Yamane R, Yamasaki N, Fujita S, Yoshimori H, Miyano S: Boundary formation by notch signaling in Drosophila multicellular systems: experimental observations and gene network modeling by Genomic Object Net. Pac Symp Biocomput. 2003, 152-163."},{"key":"310_CR31","first-page":"427","volume-title":"Pac Symp Biocomput","author":"S Troncale","year":"2006","unstructured":"Troncale S, Tahi F, Campard D, Vannier JP, Guespin J: Modeling and simulation with hybrid functional Petri nets of the role of interleukin-6 in human early haematopoiesis. Pac Symp Biocomput. 2006, 427-438."},{"issue":"4","key":"310_CR32","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1016\/0092-8674(89)90103-7","volume":"58","author":"PW Sternberg","year":"1989","unstructured":"Sternberg PW, Horvitz HR: The combined action of two intercellular signaling pathways specifies three cell fates during vulval induction in C. elegans. Cell. 1989, 58 (4): 679-693.","journal-title":"Cell"},{"key":"310_CR33","volume-title":"Petri Net Theory and the Modeling of Systems","author":"JL Peterson","year":"1981","unstructured":"Peterson JL: Petri Net Theory and the Modeling of Systems. 1981, Prentice Hall"},{"key":"310_CR34","first-page":"1","volume":"8","author":"I Greenwald","year":"2005","unstructured":"Greenwald I: LIN-12\/Notch signaling in C. elegans. Worm Book. 2005, 8: 1-16.","journal-title":"Worm Book"},{"issue":"5658","key":"310_CR35","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1126\/science.1091639","volume":"303","author":"A Yoo","year":"2004","unstructured":"Yoo A, Bais C, Greenwald I: Crosstalk between the EGFR and LIN-12\/Notch pathways in C. elegans vulval development. Science. 2004, 303 (5658): 663-666.","journal-title":"Science"},{"issue":"5","key":"310_CR36","doi-asserted-by":"crossref","first-page":"1373","DOI":"10.1242\/dev.122.5.1373","volume":"122","author":"S Christensen","year":"1996","unstructured":"Christensen S, Kodoyianni V, Bosenberg M, Friedman L, Kimble J: lag-1, a gene required for lin-12 and glp-1 signaling in Caenorhabditis elegans, is homologous to human CBF1 and Drosophila Su(H). Development. 1996, 122 (5): 1373-1383.","journal-title":"Development"},{"issue":"5","key":"310_CR37","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1016\/j.devcel.2006.04.001","volume":"10","author":"M Cui","year":"2006","unstructured":"Cui M, Chen J, Myers TR, Hwang BJ, Sternberg PW, Greenwald I, Han M: SynMuv genes redundantly inhibit lin-3\/EGF expression to prevent inappropriate vulval induction in C. elegans. Dev Cell. 2006, 10 (5): 667-672.","journal-title":"Dev Cell"},{"issue":"6","key":"310_CR38","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1101\/gad.7.6.933","volume":"7","author":"LM Miller","year":"1993","unstructured":"Miller LM, Gallegos ME, Morisseau B, Kim S: lin-31, a Caenorhabditis elegans HNF-3\/fork head transcription factor homolog, specifies three alternative cell fates in vulval development. Genes Dev. 1993, 7 (6): 933-947.","journal-title":"Genes Dev"},{"issue":"5","key":"310_CR39","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1016\/0092-8674(86)90842-1","volume":"44","author":"PW Sternberg","year":"1986","unstructured":"Sternberg PW, Horvitz HR: Pattern formation during vulval development in C. elegans. Cell. 1986, 44 (5): 761-772.","journal-title":"Cell"},{"issue":"2","key":"310_CR40","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1101\/gad.8.2.160","volume":"8","author":"M Lackner","year":"1994","unstructured":"Lackner M, Kornfeld K, Miller LM, Horvitz HR, Kim S: A MAP kinase homolog, mpk-1, is involved in ras-mediated induction of vulval cell fates in Caenorhabditis elegans. Genes Dev. 1994, 8 (2): 160-173.","journal-title":"Genes Dev"},{"issue":"6916","key":"310_CR41","doi-asserted-by":"publisher","first-page":"686","DOI":"10.1038\/nature01234","volume":"420","author":"DD Shaye","year":"2002","unstructured":"Shaye DD, Greenwald I: Endocytosis-mediated downregulation of LIN-12\/Notch upon Ras activation in Caenorhabditis elegans. Nature. 2002, 420 (6916): 686-690.","journal-title":"Nature"},{"key":"310_CR42","first-page":"1","volume":"25","author":"PW Sternberg","year":"2005","unstructured":"Sternberg PW: Vulval development. Worm Book. 2005, 25: 1-28.","journal-title":"Worm Book"},{"key":"310_CR43","volume-title":"Caenorhabditis elegans \u2013 Symphony of 1000 Cells","author":"Y Kohara","year":"1997","unstructured":"Kohara Y: Caenorhabditis elegans \u2013 Symphony of 1000 Cells. 1997, In Japanese, Kyoritsu Shuppan"},{"key":"310_CR44","volume-title":"C. Elegans II: Monograph 33","author":"DL Riddle","year":"1998","unstructured":"Riddle DL, Blumenthal T, Meyer BJ, Priess JR: C. Elegans II: Monograph 33. 1998, Cold Spring Harbor Laboratory Press"},{"issue":"4","key":"310_CR45","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1016\/S0092-8674(00)81186-1","volume":"93","author":"PB Tan","year":"1998","unstructured":"Tan PB, Lackner MR, Kim SK: MAP kinase signaling specificity mediated by the LIN-1 Ets\/LIN-31 WH transcription factor complex during C. elegans vulval induction. Cell. 1998, 93 (4): 569-580.","journal-title":"Cell"},{"issue":"5506","key":"310_CR46","doi-asserted-by":"publisher","first-page":"1055","DOI":"10.1126\/science.1055642","volume":"291","author":"T Berset","year":"2001","unstructured":"Berset T, Hoier EF, Battu G, Canevascini S, Hajnal A: Notch inhibition of RAS signaling through MAP kinase phosphatase LIP-1 during C. elegans vulval development. Science. 2001, 291 (5506): 1055-1058.","journal-title":"Science"},{"issue":"6","key":"310_CR47","doi-asserted-by":"crossref","first-page":"623","DOI":"10.3233\/ISI-2007-00335","volume":"7","author":"E Jeong","year":"2007","unstructured":"Jeong E, Nagasaki M, Saito A, Miyano S: Cell System Ontology: Representation for modeling, visualizing, and simulating biological pathways. In Silico Biol. 2007, 7 (6): 623-638.","journal-title":"In Silico Biol"},{"key":"310_CR48","unstructured":"Pnuts., http:\/\/www.pnuts.org\/"},{"issue":"1","key":"310_CR49","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/0012-1606(77)90158-0","volume":"56","author":"JE Sulston","year":"1977","unstructured":"Sulston JE, Horvitz HR: Post-embryonic cell lineages of the nematode, Caenorhabditis elegans. Dev Biol. 1977, 56 (1): 110-156.","journal-title":"Dev Biol"},{"issue":"11","key":"310_CR50","doi-asserted-by":"publisher","first-page":"1328","DOI":"10.1101\/gad.333505","volume":"19","author":"TA Berset","year":"2005","unstructured":"Berset TA, Hoier EF, Hajnal A: The C. elegans homolog of the mammalian tumor suppressor Dep-1\/Scc1 inhibits EGFR signaling to regulate binary cell fate decisions. Genes Dev. 2005, 19 (11): 1328-1340.","journal-title":"Genes Dev"},{"issue":"6110","key":"310_CR51","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1038\/326259a0","volume":"326","author":"EL Ferguson","year":"1987","unstructured":"Ferguson EL, Sternberg PW, Horvitz HR: A genetic pathway for the specification of the vulval cell lineages of Caenorhabditis elegans. Nature. 1987, 326 (6110): 259-267.","journal-title":"Nature"},{"issue":"2","key":"310_CR52","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1016\/0012-1606(81)90152-4","volume":"87","author":"J Kimble","year":"1981","unstructured":"Kimble J: Alterations in cell lineage following laser ablation of cells in the somatic gonad of Caenorhabditis elegans. Dev Biol. 1981, 87 (2): 286-300.","journal-title":"Dev Biol"},{"issue":"4","key":"310_CR53","doi-asserted-by":"crossref","first-page":"899","DOI":"10.1093\/genetics\/126.4.899","volume":"126","author":"M Han","year":"1990","unstructured":"Han M, Aroian RV, Sternberg PW: The let-60 locus controls the switch between vulval and nonvulval cell fates in Caenorhabditis elegans. Genetics. 1990, 126 (4): 899-913.","journal-title":"Genetics"},{"key":"310_CR54","unstructured":"VPC fate specification of C. elegans in CSML., http:\/\/www.csml.org\/models\/csml-models\/vulvaldev\/"},{"key":"310_CR55","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume":"1427","author":"R Alur","year":"1998","unstructured":"Alur R, Henzinger TA, Mang FYC, Qadeer S, Rajamani SK, Tasiran S: MOCHA: modularity in model checking. Lecture Notes in Computer Science. 1998, 1427: 521-525.","journal-title":"Lecture Notes in Computer Science"}],"container-title":["BMC Systems Biology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/1752-0509-3-42.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,9]],"date-time":"2025-02-09T06:00:18Z","timestamp":1739080818000},"score":1,"resource":{"primary":{"URL":"https:\/\/bmcsystbiol.biomedcentral.com\/articles\/10.1186\/1752-0509-3-42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,4,27]]},"references-count":55,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["310"],"URL":"https:\/\/doi.org\/10.1186\/1752-0509-3-42","relation":{},"ISSN":["1752-0509"],"issn-type":[{"value":"1752-0509","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,4,27]]},"assertion":[{"value":"18 August 2008","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 April 2009","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 April 2009","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"42"}}