Parameter Synthesis Using Parallelotopic Enclosure and Applications to Epidemic Models

  • Thao Dang
  • Tommaso DreossiEmail author
  • Carla Piazza
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7699)


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.


Parameter synthesis Polynomial systems Bernstein basis Symbolic computation Epidemic models 


  1. 1.
    Dreossi, T., Dang, T.: Parameter synthesis for polynomial biological models. In: HSCC 2014, New York, NY, USA, pp. 233–242. ACM (2014)Google Scholar
  2. 2.
    Dang, T., Testylier, R.: Reachability analysis for polynomial dynamical systems using the Bernstein expansion. Reliable Comput. 17(2), 128–152 (2012)MathSciNetGoogle Scholar
  3. 3.
    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) CrossRefGoogle Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Bartocci, E., Bortolussi, L., Nenzi, L.: On the robustness of temporal properties for stochastic models. In: HSB 2013, EPTCS, vol. 125 (2013)Google Scholar
  9. 9.
    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) CrossRefGoogle Scholar
  10. 10.
    Dreossi, T., Dang, T.: Falsifying oscillation properties of parametric biological models. In: HSB 2013, EPTCS, vol. 125, pp. 53–67 (2013)Google Scholar
  11. 11.
    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) CrossRefGoogle Scholar
  12. 12.
    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)MathSciNetCrossRefGoogle Scholar
  13. 13.
    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) CrossRefGoogle Scholar
  14. 14.
    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) CrossRefGoogle Scholar
  15. 15.
    Organization, W.H.: Pandemic (h1n1) 2009 - update 103, June 2010.
  16. 16.
    Organization, W.H.: Summary of probable sars cases with onset of illness from 1 November 2002 to 31 July 2003, December 2013.
  17. 17.
    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)CrossRefzbMATHGoogle Scholar
  18. 18.
    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)CrossRefGoogle Scholar
  19. 19.
    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)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.VERIMAGGieresFrance
  2. 2.Univerisity of UdineUdineItaly

Personalised recommendations