Abstract
We consider the problem of refining a parameter set to ensure that the behaviors of a dynamical system satisfy a given property. The dynamics are defined through parametric polynomial difference equations and their Bernstein representations are exploited to enclose reachable sets into parallelotopes. This allows us to achieve more accurate reachable set approximations with respect to previous works based on axis-aligned boxes. Moreover, we introduce a symbolical precomputation that leads to a significant improvement on time performances. Finally, we apply our framework to some epidemic models verifying the strength of the proposed method.
This work is partially supported by Istituto Nazionale di Alta Matematica (INdAM) and the project MALTHY (ANR-13-INSE-003).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Dreossi, T., Dang, T.: Parameter synthesis for polynomial biological models. In: HSCC 2014, New York, NY, USA, pp. 233–242. ACM (2014)
Dang, T., Testylier, R.: Reachability analysis for polynomial dynamical systems using the Bernstein expansion. Reliable Comput. 17(2), 128–152 (2012)
Ben Sassi, M.A., Testylier, R., Dang, T., Girard, A.: Reachability analysis of polynomial systems using linear programming relaxations. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 137–151. Springer, Heidelberg (2012)
Testylier, R., Dang, T.: Analysis of parametric biological models with non-linear dynamics. In: International Workshop on Hybrid Systems and Biology HSB, EPTCS, vol. 92, pp. 16–29 (2012)
Garloff, J., Smith, A.: Rigorous affine lower bound functions for multivariate polynomials and their use in global optimisation. In: Proceedings of the 1st International Conference on Applied Operational Research. Lecture Notes in Management Science, vol. 1, pp. 199–211 (2008)
Barnat, J., Brim, L., Krejci, A., Streck, A., Safranek, D., Vejnar, M., Vejpustek, T.: On parameter synthesis by parallel model checking. IEEE/ACM Trans. Comput. Biol. Bioinform. 9(3), 693–705 (2012)
Jha, S.K., Langmead, C.J.: Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement. Theor. Comput. Sci. 412(21), 2162–2187 (2011)
Bartocci, E., Bortolussi, L., Nenzi, L.: On the robustness of temporal properties for stochastic models. In: HSB 2013, EPTCS, vol. 125 (2013)
Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396–411. Springer, Heidelberg (2011)
Dreossi, T., Dang, T.: Falsifying oscillation properties of parametric biological models. In: HSB 2013, EPTCS, vol. 125, pp. 53–67 (2013)
Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010)
Donzé, A., Clermont, G., Langmead, C.J.: Parameter synthesis in nonlinear dynamical systems: application to systems biology. J. Comput. Biol. 17(3), 325–336 (2010)
Garloff, J., Smith, A.P.: A comparison of methods for the computation of affine lower bound functions for polynomials. In: Jermann, C., Neumaier, A., Sam, D. (eds.) COCOS 2003. LNCS, vol. 3478, pp. 71–85. Springer, Heidelberg (2005)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)
Organization, W.H.: Pandemic (h1n1) 2009 - update 103, June 2010. http://www.who.int/csr/don/2010_06_04/en/
Organization, W.H.: Summary of probable sars cases with onset of illness from 1 November 2002 to 31 July 2003, December 2013. http://www.who.int/csr/sars/country/table2004_04_21/en/
Kermack, W., McKendrick, A.: A contribution to the mathematical theory of epidemics. Proc. Roy. Soc. Lond.: Ser. A, Phys. Math. Sci. 115, 700–721 (1927)
Gumel, A., Ruan, S., Day, T., Watmough, J., Brauer, F., Driessche, V., Gabrielson, D., Bowman, C., Alexander, M., Ardal, S., et al.: Modelling strategies for controlling sars outbreaks. Proc. Roy. Soc. Lond. Ser. B: Biol. Sci. 271(1554), 2223–2232 (2004)
Parra, P.A.G., Lee, S., Velzquez, L., Castillo-Chavez, C.: A note on the use of optimal control on a discrete time model of influenza dynamics. Math. Biosci. Eng. 8(1), 183–197 (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Dang, T., Dreossi, T., Piazza, C. (2015). Parameter Synthesis Using Parallelotopic Enclosure and Applications to Epidemic Models. In: Maler, O., Halász, Á., Dang, T., Piazza, C. (eds) Hybrid Systems Biology. HSB 2014. Lecture Notes in Computer Science(), vol 7699. Springer, Cham. https://doi.org/10.1007/978-3-319-27656-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-27656-4_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-27655-7
Online ISBN: 978-3-319-27656-4
eBook Packages: Computer ScienceComputer Science (R0)