Stochastic population models are widely used to model phenomena in different areas such as cyber-physical systems, chemical kinetics, collective animal behaviour, and beyond. Quantitative analysis of stochastic population models easily becomes challenging due to the combinatorial number of possible states of the population. Moreover, while the modeller easily hypothesises the mechanistic aspects of the model, the quantitative parameters associated to these mechanistic transitions are difficult or impossible to measure directly. In this paper, we investigate how formal verification methods can aid parameter inference for population discrete-time Markov chains in a scenario where only a limited sample of population-level data measurements-sample distributions among terminal states-are available. We first discuss the parameter identifiability and uncertainty quantification in this setup, as well as how the existing techniques of formal parameter synthesis and Bayesian inference apply. Then, we propose and implement four different methods, three of which incorporate formal parameter synthesis as a pre-computation step. We empirically evaluate the performance of the proposed methods over four representative case studies. We find that our proposed methods incorporating formal parameter synthesis as a pre-computation step allow us to significantly enhance the accuracy, precision, and scalability of inference. Specifically, in the case of unidentifiable parameters, we accurately capture the subspace of parameters which is data-compliant at a desired confidence level.

Centre for the Advanced Study of Collective Behaviour University of Konstanz Konstanz Germany

Department of Computer and Information Sciences University of Konstanz Konstanz Germany

Systems Biology Laboratory Faculty of Informatics Masaryk University Brno Czech Republic

See more in PubMed

Di Giamberardino P, Iacoviello D. Optimal Resource Allocation to Reduce an Epidemic Spread and Its Complication. Information. 2019;10:213. doi: 10.3390/info10060213 DOI

Dorigo M, Birattari M, Blum C, Clerc M, Stützle T, Winfield A. Ant Colony Optimization and Swarm Intelligence. vol. 5217. Springer; 2008.

Loreti M, Hillston J. Modelling and analysis of collective adaptive systems with CARMA and its tools. In: Formal Methods for the Design of Computer, Communication and Software Systems. Springer; 2016. p. 83–119.

Hillston J. Challenges for quantitative analysis of collective adaptive systems. In: International Symposium on Trustworthy Global Computing. Springer; 2013. p. 14–21.

Backenköhler M, Bortolussi L, Großmann G, Wolf V. Analysis of Markov Jump Processes under Terminal Constraints. arXiv preprint arXiv:201010096. 2020;.

Laurent M, Kellershohn N. Multistability: a major means of differentiation and evolution in biological systems. Trends in Biochemical Sciences. 1999;24(11):418–422. doi: 10.1016/S0968-0004(99)01473-5 PubMed DOI

Ghaffarizadeh A, Flann NS, Podgorski GJ. Multistable switches and their role in cellular differentiation networks. BMC bioinformatics. 2014;15(7):1–13. doi: 10.1186/1471-2105-15-S7-S7 PubMed DOI PMC

Eftimie R, Dushoff J, Bridle BW, Bramson JL, Earn DJ. Multi-stability and multi-instability phenomena in a mathematical model of tumor-immune-virus interactions. Bulletin of mathematical biology. 2011;73(12):2932–2961. doi: 10.1007/s11538-011-9653-5 PubMed DOI

Cillo AR, Somasundaram A, Shan F, Cardello C, Workman CJ, Kitsios GD, et al.. Bifurcated monocyte states are predictive of mortality in severe COVID-19. bioRxiv. 2021;. doi: 10.1101/2021.02.10.430499 PubMed DOI PMC

Tyson JJ, Csikasz-Nagy A, Novak B. The dynamics of cell cycle regulation. Bioessays. 2002;24(12):1095–1109. doi: 10.1002/bies.10191 PubMed DOI

Swat M, Kel A, Herzel H. Bifurcation analysis of the regulatory modules of the mammalian G1/S transition. Bioinformatics. 2004;20(10):1506–1511. doi: 10.1093/bioinformatics/bth110 PubMed DOI

Raue A, Karlsson J, Saccomani MP, Jirstrand M, Timmer J. Comparison of approaches for parameter identifiability analysis of biological systems. Bioinformatics. 2014;30:1440–1448. doi: 10.1093/bioinformatics/btu006 PubMed DOI

Schnoerr D, Sanguinetti G, Grima R. Approximation and inference methods for stochastic biochemical kinetics—a tutorial review. Journal of Physics A: Mathematical and Theoretical. 2017;50(9):093001. doi: 10.1088/1751-8121/aa54d9 DOI

Clarke EM, Henzinger TA, Veith H, Bloem R. Handbook of model checking. vol. 10. Springer; 2018.

