Skip to main content
SpringerLink
Log in

Guaranteed Error Bounds on Approximate Model Abstractions Through Reachability Analysis

  • Conference paper
  • First Online:
Quantitative Evaluation of Systems (QEST 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11024))

Included in the following conference series:

Abstract

It is well known that exact notions of model abstraction and reduction for dynamical systems may not be robust enough in practice because they are highly sensitive to the specific choice of parameters. In this paper we consider this problem for nonlinear ordinary differential equations (ODEs) with polynomial derivatives. We introduce approximate differential equivalence as a more permissive variant of a recently developed exact counterpart, allowing ODE variables to be related even when they are governed by nearby derivatives. We develop algorithms to (i) compute the largest approximate differential equivalence; (ii) construct an approximate quotient model from the original one via an appropriate parameter perturbation; and (iii) provide a formal certificate on the quality of the approximation as an error bound, computed as an over-approximation of the reachable set of the perturbed model. Finally, we apply approximate differential equivalences to study the effect of parametric tolerances in models of symmetric electric circuits.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abate, A., Brim, L., Češka, M., Kwiatkowska, M.: Adaptive aggregation of Markov chains: quantitative analysis of chemical reaction networks. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 195–213. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_12

    Chapter  Google Scholar 

  2. Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: HSCC, pp. 173–182 (2013)

    Google Scholar 

  3. Althoff, M.: An introduction to CORA 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (2015)

    Google Scholar 

  4. Arand, J.: In vivo control of CpG and non-CpG DNA methylation by DNA methyltransferases. PLoS Genet. 8(6), e1002750 (2012)

    Article  Google Scholar 

  5. Asarin, E., Dang, T., Girard, A.: Reachability analysis of nonlinear systems using conservative approximation. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 20–35. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36580-X_5

    Chapter  MATH  Google Scholar 

  6. Benvenuti, L., et al.: Reachability computation for hybrid systems with Ariadne. In: Proceedings of the 17th IFAC World Congress, vol. 41, no. 2, pp. 8960–8965 (2008)

    Google Scholar 

  7. Bogomolov, S., Frehse, G., Grosu, R., Ladan, H., Podelski, A., Wehrle, M.: A box-based distance between regions for guiding the reachability analysis of SpaceEx. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 479–494. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_35

    Chapter  Google Scholar 

  8. Boreale, M.: Algebra, coalgebra, and minimization in polynomial differential equations. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 71–87. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_5

    Chapter  MATH  Google Scholar 

  9. van Breugel, F., Worrell, J.: Towards quantitative verification of probabilistic transition systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 421–432. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-48224-5_35

    Chapter  Google Scholar 

  10. Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Maximal aggregation of polynomial dynamical systems. Proc. Natl. Acad. Sci. 114(38), 10029–10034 (2017)

    Article  Google Scholar 

  11. Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Symbolic computation of differential equivalences. In: POPL (2016)

    Google Scholar 

  12. Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_18

    Chapter  Google Scholar 

  13. Danos, V., Laneve, C.: Formal molecular biology. Theoret. Comput. Sci. 325(1), 69–110 (2004)

    Article  MathSciNet  Google Scholar 

  14. Donzé, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 174–189. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71493-4_16

    Chapter  Google Scholar 

  15. Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: EMSOFT, pp. 26:1–26:10. IEEE Press (2013)

    Google Scholar 

  16. Weinan, E., Li, T., Vanden-Eijnden, E.: Optimal partition and effective dynamics of complex networks. PNAS 105(23), 7907–7912 (2008)

    Article  MathSciNet  Google Scholar 

  17. Fan, C., Qi, B., Mitra, S., Viswanathan, M., Duggirala, P.S.: Automatic reachability analysis for nonlinear hybrid models with C2E2. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 531–538. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_29

    Chapter  Google Scholar 

  18. Girard, A., Pappas, G.: Approximate bisimulations for nonlinear dynamical systems. In: IEEE Conference on Decision and Control and European Control Conference (2005)

    Google Scholar 

  19. Iacobelli, G., Tribastone, M.: Lumpability of fluid models with heterogeneous agent types. In: DSN (2013)

    Google Scholar 

  20. Islam, M.A., et al.: Model-order reduction of ion channel dynamics using approximate bisimulation. Theor. Comput. Sci. 599, 34–46 (2015)

    Article  MathSciNet  Google Scholar 

  21. Iwasa, Y., Levin, S.A., Andreasen, V.: Aggregation in model ecosystems II. Approximate aggregation. Math. Med. Biol. 6(1), 1–23 (1989)

    Article  MathSciNet  Google Scholar 

  22. Kozlov, M., Tarasov, S., Khachiyan, L.: The polynomial solvability of convex quadratic programming. USSR Comput. Math. Math. Phys. 20(5), 223–228 (1980)

    Article  MathSciNet  Google Scholar 

  23. Kuo, J.C.W., Wei, J.: Lumping analysis in monomolecular reaction systems. Analysis of approximately lumpable system. Ind. Eng. Chem. Fund. 8(1), 124–133 (1969)

    Article  Google Scholar 

  24. Lal, R., Prabhakar, P.: Bounded error flowpipe computation of parameterized linear systems. In: EMSOFT, pp. 237–246 (2015)

    Google Scholar 

  25. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)

    Article  MathSciNet  Google Scholar 

  26. Li, G., Rabitz, H.: A general analysis of approximate lumping in chemical kinetics. Chem. Eng. Sci. 45(4), 977–1002 (1990)

    Article  Google Scholar 

  27. Majumdar, R., Zamani, M.: Approximately bisimilar symbolic models for digital control systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 362–377. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_28

    Chapter  Google Scholar 

  28. Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J. Satisfiability Boolean Model. Comput. 1, 209–236 (2007)

    MATH  Google Scholar 

  29. Pardalos, P.M., Vavasis, S.A.: Quadratic programming with one negative eigenvalue is NP-hard. J. Global Optim. 1(1), 15–22 (1991)

    Article  MathSciNet  Google Scholar 

  30. Pedersen, M., Plotkin, G.D.: A language for biochemical systems: design and formal specification. In: Priami, C., Breitling, R., Gilbert, D., Heiner, M., Uhrmacher, A.M. (eds.) Transactions on Computational Systems Biology XII. LNCS, vol. 5945, pp. 77–145. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11712-1_3. IEEE/ACM

    Chapter  Google Scholar 

  31. Rosenfeld, J., Friedman, E.G.: Design methodology for global resonant H-Tree clock distribution networks. IEEE Trans. VLSI Syst. 15(2), 135–148 (2007)

    Article  Google Scholar 

  32. Nedialkov, N.S.: Implementing a rigorous ODE solver through literate programming. In: Rauh, A., Auer, E. (eds.) Modeling, Design, and Simulation of Systems with Uncertainties. Mathematical Engineering, vol. 3, pp. 3–19. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-15956-5_1

    Chapter  Google Scholar 

  33. Tschaikowski, M., Tribastone, M.: Tackling continuous state-space explosion in a Markovian process algebra. Theor. Comput. Sci. 517, 1–33 (2014)

    Article  MathSciNet  Google Scholar 

  34. Tschaikowski, M., Tribastone, M.: Approximate reduction of heterogeneous nonlinear models with differential hulls. In: IEEE TAC (2016)

    Google Scholar 

