Automatic validation of computational models using pseudo-3D spatio-temporal model checking

BMC Systems Biology

David Gilbert¹  Ovidiu Pârvu¹ 

[1]Department of Computer Science, Brunel University, Kingston Lane, Uxbridge UB8 3PH, London, UK

关键词: Synthetic biology;    Systems biology;    Model validation;    Computational model;    Mudi;    Model checking;    Multidimensional;    Spatio-temporal;    Probabilistic bounded linear spatial temporal logic (PBLSTL);    Stochastic spatial discrete event system (SSpDES);   

Others  :  1091454
DOI  :  10.1186/s12918-014-0124-0

 received in 2014-07-23, accepted in 2014-10-28,  发布年份 2014

【 摘 要 】

Background

Computational models play an increasingly important role in systems biology for generating predictions and in synthetic biology as executable prototypes/designs. For real life (clinical) applications there is a need to scale up and build more complex spatio-temporal multiscale models; these could enable investigating how changes at small scales reflect at large scales and viceversa. Results generated by computational models can be applied to real life applications only if the models have been validated first. Traditional in silico model checking techniques only capture how non-dimensional properties (e.g. concentrations) evolve over time and are suitable for small scale systems (e.g. metabolic pathways). The validation of larger scale systems (e.g. multicellular populations) additionally requires capturing how spatial patterns and their properties change over time, which are not considered by traditional non-spatial approaches.

Results

We developed and implemented a methodology for the automatic validation of computational models with respect to both their spatial and temporal properties. Stochastic biological systems are represented by abstract models which assume a linear structure of time and a pseudo-3D representation of space (2D space plus a density measure). Time series data generated by such models is provided as input to parameterised image processing modules which automatically detect and analyse spatial patterns (e.g. cell) and clusters of such patterns (e.g. cellular population). For capturing how spatial and numeric properties change over time the Probabilistic Bounded Linear Spatial Temporal Logic is introduced. Given a collection of time series data and a formal spatio-temporal specification the model checker Mudi (http://mudi.modelchecking.org webcite) determines probabilistically if the formal specification holds for the computational model or not. Mudi is an approximate probabilistic model checking platform which enables users to choose between frequentist and Bayesian, estimate and statistical hypothesis testing based validation approaches. We illustrate the expressivity and efficiency of our approach based on two biological case studies namely phase variation patterning in bacterial colony growth and the chemotactic aggregation of cells.

Conclusions

The formal methodology implemented in Mudi enables the validation of computational models against spatio-temporal logic properties and is a precursor to the development and validation of more complex multidimensional and multiscale models.

【 授权许可】

   
2014 Pârvu and Gilbert; licensee BioMed Central Ltd.

【 图 表 】

Figure 1.

Figure 2.

Figure 3.

Figure 4.

Figure 6.

Figure 7.

Figure 8.

【 参考文献 】

• [1]Ideker T, Galitski T, Hood L: A new approach to decoding life: systems biology. Annu Rev Genomics Hum Genet 2001, 2(1):343-372. PMID: 11701654
• [2]Kitano H: Systems biology: a brief overview. Science 2002, 295(5560):1662-1664. PMID: 11872829
• [3]Benner SA, Sismour AM: Synthetic biology. Nat Rev Genet 2005, 6(7):533-543.
• [4]Endy D: Foundations for engineering biology. Nature 2005, 438(7067):449-453.
• [5]Cvijovic M, Almquist J, Hagmar J, Hohmann S, Kaltenbach H-M, Klipp E, Krantz M, Mendes P, Nelander S, Nielsen J, Pagnani A, Przulj N, Raue A, Stelling J, Stoma S, Tobin F, Wodke JAH, Zecchina R, Jirstrand M: Bridging the gaps in systems biology. Mol Genet Genom 2014, 289:727-734.
• [6]Dada JO, Mendes P: Multi-scale modelling and simulation in systems biology. Integr Biol (Camb) 2011, 3(2):86-96.
• [7]Weber W, Fussenegger M: Emerging biomedical applications of synthetic biology. Nat Rev Genet 2012, 13(1):21-35. Accessed 2014-04-08
• [8]Kohl P, Noble D: Systems biology and the virtual physiological human. Mol Syst Biol 2009, 5:292. WOS:000268718900008
• [9]Kurachi Y: High Definition Physiology project. [http://hd-physiology.jp/] Accessed 2014-04-07.
• [10]Cheng AA, Lu TK: Synthetic biology: an emerging engineering discipline. Annu Rev Biomed Eng 2012, 14:155-178. PMID: 22577777
• [11]Clarke EM, Grumberg O, Peled D: Model Checking. MIT Press, Cambridge; 1999.
• [12]Baier C, Katoen J-P: Principles of Model Checking. The MIT Press, Cambridge, London, England; 2008.
• [13]Emerson EA: Temporal and modal logic. In Handbook of Theoretical Computer Science. Edited by Jan van Leeuwen. MIT Press, Cambridge; 1995:995-1072.
• [14]Konur S. A survey on temporal logics. arXiv e-print 1005.3199, Department of Computer Science, University of Liverpool May 2010. [http://arxiv.org/abs/1005.3199] Accessed 2013-07-03.
• [15]Finkbeiner B, Sipma H: Checking finite traces using alternating automata. Electron Notes Theor Comput Sci 2001, 55(2):147-163. Accessed 2013-11-13
• [16]Pnueli A: The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science: 31 October-2 November 1977; Providence, RI, USA. IEEE, New York; 1977:46-57.
• [17]Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P: A bayesian approach to model checking biological systems. In Computational Methods in Systems Biology. Lecture Notes in Computer Science. Edited by Degano P, Gorrieri R. Springer, Bologna; 2009:218-234. [http://link.springer.com/chapter/10.1007/978-3-642-03845-7_15] Accessed 2013-11-05
• [18]Zuliani P, Platzer A, Clarke EM: Bayesian statistical model checking with application to Simulink/Stateflow verification. In Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control. HSCC ‘10. ACM, New York; 2010:243-252. [http://doi.acm.org/10.1145/1755952.1755987] Accessed 2013-11-05
• [19]Chabrier N, Fages F: Symbolic model checking of biochemical networks. In Computational Methods in Systems Biology. Lecture Notes in Computer Science. Edited by Priami C. Springer, Rovereto; 2003:149-162. [http://link.springer.com/chapter/10.1007/3-540-36481-1_13] Accessed 2014-04-14
• [20]Kwiatkowska M, Norman G, Parker D: Using probabilistic model checking in systems biology. SIGMETRICS Perform Eval Rev 2008, 35(4):14-21. Accessed 2014-04-14
• [21]Barbuti R, Levi F, Milazzo P, Scatena G: Probabilistic model checking of biological systems with uncertain kinetic rates. Theor Comput Sci 2012, 419:2-16. Accessed 2014-04-14
• [22]Barnat J, Brim L, Sǎfránek D, Vejnár M: Parameter scanning by parallel model checking with applications in systems biology. In Second International Workshop on Parallel and Distributed Methods in Verification, 2010 Ninth International Workshop On, and High Performance Computational Systems Biology: 30 September-1 October 2010; Enschede. IEEE, New York; 2010:95-104.
• [23]Jha SK, Langmead CJ: Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement. Theor Comput Sci 2011, 412(21):2162-2187. Accessed 2014-04-15
• [24]Rizk A, Batt G, Fages F, Soliman S: Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures. Theor Comput Sci 2011, 412(26):2827-2839. Accessed 2014-09-23
• [25]Madsen C, Myers C, Roehner N, Winstead C, Zhang Z: Utilizing stochastic model checking to analyze genetic circuits. In 2012 IEEE Symposium on Computational Intelligence in Bioinformatics and Computational Biology (CIBCB): 9-12 May 2012. IEEE, San Diego, CA, New York; 2012:379-386.
• [26]Rizk A, Batt G, Fages F, Soliman S: A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 2009, 25(12):169-178. Accessed 2014-09-23
• [27]Yordanov B, Belta C: A formal verification approach to the design of synthetic gene networks. CoRR2011abs/1109.1275. arXiv:1109.1275 [cs, math, q-bio], 2011. Accessed 2014-04-14.
• [28]Brim L, Češka M, Šafránek D: Model checking of biological systems. In Formal Methods for Dynamical Systems. Lecture Notes in Computer Science. Edited by Bernardo M, Vink Ed, Pierro AD, Wiklicky H. Springer, Bertinoro; 2013:63-112. [http://link.springer.com/chapter/10.1007/978-3-642-38874-3_3] Accessed 2014-01-08
• [29]Zuliani P: Statistical model checking for biological applications. CoRR2014,abs/1405.2705. arXiv:1405.2705 [cs, q-bio], 2014. Accessed 2014-05-17.
• [30]Heiner M, Rohr C, Schwarick M: MARCIE – model checking and reachability analysis done efficiently. In Application and Theory of Petri Nets and Concurrency. Lecture Notes in Computer Science. Edited by Colom J-M, Desel J. Springer, Milano; 2013:389-399. [http://link.springer.com/chapter/10.1007/978-3-642-38697-8_21] Accessed 2014-04-14
• [31]Kwiatkowska M, Norman G, Parker D: PRISM 4.0: Verification of probabilistic real-time systems. In Computer Aided Verification. Lecture Notes in Computer Science. Edited by Gopalakrishnan G, Qadeer S. Springer, Snowbird; 2011:585-591. [http://link.springer.com/chapter/10.1007/978-3-642-22110-1_47] Accessed 2014-04-14
• [32]Appelmelk BJ, Shiberu B, Trinks C, Tapsi N, Zheng PY, Verboom T, Maaskant J, Hokke CH, Schiphorst WECM, Blanchard D, Simoons-Smit IM, van den Eijnden DH, Vandenbroucke-Grauls CMJE: Phase variation in helicobacter pylori lipopolysaccharide. Infect Immun 1998, 66(1):70-76. Accessed 2013-06-12
• [33]Weijer C: Dictyostelium discoideum webpage. [http://www.personal.dundee.ac.uk/~cjweijer/dictyweb/] Accessed 2014-09-23.
• [34]Younes HLS: Verification and planning for stochastic processes with asynchronous events. Doctor of philosophy,Carnegie Mellon, Pittsburgh, 2005.
• [35]Pârvu O, Gilbert D, Heiner M, Liu F, Saunders N: Modelling and analysis of phase variation in bacterial colony growth. In Computational Methods in Systems Biology. Lecture Notes in Computer Science. Edited by Gupta A, Henzinger TA. Springer, Klosterneuburg; 2013:78-91. [http://link.springer.com/chapter/10.1007/978-3-642-40708-6_7] Accessed 2013-09-29
• [36]Saunders NJ, Moxon ER, Gravenor MB: Mutation rates: estimating phase variation rates when fitness differences are present and their impact on population structure. Microbiology 2003, 149(2):485-495. PMID: 12624210. Accessed 2013-06-11
• [37]Szeliski R: Computer Vision: Algorithms and Applications. Springer, New York; 2010.
• [38]Bradski G, Kaehler A: Learning OpenCV: Computer Vision with the OpenCV Library. O’Reilly, Cambridge; 2008.
• [39]Itseez: OpenCV documentation2013. [http://docs.opencv.org]
• [40]Jain AK: Data clustering: 50 years beyond k-means. Pattern Recogn Lett 2010, 31(8):651-666. Accessed 2013-07-24
• [41]Ester M, Xu X: Kriegel H-pS J: A Density-Based Algorithm for Discovering Clusters in Large Spatial Databases with Noise. AAAI Press, Menlo Park; 1996.
• [42]Tran TN, Drab K, Daszykowski M: Revised DBSCAN algorithm to cluster data with dense adjacent clusters. Chemometr Intell Lab Syst 2013, 120:92-96. Accessed 2013-07-04
• [43]O’Rourke J, Aggarwal A, Maddila S, Baldwin M: An optimal algorithm for finding minimal enclosing triangles. J Algorithm 1986, 7(2):258-269. Accessed 2013-07-09
• [44]Freeman H, Shapira R: Determining the minimum-area encasing rectangle for an arbitrary closed curve. Commun ACM 1975, 18(7):409-413. Accessed 2014-04-24
• [45]Toussaint GT: Solving geometric problems with the rotating calipers. In Proc. IEEE Melecon; 1983:10. [http://web.cs.swarthmore.edu/~adanner/cs97/s08/pdf/calipers.pdf] Accessed 2013-07-09.
• [46]Gärtner B: Fast and robust smallest enclosing balls. [http://link.springer.com/chapter/10.1007/3-540-48481-7_29] webciteIn Algorithms - ESA ‘99. Lecture Notes in Computer Science Edited by Nešetřil J. Springer, Prague; 1999, 325-338. [http://link.springer.com/chapter/10.1007/3-540-48481-7_29] Accessed 2014-04-24
• [47]Steger C: On the calculation of moments of polygons. Technical Report FGBV–96–04, Forschungsgruppe Bildverstehen (FG BV), Informatik IX, Technische Universität München, 1996.
• [48]Parvu O: Mudi. [http://mudi.modelchecking.org/home] Accessed 2014-07-21.
• [49]Hérault T, Lassaigne R, Magniette F, Peyronnet S: Approximate probabilistic model checking. In Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science. Edited by Steffen B, Levi G. Springer, Venice; 2004:73-84. [http://link.springer.com/chapter/10.1007/978-3-540-24622-0_8] Accessed 2013-10-27
• [50]Langmead C: Generalized queries and bayesian statistical model checking in dynamic bayesian networks: Application to personalized medicine. In Proceedings of the 8th International Conference on Computational Systems Bioinformatics (CSB): 10-12 August, 2009; California. Edited by Life Sciences Society; 2009:201–212.
• [51]Younes HL, Simmons RG: Statistical probabilistic model checking with a focus on time-bounded properties. Inform Comput 2006, 204(9):1368-1409. Accessed 2013-10-28
• [52]Sen K, Viswanathan M, Agha G: Statistical model checking of black-box probabilistic systems. In Computer Aided Verification. Lecture Notes in Computer Science. Edited by Alur R, Peled DA. Springer, Boston; 2004:202-215. [http://link.springer.com/chapter/10.1007/978-3-540-27813-9_16] Accessed 2014-04-21
• [53]Younes HLS: Probabilistic verification for “Black-Box” systems. In Computer Aided Verification. Lecture Notes in Computer Science. Edited by Etessami K, Rajamani SK. Springer, Edinburgh; 2005:253-265. [http://link.springer.com/chapter/10.1007/11513988_25] Accessed 2014-04-08
• [54]Koh CH, Palaniappan SK, Thiagarajan PS, Wong L: Improved statistical model checking methods for pathway analysis. BMC Bioinformatics2012, 15(Suppl 17). PMID: 23282174. Accessed 2013-10-31.
• [55]Jha S, Clarke E, Langmead C Legay, A, Platzer A, Zuliani P: Statistical model checking for complex stochastic models in systems biology. [http://repository.cmu.edu/cgi/viewcontent.cgi?article=2244&context=compsci]
• [56]Salaün L, Snyder LA, Saunders NJ: Adaptation by phase variation in pathogenic bacteria. Adv Appl Microbiol 2003, 52:263-301. PMID: 12964248
• [57]Salaün L, Ayraud S, Saunders NJ: Phase variation mediated niche adaptation during prolonged experimental murine infection with helicobacter pylori. Microbiology (Reading, England) 2005, 151(Pt 3):917-923. PMID: 15758236
• [58]Heiner M, Herajy M, Liu F, Rohr C, Schwarick M: Snoopy – a unifying petri net tool. [http://link.springer.com/chapter/10.1007/978-3-642-31131-4_22] webciteIn Application and Theory of Petri Nets. Lecture Notes in Computer Science Edited by Haddad S, Pomello L. Springer, Hamburg; 2012, 398-407. [http://link.springer.com/chapter/10.1007/978-3-642-31131-4_22] Accessed 2013-08-22
• [59]Cai H, Devreotes PN: Moving in the right direction: How eukaryotic cells migrate along chemical gradients. Semin Cell Dev Biol 2011, 22(8):834-841. Accessed 2014-06-03
• [60]Jin T: Gradient sensing during chemotaxis. Curr Opin Cell Biol 2013, 25(5):532-537. Accessed 2014-06-03
• [61]Jilkine A, Edelstein-Keshet L: A comparison of mathematical models for polarization of single eukaryotic cells in response to guided cues. PLoS Comput Biol 2011, 7(4):1001121. Accessed 2014-06-03
• [62]Starruß J, Back Wd, Brusch L, Deutsch A: Morpheus: a user-friendly modeling environment for multiscale and multicellular systems biology. Bioinformatics 2014, 30(9):1331-1332. PMID: 24443380. Accessed 2014-05-30
• [63]Graner F, Glazier JA: Simulation of biological cell sorting using a two-dimensional extended potts model. Phys Rev Lett 1992, 69(13):2013-2016. PMID: 10046374
• [64]Stoma S, Fröhlich M, Gerber S, Klipp E: STSE: spatio-temporal simulation environment dedicated to biology. BMC Bioinformatics 2011, 12(1):126. PMID: 21527030. Accessed 2013-03-10 BioMed Central Full Text
• [65]Jha S, Ramanathan A: Quantifying uncertainty in epidemiological models. In 2012 ASE/IEEE International Conference on BioMedical Computing (BioMedCom): 14-16 December 2012. IEEE, Washington, DC, New York; 2012:80-85.
• [66]Hussain F, Jha SK, Ramanathan A, Pullum LL: EpiSpec: A formal specification language for parameterized agent-based models against epidemiological ground truth. In 4th International Conference on Computational Advances in Bio and Medical Sciences (ICCABS): 2-4 June 2014; Miami, FL. IEEE, New York; 2014:1-6.
• [67]Rousseeuw PJ: Silhouettes: a graphical aid to the interpretation and validation of cluster analysis. J Comput Appl Math 1987, 20:53-65. Accessed 2013-07-24
• [68]Arbelaitz O, Gurrutxaga I, Muguerza J, Pérez JM, Perona I: An extensive comparative study of cluster validity indices. Pattern Recogn 2013, 46(1):243-256. Accessed 2013-07-23