Bartocci E, Lió P. Computational Modelling, Formal Analysis, and Tools for Systems Biology. PLoS Computational Biology. 2016;12:e1004591. doi: 10.1371/journal.pcbi.1004591 PubMed DOI PMC

Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of probabilistic real-time systems. In: International conference on computer aided verification. Springer; 2011. p. 585–591.

Dehnert C, Junges S, Katoen JP, Volk M. A STORM is coming: A modern probabilistic model checker. In: Computer Aided Verification. Springer; 2017. p. 592–600.

Daws C. Symbolic and parametric model checking of discrete-time Markov chains. In: International Colloquium on Theoretical Aspects of Computing. Springer; 2004. p. 280–294.

Jansen N, Corzilius F, Volk M, Wimmer R, Ábrahám E, Katoen JP, et al.. Accelerating parametric probabilistic verification. In: Quantitative Evaluation of Systems. Springer; 2014. p. 404–420.

Quatmann T, Dehnert C, Jansen N, Junges S, Katoen JP. Parameter synthesis for Markov models: Faster than ever. In: International Symposium on Automated Technology for Verification and Analysis. Springer; 2016. p. 50–67.

Katoen JP. The probabilistic model checking landscape. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. ACM; 2016. p. 31–45.

Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixão T, Petrov T. Model checking the evolution of gene regulatory networks. Acta Informatica. 2017;54(8):765–787. doi: 10.1007/s00236-016-0278-x DOI

Brim L, Češka M, Dražan S, Šafránek D. Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Computer Aided Verification. Springer; 2013. p. 107–123.

Češka M, Dannenberg F, Paoletti N, Kwiatkowska M, Brim L. Precise parameter synthesis for stochastic biochemical systems. Acta Informatica. 2017;54(6):589–623. doi: 10.1007/s00236-016-0265-2 DOI

Česka M, Šafránek D, Dražan S, Brim L. Robustness Analysis of Stochastic Biochemical Systems. PLOS ONE. 2014;9(4):1–23. doi: 10.1371/journal.pone.0094553 PubMed DOI PMC

Polgreen E, Wijesuriya VB, Haesaert S, Abate A. Data-efficient Bayesian verification of parametric Markov chains. In: International Conference on Quantitative Evaluation of Systems. Springer; 2016. p. 35–51.

Molyneux GW, Wijesuriya VB, Abate A. Bayesian verification of chemical reaction networks. In: International Symposium on Formal Methods. Springer; 2019. p. 461–479.

Hajnal M, Nouvian M, Šafránek D, Petrov T. Data-Informed Parameter Synthesis for Population Markov Chains. In: International Workshop on Hybrid Systems Biology. Springer; 2019. p. 147–164.

Petrov T, Hajnal M, Klein J, Šafránek D, Nouvian M. Extracting individual characteristics from population data reveals a negative social effect during honeybee defence. PLoS Computational Biology. 2022;18:e1010305. doi: 10.1371/journal.pcbi.1010305 PubMed DOI PMC

Dehnert C, Junges S, Jansen N, Corzilius F, Volk M, Bruintjes H, et al.. Prophesy: A probabilistic parameter synthesis tool. In: Computer Aided Verification. Springer; 2015. p. 214–231.

Hansson H, Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing. 1994;6(5):512–535. doi: 10.1007/BF01211866 DOI

Baier C, Katoen JP. Principles of Model Checking. Principles of Model Checking. MIT press; 2008.

Jean Dunn O. On multiple tests and confidence intervals. Communications in Statistics-Theory and Methods. 1974;3(1):101–103. doi: 10.1080/03610927408827108 DOI

Hajnal M, Šafránek D, Petrov T. DiPS: A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications. In: Performance Engineering and Stochastic Modeling. Cham: Springer International Publishing; 2021. p. 79–95.

May WL, Johnson WD. A SAS® macro for constructing simultaneous confidence intervals for multinomial proportions. Computer methods and Programs in Biomedicine. 1997;53(3):153–162. doi: 10.1016/S0169-2607(97)01809-9 PubMed DOI

Brown LD, Cai TT, DasGupta A. Interval Estimation for a Binomial Proportion. Statistical science. 2001; p. 101–117.

Dean N, Pagano M. Evaluating confidence interval methods for binomial proportions in clustered surveys. Journal of Survey Statistics and Methodology. 2015;3(4):484–503. doi: 10.1093/jssam/smv024 DOI

Hanley J, Lippman-Hand A. If nothing goes wrong, is everything all right? Interpreting zero numerators. JAMA. 1983;249 13:1743–5. doi: 10.1001/jama.1983.03330370053031 PubMed DOI

De Moura L, Bjørner N. Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer; 2008. p. 337–340.