Download references

Acknowledgement

Luca Cardelli is partially funded by a Royal Society Research Professorship. Mirco Tribastone is supported by a DFG Mercator Fellowship (SPP 1593, DAPS2 Project). Max Tschaikowski is supported by a Lise Meitner Fellowship funded by the Austrian Science Fund (FWF) under grant number M 2393-N32 (COCO).

Author information

Authors and Affiliations

  1. Microsoft Research, Cambridge, UK

    Luca Cardelli

  2. University of Oxford, Oxford, UK

    Luca Cardelli

  3. IMT School for Advanced Studies Lucca, Lucca, Italy

    Mirco Tribastone & Max Tschaikowski

  4. DTU Compute, Kongens Lyngby, Denmark

    Andrea Vandin

Authors
  1. Luca Cardelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mirco Tribastone
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Max Tschaikowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Andrea Vandin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrea Vandin .

Editor information

Editors and Affiliations

  1. Macquarie University , Sydney, New South Wales, Australia

    Annabelle McIver

  2. University of Turin , Turin, Italy

    Andras Horvath

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A. (2018). Guaranteed Error Bounds on Approximate Model Abstractions Through Reachability Analysis. In: McIver, A., Horvath, A. (eds) Quantitative Evaluation of Systems. QEST 2018. Lecture Notes in Computer Science(), vol 11024. Springer, Cham. https://doi.org/10.1007/978-3-319-99154-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99154-2_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99153-5

  • Online ISBN: 978-3-319-99154-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation