| [1] | Fisher J, Henzinger TA. Executable cell biology. Nat Biotechnol. 2007 Nov;25(11):1239–1249. pmid:17989686 doi: 10.1038/nbt1356
|
| [2] | Hunt CH, Ropella GEP, Park S, Engelberg J. Dichotomies between computational and mathematical models. Nature Biotechnology. 2008;26(7):737–738. doi: 10.1038/nbt0708-737. pmid:18612289
|
| [3] | Hlavacek WS, Faeder JR, Blinov ML, Posner RG, Hucka M, Fontana W. Rules for Modeling Signal-Transduction Systems. Sci STKE. 2006;2006(344):re6. pmid:16849649 doi: 10.1126/stke.3442006re6
|
| [4] | Fisher J, Harel D, Henzinger TA. Biology As Reactivity. Commun ACM. 2011 Oct;54(10):72–82. doi: 10.1145/2001269.2001289
|
| [5] | Fisher J, Piterman N. The executable pathway to biological networks. Brief Funct Genomics. 2010 Jan;9(1):79–92. doi: 10.1093/bfgp/elp054. pmid:20118126
|
| [6] | Kwiatkowska M, Norman G, Parker D. Probabilistic Model Checking for Systems Biology. In: Symbolic Systems Biology. Jones and Bartlett; 2010. p. 31–59.
|
| [7] | Gay S, Soliman S, Fages F. A graphical method for reducing and relating models in systems biology. Bioinformatics. 2010;26(18). doi: 10.1093/bioinformatics/btq388
|
| [8] | Hoops S, Sahle S, Gauges R, Lee C, Pahle J, Simus N, et al. COPASI—a COmplex PAthway SImulator. Bioinformatics. 2006 Dec;22(24):3067–3074. pmid:17032683 doi: 10.1093/bioinformatics/btl485
|
| [9] | Sahle S, Gauges R, Pahle J, Simus N, Kummer U, Hoops S, et al. Simulation of Biochemical Networks using Copasi—A Complex Pathway Simulator. In: Proc. of WSC 06: the Winter Simulation Conference. IEEE; 2006. p. 1698–1706.
|
| [10] | Priami C, Regev A, Shapiro E, Silverman W. Application of a stochastic name-passing calculus to representation and simulation of molecular processes. Information Processing Letters. 2001;80(1):25–31. doi: 10.1016/s0020-0190(01)00214-9
|
| [11] | Dematté L, Priami C, Romanel A. The BlenX Language: A Tutorial. In: Formal Methods for Computational Systems Biology 2008: 8th International School on Formal Methods for the Design of Computer, Communication, and Software Systems. vol. 5016 of LNCS. Springer-Verlag; 2008. p. 313–365.
|
| [12] | Dematté L, Priami C, Romanel A. The Beta Workbench: a computational tool to study the dynamics of biological systems. Brief Bioinform. 2008;9(5):437–449. doi: 10.1093/bib/bbn023. pmid:18463130
|
| [13] | Ciocchetta F, Hillston J. Bio-PEPA: A framework for the modelling and analysis of biological systems. Theoretical Computer Science. 2009;410(33–34):3065–3084. doi: 10.1016/j.tcs.2009.02.037
|
| [14] | Guerriero ML, Pokhilko A, Fernandez AP, Halliday KJ, Millar AJ, Hillston J. Stochastic properties of the plant circadian clock. J R Soc Interface. 2012 Apr;9(69):744–756. doi: 10.1098/rsif.2011.0378. pmid:21880617
|
| [15] | Phillips A, Cardelli L. Efficient, Correct Simulation of Biological Processes in the Stochastic Pi-calculus. In: Proc. of CMSB 2007: The 6th Conference on Computational Methods in Systems Biology. vol. 4695 of LNCS. Springer; 2007. p. 184–199.
|
| [16] | Wang DY, Cardelli L, Phillips A, Piterman N, Fisher J. Computational modeling of the EGFR network elucidates control mechanisms regulating signal dynamics. BMC Syst Biol. 2009;3:118. doi: 10.1186/1752-0509-3-118. pmid:20028552
|
| [17] | Dalchau N, Phillips A, Goldstein LD, Howarth M, Cardelli L, Emmott S, et al. A peptide filtering relation quantifies MHC class I peptide optimization. PLoS Comput Biol. 2011 Oct;7(10):e1002144. doi: 10.1371/journal.pcbi.1002144. pmid:22022238
|
| [18] | Bortolussi L, Policriti A. Modeling Biological Systems in Stochastic Concurrent Constraint Programming. Constraints. 2008;13(1–2):66–90. doi: 10.1007/s10601-007-9034-8
|
| [19] | Bartocci E, Corradini F, Di Berardini MR, Merelli E, Tesei L. Shape Calculus. A Spatial Mobile Calculus for 3D Shapes. Scientific Annals of Computer Science. 2010;20(1):2010. doi: 10.1016/j.entcs.2012.05.013
|
| [20] | Bartocci E, Cacciagrano DR, Di Berardini MR, Merelli E, Tesei L. Timed Operational Semantics and Well-Formedness of Shape Calculus. Scientific Annals of Computer Science. 2010;20(33):2010.
|
| [21] | Regev A, Panina EM, Silverman W, Cardelli L, Shapiro E. BioAmbients: an abstraction for biological compartments. Theoretical Computer Science. 2004;325(1):141–167. doi: 10.1016/j.tcs.2004.03.061
|
| [22] | Faeder JR, Blinov ML, Hlavacek WS. Rule-Based Modeling of Biochemical Systems with BioNetGen. Methods in Molecular Biology. 2009;500:113–167. doi: 10.1007/978-1-59745-525-1_5. pmid:19399430
|
| [23] | Fisher J, Harel D. On Statecharts for Biology. In: Symbolic Systems Biology: Theory and Methods. Jones & Bartlett Publishers; 2010.
|
| [24] | Bortolussi L, Policriti A. Hybrid Systems and Biology. In: Formal Methods for Computational Systems Biology. vol. 5016 of LNCS. Springer; 2008. p. 424–448.
|
| [25] | Kauffman S. Metabolic stability and epigenesis in randomly constructed genetic nets. J Theor Biology. 1969 Mar;22:437–467. doi: 10.1016/0022-5193(69)90015-0
|
| [26] | Heiner M, Herajy M, Liu F, Rohr C, Schwarick M. Snoopy—A Unifying Petri Net Tool. In: Proc. of Petri Nets 2012: the 33rd International Conference on Application and Theory of Petri Nets. vol. 7347 of LNCS. Springer; 2012. p. 398–407.
|
| [27] | Richmond P, Walker DC, Coakley S, Romano DM. High performance cellular level agent-based simulation with FLAME for the GPU. Briefings in Bioinformatics. 2010;11(3):334–347. doi: 10.1093/bib/bbp073. pmid:20123941
|
| [28] | North MJ, Collier NT, Vos JR. Experiences creating three implementations of the REPAST agent modeling toolkit. ACM Trans Model Comput Simul. 2006 Jan;16(1):1–25. doi: 10.1145/1122012.1122013
|
| [29] | John M, Lhoussaine C, Niehren J, Versari C. Biochemical Reaction Rules with Constraints. In: Proc. of ESOP 2011: the 20th European Symposium on Programming. vol. 6602 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2011. p. 338–357.
|
| [30] | Chabrier-Rivier N, Fages F, Soliman S. The Biochemical Abstract Machine BIOCHAM. In: Proc. of CMSB 2005: the 3rd International Conference on Computational Methods in Systems Biology. vol. 3082 of LNCS. Springer; 2005. p. 172–191.
|
| [31] | Heitzler D, Durand G, Gallay N, Rizk A, Ahn S, Kim J, et al. Competing G protein-coupled receptor kinases balance G protein and β-arrestin signaling. Mol Syst Biol. 2012;8:590. doi: 10.1038/msb.2012.22. pmid:22735336
|
| [32] | Danos V, Feret J, Fontana W, Harmer R, Krivine J. Rule-Based Modelling of Cellular Signalling. In: Proc. of CONCUR 2007: 18th International Conference on Concurrency Theory. vol. 4703 of LNCS. Springer Berlin Heidelberg; 2007. p. 17–41.
|
| [33] | Clarke EM, Faeder JR, Langmead CJ, Harris LA, Jha SK, Legay A. Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway. In: Proc. of CMSB 2008: the 6th International Conference on Computational Methods in Systems Biology. vol. 5307 of LNCS. Springer; 2008. p. 231–250.
|
| [34] | Chabrier-Rivier N, Chiaverini M, Danos V, Fages F, Sch？chter V. Modeling and querying biomolecular interaction networks. Theor Comput Sci. 2004;325(1):25–44. doi: 10.1016/j.tcs.2004.03.063
|
| [35] | Gong H, Zuliani P, Komuravelli A, Faeder JR, Clarke EM. Analysis and verification of the HMGB1 signaling pathway. BMC Bioinformatics. 2010;11 Suppl 7:S10. doi: 10.1186/1471-2105-11-S7-S10. pmid:21106117
|
| [36] | Feret J, Danos V, Krivine J, Harmer R, Fontana W. Internal coarse-graining of molecular systems. Proceedings of the National Academy of Sciences. 2009;106(16):6453–6458. doi: 10.1073/pnas.0809908106
|
| [37] | Petri CA, Reisig W. Petri net. Scholarpedia. 2008;3(4):6477. doi: 10.4249/scholarpedia.6477
|
| [38] | Cordero F, Horváth A, Manini D, Napione L, Pierro MD, Pavan S, et al. Simplification of a complex signal transduction model using invariants and flow equivalent servers. Theor Comput Sci. 2011;412(43):6036–6057. doi: 10.1016/j.tcs.2011.06.013
|
| [39] | Koch I, Junker BH, Heiner M. Application of Petri Net theory for modelling and validation of the sucrose breakdown pathway in the potato tuber. Bioinformatics. 2005;21(7):1219–1226. pmid:15546934 doi: 10.1093/bioinformatics/bti145
|
| [40] | Bl？tke MA, Heiner M, Marwan W. Predicting Phenotype from Genotype through Automatically Composed Petri Nets. In: Proc. of CMSB 2012: the 10th International Conference on Computational Methods in Systems Biology. vol. 7605 of LNCS; 2012. p. 87–106.
|
| [41] | Heiner M, Gilbert D, Donaldson R. Petri Nets for Systems and Synthetic Biology. In: Formal Methods for Computational Systems Biology 2008: 8th International School on Formal Methods for the Design of Computer, Communication, and Software Systems. No. 5016 in Lecture Notes in Computer Science. Springer; 2008. p. 215–264.
|
| [42] | Heiner M, Rohr C, Schwarick M. MARCIE—Model Checking and Reachability Analysis Done Efficiently. In: Application and Theory of Petri Nets and Concurrency. vol. 7927 of LNCS. Springer Berlin Heidelberg; 2013. p. 389–399.
|
| [43] | Baarir S, Beccuti M, Cerotti D, De Pierro M, Donatelli S, Franceschinis G. The GreatSPN tool: recent enhancements. SIGMETRICS Perform Eval Rev. 2009;36(4):4–9. doi: 10.1145/1530873.1530876
|
| [44] | Napione L, Manini D, Cordero F, Horváth A, Picco A, Pierro M, et al. On the Use of Stochastic Petri Nets in the Analysis of Signal Transduction Pathways for Angiogenesis Process. In: Proc. of CMSB 2009: the 7th Conference on Computational Methods in Systems Biology. vol. 5688 of LNCS; 2009. p. 281–295.
|
| [45] | Talcott C, Dill DL. The Pathway Logic Assistant. In: Proceedings of the Workshop Computational Methods in Systems Biology (CMSB); 2005. p. 228–239.
|
| [46] | Tiwari A, Talcott C, Knapp M, Lincoln P, Laderoute K. Analyzing Pathways using SAT-based Approaches. In: Proc. of AB 2007: the 2nd Intl. Conf. on Algebraic Biology. vol. 4545 of LNCS. Springer; 2007. p. 155–169.
|
| [47] | Thomas R, Kaufman M. Multistationarity, the basis of cell differentiation and memory. II. Logical analysis of regulatory networks in terms of feedback circuits. Chaos. 2001;11(1):180–195. pmid:12779452 doi: 10.1063/1.1349893
|
| [48] | Thomas R, Kaufman M. Multistationarity, the basis of cell differentiation and memory. I. Structural conditions of multistationarity and other nontrivial behavior. Chaos. 2001 Mar;11(1):170–179. pmid:12779451 doi: 10.1063/1.1350439
|
| [49] | Chaouiya C, Naldi A, Thieffry D. Logical modelling of gene regulatory networks with GINsim. Methods Mol Biol. 2012;804:463–479. doi: 10.1007/978-1-61779-361-5_23. pmid:22144167
|
| [50] | Naldi A, Carneiro J, Chaouiya C, Thieffry D. Diversity and plasticity of Th cell types predicted from regulatory network modelling. PLoS Comput Biol. 2010;6(9):e1000912. doi: 10.1371/journal.pcbi.1000912. pmid:20824124
|
| [51] | Grieco L, Calzone L, Bernard-Pierrot I, Radvanyi F, Kahn-Perles B, Thieffry D. Integrative modelling of the influence of MAPK network on cancer cell fate decision. PLoS Comput Biol. 2013 Oct;9(10):e1003286. doi: 10.1371/journal.pcbi.1003286. pmid:24250280
|
| [52] | Mussel C, Hopfensitz M, Kestler HA. BoolNet—an R package for generation, reconstruction and analysis of Boolean networks. Bioinformatics. 2010 May;26(10):1378–1380. doi: 10.1093/bioinformatics/btq124. pmid:20378558
|
| [53] | Dubrova E, Teslenko M. A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks. IEEE/ACM Transactions on Computational Biology and Bioinformatics. 2011;8(5):1393–1399. doi: 10.1109/TCBB.2010.20. pmid:21778527
|
| [54] | Davidich MI, Bornholdt S. Boolean Network Model Predicts Cell Cycle Sequence of Fission Yeast. PLoS ONE. 2008;3(2):e1672. doi: 10.1371/journal.pone.0001672. pmid:18301750
|
| [55] | Schaub MA, Henzinger TA, Fisher J. Qualitative networks: a symbolic approach to analyze biological signaling networks. BMC Syst Biol. 2007;1:4. pmid:17408511
|
| [56] | Benque D, Bourton S, Cockerton C, Cook B, Fisher J, Ishtiaq S, et al. BMA: Visual Tool for Modeling and Analyzing Biological Networks. In: Proc. of CAV 2012: the 24th International Conference on Computer Aided Verification. vol. 7358 of LNCS. Berlin, Heidelberg: Springer-Verlag; 2012. p. 686–692.
|
| [57] | Harel D. Statecharts: A Visual Formalism for Complex Systems. Sci Comput Program. 1987;8(3):231–274. doi: 10.1016/0167-6423(87)90035-9
|
| [58] | Harel D, Gery E. Executable object modeling with statecharts. Computer. 1997;30(7):31–42. doi: 10.1109/2.596624
|
| [59] | Kam N, Cohen IR, Harel D. The Immune System as a Reactive System: Modeling T-Cell Activation With Statecharts. In: Proc. HCC 2001: Human-Centric Computing Languages and Environments. IEEE Computer Society; 2001. p. 15–22. doi: 10.1109/hcc.2001.995228
|
| [60] | Alur R, Courcoubetis C, Henzinger TA, Ho PH. Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In: Hybrid Systems. vol. 736 of LNCS. Springer; 1993. p. 209–229.
|
| [61] | Bartocci E, Bortolussi L, Smolka SA. Hybrid Systems and Biology. Information and Computation. 2014;236:1–2. doi: 10.1016/j.ic.2014.01.008
|
| [62] | Fromentin J, Eveillard D, Roux O. Hybrid modeling of biological networks: mixing temporal and qualitative biological properties. BMC Syst Biol. 2010;4:79. doi: 10.1186/1752-0509-4-79. pmid:20525331
|
| [63] | Asarin E, Dang T, Girard A. Hybridization methods for the analysis of nonlinear systems. Acta Informatica. 2007;43(7):451–476. doi: 10.1007/s00236-006-0035-7
|
| [64] | Dang T, Maler O, Testylier R. Accurate hybridization of nonlinear systems. In: Proc. of HSCC 2010: the 13th ACM International Conference on Hybrid Systems: Computation and Control. ACM; 2010. p. 11–20.
|
| [65] | Dang T, Testylier R. Hybridization domain construction using curvature estimation. In: Proc. of HSCC 2011: the 14th International Conference on Hybrid Systems: computation and control. ACM; 2011. p. 123–132.
|
| [66] | Grosu R, Batt G, Fenton F, Glimm J, Le Guernic C, Smolka SA, et al. From Cardiac Cells to Genetic Regulatory Networks. In: Proc. of CAV 2011: the 14th International Conference on Computer Aided Verification. vol. 6806 of LNCS. Springer Berlin / Heidelberg; 2011. p. 396–411.
|
| [67] | Ghosh R, Tomlin C. Lateral Inhibition through Delta-Notch Signaling: A Piecewise Affine Hybrid Model. In: Proc. of HSCC 2001: the 4th International Workshop on Hybrid Systems: Computation and Control. vol. 2034 of LNCS. Springer; 2001. p. 232–246.
|
| [68] | Ghosh R, Tiwari A, Tomlin C. Automated Symbolic Reachability Analysis; with Application to Delta-Notch Signaling Automata. In: Proc. of HSCC 2003: the 6th International Workshop on Hybrid Systems: Computation and Control. vol. 2623 of LNCS. Springer; 2003. p. 233–248.
|
| [69] | Barnat J, Brim L, Cerná I, Drazan S, Fabriková J, Lánk J, et al. BioDiVinE: A Framework for Parallel Analysis of Biological Models. In: Proc. of COMPMOD 2009: the 2nd International Workshop on Computational Models for Cell Processes. vol. 6 of EPTCS; 2009. p. 31–45.
|
| [70] | Batt G, Belta C, Weiss R. Temporal Logic Analysis of Gene Networks under Parameter Uncertainty. IEEE Trans of Automatic Control. 2008;53:215–229. doi: 10.1109/tac.2007.911330
|
| [71] | Batt G, Yordanov B, Weiss R, Belta C. Robustness analysis and tuning of synthetic gene networks. Bioinformatics. 2007;23(18):2415–2422. pmid:17660209 doi: 10.1093/bioinformatics/btm362
|
| [72] | Bartocci E, Cherry EM, Glimm J, Grosu R, Smolka SA, Fenton FH. Toward real-time simulation of cardiac dynamics. In: Proc. of CMSB 2011: the 9th International Conference on Computational Methods in Systems Biology. ACM; 2011. p. 103–112.
|
| [73] | Bartocci E, Corradini F, Di Berardini MR, Entcheva E, Smolka SA, Grosu R. Modeling and simulation of cardiac tissue using hybrid I/O automata. Theoretical Computer Science. 2009;410(33–34):3149–3165. doi: 10.1016/j.tcs.2009.02.042
|
| [74] | Bartocci E, Corradini F, Entcheva E, Grosu R, Smolka S. CellExcite: an efficient simulation environment for excitable cells. BMC Bioinformatics. 2008;9(Suppl 2):S3. doi: 10.1186/1471-2105-9-S2-S3. pmid:18387205
|
| [75] | The MathWorks I. MATLAB; 2015. Natick, Massachusetts, United States.
|
| [76] | The MathWorks I. Simulink; 2015. Natick, Massachusetts, United States.
|
| [77] | Chen T, Diciolla M, Kwiatkowska MZ, Mereacre A. A simulink hybrid heart model for quantitative verification of cardiac pacemakers. In: Proc. of HSCC 2013: the 16th International Conference on Hybrid Systems: Computation and Control. ACM; 2013. p. 131–136.
|
| [78] | Brim L, Ceska M, Drazan S, Safránek D. Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking. In: Proc. of CAV 2013: the 25th International Conference on Computer Aided Verification 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings. vol. 8044 of LNCS. Springer; 2013. p. 107–123.
|
| [79] | Barnat J, Brim L, Krejci A, Streck A, Safránek D, Vejnar M, et al. On Parameter Synthesis by Parallel Model Checking. IEEE/ACM Trans Comput Biology Bioinform. 2012;9(3):693–705. doi: 10.1109/tcbb.2011.110
|
| [80] | Donzé A. Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. In: Proc. of CAV 2010: the 22nd International Conference on Computer Aided Verification. vol. 6174 of LNCS. Springer Berlin; 2010. p. 167–170.
|
| [81] | Mobilia N, Donzé A, Moulis JM, Fanchon E. A Model of the Cellular Iron Homeostasis Network Using Semi-Formal Methods for Parameter Space Exploration. In: Proc. of HSB 2012: First International Workshop on Hybrid Systems and Biology. vol. 92 of EPTCS; 2012. p. 42–57.
|
| [82] | Kong S, Gao S, Chen W, Clarke E. dReach: δ-Reachability Analysis for Hybrid Systems. In: Proc. of TACAS 2015: the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. vol. 9035. Springer Berlin Heidelberg; 2015. p. 200–205.
|
| [83] | Liu B, Kong S, Gao S, Zuliani P, Clarke EM. Parameter Synthesis for Cardiac Cell Hybrid Models Using δ-Decisions. In: Proc. of CMSB 2014: the 12th International Conference on Computational Methods in Systems Biology. vol. 8859 of LNCS; 2014. p. 99–113.
|
| [84] | Annapureddy YSR, Liu C, Fainekos GE, Sankaranarayanan S. S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In: Proc. of TACAS 2011: the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. vol. 6605 of LNCS. Springer; 2011. p. 254–257.
|
| [85] | Murthy A, Bartocci E, Fenton FH, Glimm J, Gray R, Smolka SA, et al. Curvature analysis of cardiac excitation wavefronts. In: Proceedings of the 9th International Conference on Computational Methods in Systems Biology. CMSB ‘11. New York, NY, USA: ACM; 2011. p. 151–160.
|
| [86] | Gol EA, Bartocci E, Belta C. A formal methods approach to pattern synthesis in reaction diffusion systems. In: Proc. of CDC 2014: the IEEE 53rd Annual Conference on Decision and Control; 2014. p. 108–113.
|
| [87] | Haghighi I, Jones A, Kong Z, Bartocci E, Grosu R, Belta C. SpaTeL: A Novel Spatial-temporal Logic and Its Applications to Networked Systems. In: Proc. of HSCC ‘15: the 18th International Conference on Hybrid Systems: Computation and Control. ACM; 2015. p. 189–198.
|
| [88] | Grosu R, Smolka SA, Corradini F, Wasilewska A, Entcheva E, Bartocci E. Learning and detecting emergent behavior in networks of cardiac myocytes. Communications of the ACM. 2009;52(3):97–105. doi: 10.1145/1467247.1467271
|
| [89] | Bartocci E, Singh R, von Stein FB, Amedome A, Caceres AJJ, Castillo J, et al. Teaching cardiac electrophysiology modeling to undergraduate students: laboratory exercises and GPU programming for the study of arrhythmias and spiral wave dynamics. Advances in Physiology Education. 2011;35(4):427–437. doi: 10.1152/advan.00034.2011. pmid:22139782
|
| [90] | Paun G, Rozenberg G. A guide to membrane computing. Theoretical Computer Science. 2002;287(1):73–100. Natural Computing. doi: 10.1016/s0304-3975(02)00136-6
|
| [91] | Regev A, Panina E, Silverman W, Cardelli L, Shapiro E. BioAmbients: an abstraction for biological compartments. Theoretical Computer Science. 2004;325(1):141–167. Computational Systems Biology. doi: 10.1016/j.tcs.2004.03.061
|
| [92] | Muganthan VA, Phillips A, Vigliotti MG. BAM: BioAmbient machine. In: Proc. of ACSD 2008: the 8th International Conference on Application of Concurrency to System Design. IEEE; 2008. p. 45–49.
|
| [93] | Pilegaard H, Nielson F, Nielson HR. Pathway analysis for BioAmbients. J Log Algebr Program. 2008;77(1–2):92–130. doi: 10.1016/j.jlap.2008.05.006
|
| [94] | Cardelli L. Brane Calculi. In: Proc. of CMSB 2004: the international Conference, Computational Methods in Systems Biology. vol. 3082 of LNCS. Springer; 2004. p. 257–278.
|
| [95] | Merelli E, Armano G, Cannata N, Corradini F, d’Inverno M, Doms A, et al. Agents in bioinformatics, computational and systems biology. Briefings in Bioinformatics. 2007;8(1):45–59. pmid:16772270 doi: 10.1093/bib/bbl014
|
| [96] | Bartocci E, Cacciagrano D, Cannata N, Corradini F, Merelli E, Milanesi L, et al. An agent-based multilayer architecture for bioinformatics grids. NanoBioscience, IEEE Transactions on. 2007;6(2):142–148. doi: 10.1109/tnb.2007.897492
|
| [97] | Burkitt M, Walker DC, Romano DM, Fazeli A. Modelling sperm behaviour in a 3D environment. In: Proc. of CMSB 2011: the 9th International Conference on Computational Methods in Systems Biology; 2011. p. 141–149.
|
| [98] | Paoletti N, Liò P, Merelli E, Viceconti M. Multilevel Computational Modeling and Quantitative Analysis of Bone Remodeling. IEEE/ACM Trans Comput Biology Bioinform. 2012;9(5):1366–1378. doi: 10.1109/tcbb.2012.51
|
| [99] | Deutsch A, Dormann S. Cellular Automaton Modeling of Biological Pattern Formation: Characterization, Applications, and Analysis. Genetic Programming and Evolvable Machines. 2007 Mar;8(1):105–106. doi: 10.1007/s10710-006-9021-7
|
| [100] | Bethe HA. Statistical Theory of Superlattices. Proceedings of the Royal Society of London Series A, Mathematical and Physical Sciences. 1935;150(871):552–575. doi: 10.1098/rspa.1935.0122
|
| [101] | Zaki MH, Tahar S, Bois G. Computing cancer software models of complex tissues and disease are yielding a better understanding of cancer and suggesting potential treatments. Nature. 2012;491:s62–s63.
|
| [102] | Scianna M, P L, editor. Cellular Potts Models: Multiscale Developments and Biological Applications. Chapman Hall/CRC Press; 2013.
|
| [103] | Izaguirre JA, Chaturvedi R, Huang C, Cickovski TM, Coffland J, Thomas GL, et al. COMPUCELL, a multi-model framework for simulation of morphogenesis. Bioinformatics. 2004;20(7):1129–1137. doi: 10.1093/bioinformatics/bth050
|
| [104] | Hester SD, Belmonte JM, Gens JS, Clendenon SG, Glazier JA. A Multi-cell, Multi-scale Model of Vertebrate Segmentation and Somite Formation. PLoS Comput Biol. 2011;7(10):e1002155. doi: 10.1371/journal.pcbi.1002155. pmid:21998560
|
| [105] | Menichetti G, Remondini D, Bianconi G. Correlations between weights and overlap in ensembles of weighted multiplex networks. Phys Rev E. 2014;90:062817. doi: 10.1103/physreve.90.062817
|
| [106] | Bartocci E, Corradini F, Merelli E, Tesei L. Detecting synchronisation of biological oscillators by model checking. Theoretical Computer Science. 2010;411(20):1999–2018. doi: 10.1016/j.tcs.2009.12.019
|
| [107] | Bartocci E, Liò P, Merelli E, Paoletti N. Multiple Verification in Complex Biological Systems: The Bone Remodelling Case Study. T Comp Sys Biology. 2012;14:53–76. doi: 10.1007/978-3-642-35524-0_3
|
| [108] | Calzone L, Fages F, Soliman S. BIOCHAM: an environment for modeling biological systems and formalizing experimental knowledge. Bioinformatics. 2006;22(14):1805–1807. pmid:16672256 doi: 10.1093/bioinformatics/btl172
|
| [109] | Batt G, Bergamini D, de Jong H, Garavel H, Mateescu R. Model Checking Genetic Regulatory Networks Using GNA and CADP. In: Proc. of SPIN 2004: the 11th International SPIN Workshop on Model Checking Software. vol. 2989 of LNCS; 2004. p. 158–163.
|
| [110] | Rizk A, Batt G, Fages F, Soliman S. Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures. Theoretical Computer Science. 2011;412(26):2827–2839. doi: 10.1016/j.tcs.2010.05.008
|
| [111] | Fainekos G, Pappas G. Robust Sampling for MITL Specifications. In: Proc. of FORMATS 2007: the 5th International Conference on Formal Modeling and Analysis of Timed Systems. vol. 4763 of LNCS. Springer; 2007. p. 147–162.
|
| [112] | Rizk A, Batt G, Fages F, Soliman S. On a Continuous Degree of Satisfaction of Temporal Logic Formulae with Applications to Systems Biology. In: Proceedings of the 6th International Conference on Computational Methods in Systems Biology. CMSB ‘08. Berlin, Heidelberg: Springer-Verlag; 2008. p. 251–268.
|
| [113] | Donzé A, Maler O. Robust Satisfaction of Temporal Logic over Real-Valued Signals. In: Proc. of FORMATS 2010: the 8th International Conference on Formal Modeling and Analysis of Timed Systems. vol. 6246 of LNCS. Springer; 2010. p. 92–106.
|
| [114] | Donzé A, Clermont G, Langmead CJ. Parameter Synthesis in Nonlinear Dynamical Systems: Application to Systems Biology. Journal of Computational Biology. 2010;17(3):325–336. doi: 10.1089/cmb.2009.0172. pmid:20377448
|
| [115] | Donzé A, Fanchon E, Gattepaille LM, Maler O, Tracqui P. Robustness analysis and behavior discrimination in enzymatic reaction networks. PLoS ONE. 2011;6(9):e24246. doi: 10.1371/journal.pone.0024246. pmid:21980344
|
| [116] | Bartocci E, Bortolussi L, Nenzi L, Sanguinetti G. System design of stochastic models using robustness of temporal properties. Theor Comput Sci. 2015;587:3–25. doi: 10.1016/j.tcs.2015.02.046
|
| [117] | Nielson F, Nielson HR, Priami C, Rosa D. Static Analysis for Systems Biology. In: Proc. of the Winter International Synposium on Information and Communication Technologies. WISICT ‘04. Trinity College Dublin; 2004. p. 1–6.
|
| [118] | Danos V, Feret J, Fontana W, Krivine J. Abstract interpretation of cellular signalling networks. In: Proc. of VMCAI’2008: the Ninth International Conference on Verification, Model Checking and Abstract Interpretation. vol. 4905 of LNCS. Springer, Berlin, Germany; 2008. p. 83–97.
|
| [119] | Feret J. Reachability Analysis of Biological Signalling Pathways by Abstract Interpretation. In: Proc. of ICCMSE’2007: the International Conference of Computational Methods in Sciences and Engineering. No. 963.(2) in American Institute of Physics Conference Proceedings. American Institute of Physics; 2007. p. 619–622.
|
| [120] | Pnueli A. The temporal logic of programs. Foundations of Computer Science, IEEE Annual Symposium on. 1977;0:46–57. doi: 10.1109/sfcs.1977.32
|
| [121] | Clarke EM, Emerson E. Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. of Logics of Programs, Workshop. vol. 131 of LNCS. Springer Berlin; 1982. p. 52–71.
|
| [122] | Hansson H, Jonsson B. A Logic for Reasoning about Time and Reliability. Formal Asp Comput. 1994;6(5):512–535. doi: 10.1007/bf01211866
|
| [123] | Aziz A, Sanwal K, Singhal V, Brayton R. Model-checking continuous-time Markov chains. ACM Trans Comput Logic. 2000 Jul;1(1):162–170. doi: 10.1145/343369.343402
|
| [124] | Batt G, Belta C, Weiss R. Model Checking Liveness Properties of Genetic Regulatory Networks. In: Proc. of TACAS 2007: the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. vol. 5016 of LNCS. Springer-Verlag; 2007. p. 323–338.
|
| [125] | Cook B, Fisher J, Krepska E, Piterman N. Proving Stabilization of Biological Systems. In: Proc. of VMCAI 2011: the 12th International Conference on Verification, Model Checking, and Abstract Interpretation. vol. 6538 of LNCS. Springer; 2011. p. 134–149.
|
| [126] | Clarke EM, Emerson EA, Sistla AP. Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specifications. ACM Trans Program Lang Syst. 1986;8(2):244–263. doi: 10.1145/5397.5399
|
| [127] | Emerson EA, Halpern JY. "Sometimes" and "Not Never" Revisited: On Branching Versus Linear Time Temporal Logic. J ACM. 1986;33(1):151–178. doi: 10.1145/4904.4999
|
| [128] | Alur R, Henzinger TA. Real-time Logics: Complexity and Expressiveness. In: LICS; 1990. p. 390–401.
|
| [129] | Alur R, Henzinger TA. A Really Temporal Logic. J ACM. 1994;41(1):181–204. doi: 10.1145/174644.174651
|
| [130] | Alur R, Feder T, Henzinger TA. The Benefits of Relaxing Punctuality. J ACM. 1996;43(1):116–146. doi: 10.1145/227595.227602
|
| [131] | Maler O, Nickovic D. Monitoring Temporal Properties of Continuous Signals. In: Proc. of FORMATS/FTRTFT 2004: joint International Conferences on Formal Modeling and Analysis of Timed Systmes and Formal Techniques in Real-Time and Fault-Tolerant Systems. vol. 3253 of LNCS; 2004. p. 152–166.
|
| [132] | Donzé A, Maler O, Bartocci E, Nickovic D, Grosu R, Smolka SA. On Temporal Logic and Signal Processing. In: Proc. of ATVA 2012, the 10th International Symposium on Automated Technology for Verification and Analysis. vol. 7561 of Lecture Notes in Computer Science. Springer; 2012. p. 92–106.
|
| [133] | Bartocci E, Bortolussi L, Sanguinetti S. Data-driven Statistical Learning of Temporal Logic Properties. In: Proc. of FORMATS 2014: the 12th International Conference on Formal Modeling and Analysis of Timed Systems. vol. 8711 of LNCS; 2014. p. 23–37.
|
| [134] | Bufo S, Bartocci E, Sanguinetti G, Borelli M, Lucangelo U, Bortolussi L. Temporal Logic Based Monitoring of Assisted Ventilation in Intensive Care Patients. In: Proc. of ISoLA 2014: the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Part II. vol. 8803 of Lecture Notes in Computer Science. Springer; 2014. p. 391–403.
|
| [135] | Bartocci E, Bortolussi L, Nenzi L. A Temporal Logic Approach to Modular Design of Synthetic Biological Circuits. In: Computational Methods in Systems Biology. vol. 8130 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2013. p. 164–177.
|
| [136] | Kripke S. Semantical Considerations on Modal Logic. Acta Philosophica Fennica. 1963;16:83–94. doi: 10.2307/2270922
|
| [137] | Cimatti A, Clarke EM, Giunchiglia F, Roveri M. NuSMV: A New Symbolic Model Checker. STTT. 2000;2(4):410–425. doi: 10.1007/s100090050046
|
| [138] | Nusser-Stein S, Beyer A, Rimann I, Adamczyk M, Piterman N, Hajnal A, et al. Cell-cycle regulation of NOTCH signaling during C. elegans vulval development. Mol Syst Biol. 2012;8:618. doi: 10.1038/msb.2012.51. pmid:23047528
|
| [139] | Garavel H, Lang F, Mateescu R, Serwe W. CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Proc. of TACAS 2011: the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. vol. 6605. Springer; 2011. p. 372–387.
|
| [140] | Bryant RE. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans Computers. 1986;35(8):677–691. doi: 10.1109/tc.1986.1676819
|
| [141] | Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ. Symbolic Model Checking: 1020 States and Beyond. Inf Comput. 1992;98(2):142–170. doi: 10.1016/0890-5401(92)90017-a
|
| [142] | Ahmad J, Bourdon J, Eveillard D, Fromentin J, Roux O, Sinoquet C. Temporal constraints of a gene regulatory network: Refining a qualitative simulation. Biosystems. 2009;98(3):149–159. doi: 10.1016/j.biosystems.2009.05.002. pmid:19446002
|
| [143] | Calder M, Vyshemirsky V, Gilbert D, Orton RJ. Analysis of Signalling Pathways Using Continuous Time Markov Chains. T Comp Sys Biology. 2006;4220:44–67. doi: 10.1007/11880646_3
|
| [144] | Heath J, Kwiatkowska M, Norman G, Parker D, Tymchyshyn O. Probabilistic model checking of complex biological pathways. Theoretical Computer Science. 2008;319(3):239–257. doi: 10.1016/j.tcs.2007.11.013
|
| [145] | Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P. A Bayesian Approach to Model Checking Biological Systems. In: Proc. of CMSB 2009: the 7th International Conference on Computational Methods in Systems Biology. vol. 5688 of Lecture Notes in Computer Science. Springer; 2009. p. 218–234.
|
| [146] | Zuliani P, Baier C, Clarke EM. Rare-event verification for stochastic hybrid systems. In: HSCC. ACM; 2012. p. 217–226.
|
| [147] | Antoniotti M, Policriti A, Ugel N, Mishra B. Model building and model checking for biochemical processes. Cell Biochemistry and Biophysics. 2003;38:271–286. doi: 10.1385/CBB:38:3:271. pmid:12794268
|
| [148] | Calzone L, Chabrier-Rivier N, Fages F, Soliman S. Machine learning biochemical networks from temporal logic properties. Transactions on Computational Systems Biology VI. 2006; p. 68–94.
|
| [149] | Sankaranarayanan S, Fainekos G. Simulating Insulin Infusion Pump Risks by In-Silico Modeling of the Insulin-Glucose Regulatory System. In: Proc. of CMSB 2012: the 10th Conference on Computational Methods in Systems Biology. vol. 7605 of LNCS; 2012. p. 322–341.
|
| [150] | Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL ‘77: the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. ACM; 1977. p. 238–252.
|
| [151] | Paulev L, Magnin M, Roux O. Static analysis of Biological Regulatory Networks dynamics using abstract interpretation. Math Struct in Comp Science. 2012;22:651–685. doi: 10.1017/s0960129511000739
|
| [152] | Fages F, Soliman S. Abstract interpretation and types for systems biology. Theor Comput Sci. 2008;403(1):52–70. doi: 10.1016/j.tcs.2008.04.024
|
| [153] | Bartocci E, Bortolussi L, Milios D., Nenzi L., Sanguinetti G. Studying Emergent Behaviours in Morphogenesis using Signal Spatio-Temporal Logic. In: Proc. of HSB 2015: the 4th International Workshop on Hybrid Systems Biology. vol. 9271 of LNCS. Springer; 2015. p. 156–172
|
| [154] | Bartocci E, Gao S, Smolka SA. Proc. of ISoLA 2014: the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Part II. In: Medical Cyber-Physical Systems—(Track Introduction). vol. 8803 of Lecture Notes in Computer Science. Springer; 2014. p. 353–355.
|