Gao S, Kong S, Clarke EM. dReal: An SMT Solver for Nonlinear Theories over the Reals. In: CADE-24. vol. 7898 of LNCS. Springer; 2013. p. 208–214.

Metropolis N, Rosenbluth AW, Rosenbluth MN, Teller AH, Teller E. Equation of state calculations by fast computing machines. The journal of chemical physics. 1953;21(6):1087–1092. doi: 10.1063/1.1699114 DOI

Del Moral P, Doucet A, Jasra A. Sequential Monte Carlo samplers. Journal of the Royal Statistical Society: Series B (Statistical Methodology). 2006;68(3):411–436. doi: 10.1111/j.1467-9868.2006.00553.x DOI

Toni T, Welch D, Strelkowa N, Ipsen A, Stumpf MP. Approximate Bayesian computation scheme for parameter inference and model selection in dynamical systems. Journal of the Royal Society Interface. 2009;6(31):187–202. doi: 10.1098/rsif.2008.0172 PubMed DOI PMC

Sadegh M, Vrugt JA. Approximate bayesian computation using Markov chain Monte Carlo simulation: DREAM (ABC). Water Resources Research. 2014;50(8):6767–6787. doi: 10.1002/2014WR015386 DOI

Plagnol V, Tavaré S. Approximate Bayesian computation and MCMC. In: Monte Carlo and Quasi-Monte Carlo Methods 2002. Springer; 2004. p. 99–113.

Sisson SA, Fan Y, Tanaka MM. Sequential monte carlo without likelihoods. Proceedings of the National Academy of Sciences. 2007;104(6):1760–1765. doi: 10.1073/pnas.0607208104 PubMed DOI PMC

Molyneux GW, Abate A. ABC (SMC)2: Simultaneous Inference and Model Checking of Chemical Reaction Networks. In: International Conference on Computational Methods in Systems Biology. Springer; 2020. p. 255–279.

Silk D, Filippi S, Stumpf MP. Optimizing threshold-schedules for approximate Bayesian computation sequential Monte Carlo samplers: applications to molecular systems. arXiv preprint arXiv:12103296. 2012;.

Nouvian M, Reinhard J, Giurfa M. The defensive response of the honeybee Apis mellifera. J Exp Biol. 2016;219(22):3505–3517. doi: 10.1242/jeb.143016 PubMed DOI

Kermack WO, McKendrick AG. A contribution to the mathematical theory of epidemics. Proceedings of the royal society of london Series A, Containing papers of a mathematical and physical character. 1927;115(772):700–721.

Kulkarni VG. Introduction to Modeling and Analysis of Stochastic Systems. Springer Texts in Statistics. New York, NY: Springer New York; 2011. Available from: https://link.springer.com/10.1007/978-1-4419-1772-0. DOI

Wacker B, Schlüter J. Time-Continuous and Time-Discrete SIR Models Revisited: Theory and Applications. Advances in Difference Equations. 2020;556. doi: 10.1186/s13662-020-02995-1 PubMed DOI PMC

Dynamic Configuration of IPv4 Link-Local Addresses. https://tools.ietf.org/html/rfc3927.

Bortolussi L, Hillston J, Latella D, Massink M. Continuous approximation of collective system behaviour: A tutorial. Performance Evaluation. 2013;70(5):317–349. doi: 10.1016/j.peva.2013.01.001 DOI

Bortolussi L, Cardelli L, Kwiatkowska M, Laurenti L. Approximation of probabilistic reachability for chemical reaction networks using the linear noise approximation. In: QEST. Springer; 2016. p. 72–88.

Hansen LP. Large sample properties of generalized method of moments estimators. Econometrica. 1982; p. 1029–1054. doi: 10.2307/1912775 DOI

Backenkohler M, Bortolussi L, Wolf V. Moment-Based Parameter Estimation for Stochastic Reaction Networks in Equilibrium. IEEE/ACM Transactions on Computational Biology and Bioinformatics. 2018;15(4):1180–1192. doi: 10.1109/TCBB.2017.2775219 PubMed DOI

Backenköhler M, Bortolussi L, Wolf V. Generalized method of moments for stochastic reaction networks in equilibrium. In: Computational Methods in Systems Biology. Springer; 2016. p. 15–29.

Bortolussi L, Sanguinetti G. Learning and Designing Stochastic Processes from Logical Constraints. In: Quantitative Evaluation of Systems. Springer; 2013. p. 89–105.

Bartocci E, Bortolussi L, Nenzi L, Sanguinetti G. System design of stochastic models using robustness of temporal properties. Theoretical Computer Science. 2015;587:3–25. doi: 10.1016/j.tcs.2015.02.046 DOI