×

zbMATH — the first resource for mathematics

Toward model selection by formal methods. (English) Zbl 1458.92035
Gupta, Ankit (ed.) et al., Proceedings of SASB 2018, the 9th international workshop on static analysis and systems biology, Freiburg, Germany, August 28, 2018. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 350, 57-71 (2020).
Summary: We address the problem of selecting a model from a list of potential models in the field of dynamical systems. The selection is based on model behaviour specified in temporal logic rather than time series. This provides more global constraints on the system dynamics. Not only to select one model but also to create an ordered structure, we propose the model ordering problem. We suggest and apply several ordering relations comparing models given property specification. To provide a formal method with global results for the proposed setting we employ and adapt model checking and parameter synthesis methods. To evaluate the method, we apply the proposed method to several qualitative models of regulatory networks.
For the entire collection see [Zbl 1448.92002].
MSC:
92C42 Systems biology, networks
Software:
NuSMV
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alon, U., An Introduction to Systems Biology: Design Principles of Biological Circuits, Mathematical and Computational Biology (2006), Chapman & Hall/CRC · Zbl 1141.92002
[2] Beneš, N.; Brim, L.; Demko, M.; Pastva, S.; Šafránek, D., Pithya: A parallel tool for parameter synthesis of piecewise multi-affine dynamical systems, (Majumdar, R.; Kunčak, V., CAV 2017. CAV 2017, LNCS, vol. 10426 (2017)), 591-598
[3] Brim, L.; Demko, M.; Češka, M.; Pastva, S.; Šafránek, D., Parameter synthesis by parallel coloured CTL model checking, (Roux, O.; Bourdon, J., CMSB 2015. CMSB 2015, LNBI, vol. 9308 (2015)), 251-263
[4] Brim, L.; Demko, M.; Pastva, S.; Šafránek, D., High-performance discrete bifurcation analysis for piecewise-affine dynamical systems, (Abate, A.; Šafránek, D., Hybrid Systems Biology 2015. Hybrid Systems Biology 2015, LNBI, vol. 9271 (2015)), 58-74 · Zbl 1412.92115
[5] Cimatti, A.; Clarke, E.; Giunchiglia, E.; Giunchiglia, F.; Pistore, M.; Roveri, M.; Sebastiani, R.; Tacchella, A., NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking, (Proc. International Conference on Computer-Aided Verification (CAV). Proc. International Conference on Computer-Aided Verification (CAV), LNCS, vol. 2404 (2002)) · Zbl 1010.68766
[6] Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M., Nusmv: A new symbolic model verifier, (International conference on computer aided verification (1999), Springer), 495-499 · Zbl 1046.68587
[7] Clarke, E. M.; Emerson, E. A., Design and synthesis of synchronization skeletons using branching time temporal logic, (Workshop on Logic of Programs (1981), Springer), 52-71
[8] Clarke, E. M.; Emerson, E. A.; Sistla, A. P., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst., 8, 244-263 (1986) · Zbl 0591.68027
[9] Fages, F.; Rizk, A., From model-checking to temporal logic constraint solving, (International Conference on Principles and Practice of Constraint Programming (2009), Springer), 319-334
[10] Fages, F.; Soliman, S., Formal cell biology in biocham, (SFM. SFM, LNCS, vol. 5016 (2008)), 54-80
[11] Hafner, M.; Koeppl, H.; Hasler, M.; Wagner, A., ‘Glocal’ robustness analysis and model discrimination for circadian oscillators, PLoS computational biology, 5, Article e1000534 pp. (2009)
[12] Kitano, H., Towards a theory of biological robustness, Molecular systems biology, 3, 137 (2007)
[13] McMillan, K. L., Symbolic model checking, (Symbolic Model Checking (1993), Springer), 25-60
[14] Naldi, A.; Hernandez, C.; Levy, N.; Stoll, G.; Monteiro, P. T.; Chaouiya, C.; Helikar, T.; Zinovyev, A.; Calzone, L.; Cohen-Boulakia, S.; Thieffry, D.; Paulevé, L., The CoLoMoTo Interactive Notebook: Accessible and Reproducible Computational Analyses for Qualitative Biological Networks (2018), bioRxiv
[15] Naldi, A.; Monteiro, P. T.; Müssel, C.; Kestler, H. A.; Thieffry, D.; Xenarios, I.; Saez-Rodriguez, J.; Helikar, T.; Chaouiya, C., Cooperative development of logical modelling standards and tools with colomoto, Bioinformatics, 31, 1154-1159 (2015)
[16] Rizk, A.; Batt, G.; Fages, F.; Soliman, S., A general computational method for robustness analysis with applications to synthetic gene networks, Bioinformatics, 25 (2009)
[17] Silk, D.; Kirk, P. D.; Barnes, C. P.; Toni, T.; Stumpf, M. P., Model selection in systems biology depends on experimental design, PLoS computational biology, 10, Article e1003650 pp. (2014)
[18] Toni, T.; Stumpf, M. P., Simulation-based model selection for dynamical systems in systems and population biology, Bioinformatics, 26, 104-110 (2009)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.