Skip to main content
Top

2016 | OriginalPaper | Chapter

Efficient Syntax-Driven Lumping of Differential Equations

Authors : Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin

Published in: Tools and Algorithms for the Construction and Analysis of Systems

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We present an algorithm to compute exact aggregations of a class of systems of ordinary differential equations (ODEs). Our approach consists in an extension of Paige and Tarjan’s seminal solution to the coarsest refinement problem by encoding an ODE system into a suitable discrete-state representation. In particular, we consider a simple extension of the syntax of elementary chemical reaction networks because (i) it can express ODEs with derivatives given by polynomials of degree at most two, which are relevant in many applications in natural sciences and engineering; and (ii) we can build on two recently introduced bisimulations, which yield two complementary notions of ODE lumping. Our algorithm computes the largest bisimulations in \(O(r \cdot s \cdot \log s)\) time, where r is the number of monomials and s is the number of variables in the ODEs. Numerical experiments on real-world models from biochemistry, electrical engineering, and structural mechanics show that our prototype is able to handle ODEs with millions of variables and monomials, providing significant model reductions.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
All proofs are given in a technical report available at http://​sysma.​imtlucca.​it/​crnreducer/​.
 
2
We implicitly disregard pathological cases with species not appearing in any reaction.
 
Literature
1.
go back to reference Danos, V., Feret, J., Fontana, W., Harmer, R., Krivine, J.: Abstracting the differential semantics of rule-based models: exact and automated model reduction. In: LICS, pp. 362–381 (2010) Danos, V., Feret, J., Fontana, W., Harmer, R., Krivine, J.: Abstracting the differential semantics of rule-based models: exact and automated model reduction. In: LICS, pp. 362–381 (2010)
2.
go back to reference Blinov, M.L., Faeder, J.R., Goldstein, B., Hlavacek, W.S.: BioNetGen: software for rule-based modeling of signal transduction based on the interactions of molecular domains. Bioinformatics 20, 3289–3291 (2004)CrossRef Blinov, M.L., Faeder, J.R., Goldstein, B., Hlavacek, W.S.: BioNetGen: software for rule-based modeling of signal transduction based on the interactions of molecular domains. Bioinformatics 20, 3289–3291 (2004)CrossRef
3.
4.
go back to reference 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)CrossRef 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)CrossRef
5.
go back to reference Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60, 187–231 (2000)MathSciNetCrossRefMATH Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60, 187–231 (2000)MathSciNetCrossRefMATH
6.
7.
go back to reference Valmari, A., Franceschinis, G.: Simple O(m logn) time Markov chain lumping. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 38–52. Springer, Heidelberg (2010)CrossRef Valmari, A., Franceschinis, G.: Simple O(m logn) time Markov chain lumping. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 38–52. Springer, Heidelberg (2010)CrossRef
9.
go back to reference Murray, J.D.: Mathematical Biology I: An Introduction, 3rd edn. Springer, Heidelberg (2002)MATH Murray, J.D.: Mathematical Biology I: An Introduction, 3rd edn. Springer, Heidelberg (2002)MATH
10.
go back to reference Feinberg, M.: Chemical reaction network structure and the stability of complex isothermal reactors – I. The deficiency zero and deficiency one theorems. Chem. Eng. Sci. 42, 2229–2268 (1987)CrossRef Feinberg, M.: Chemical reaction network structure and the stability of complex isothermal reactors – I. The deficiency zero and deficiency one theorems. Chem. Eng. Sci. 42, 2229–2268 (1987)CrossRef
11.
go back to reference Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Forward and backward bisimulations for chemical reaction networks. In: CONCUR, pp. 226–239 (2015) Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Forward and backward bisimulations for chemical reaction networks. In: CONCUR, pp. 226–239 (2015)
14.
go back to reference Saad, Y.: Iterative Methods for Sparse Linear Systems, 2nd edn. Society for Industrial and Applied Mathematics, Philadelphia (2003)CrossRefMATH Saad, Y.: Iterative Methods for Sparse Linear Systems, 2nd edn. Society for Industrial and Applied Mathematics, Philadelphia (2003)CrossRefMATH
15.
go back to reference Davis, T.A., Hu, Y.: The University of Florida sparse matrix collection. ACM Trans. Math. Softw. 38, 1–25 (2011)MathSciNet Davis, T.A., Hu, Y.: The University of Florida sparse matrix collection. ACM Trans. Math. Softw. 38, 1–25 (2011)MathSciNet
16.
go back to reference Li, G., Rabitz, H.: A general analysis of exact lumping in chemical kinetics. Chem. Eng. Sci. 44, 1413–1430 (1989)CrossRef Li, G., Rabitz, H.: A general analysis of exact lumping in chemical kinetics. Chem. Eng. Sci. 44, 1413–1430 (1989)CrossRef
17.
go back to reference Toth, J., Li, G., Rabitz, H., Tomlin, A.S.: The effect of lumping and expanding on kinetic differential equations. SIAM J. Appl. Math. 57, 1531–1556 (1997)MathSciNetCrossRefMATH Toth, J., Li, G., Rabitz, H., Tomlin, A.S.: The effect of lumping and expanding on kinetic differential equations. SIAM J. Appl. Math. 57, 1531–1556 (1997)MathSciNetCrossRefMATH
18.
go back to reference Tschaikowski, M., Tribastone, M.: Exact fluid lumpability for Markovian process algebra. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 380–394. Springer, Heidelberg (2012)CrossRef Tschaikowski, M., Tribastone, M.: Exact fluid lumpability for Markovian process algebra. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 380–394. Springer, Heidelberg (2012)CrossRef
19.
go back to reference Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Symbolic computation of differential equivalences. In: POPL (2016, to appear) Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Symbolic computation of differential equivalences. In: POPL (2016, to appear)
20.
go back to reference Iacobelli, G., Tribastone, M., Vandin, A.: Differential bisimulation for a Markovian process algebra. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 293–306. Springer, Heidelberg (2015)CrossRef Iacobelli, G., Tribastone, M., Vandin, A.: Differential bisimulation for a Markovian process algebra. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 293–306. Springer, Heidelberg (2015)CrossRef
21.
go back to reference Hars, V., Toth, J.: On the inverse problem of reaction kinetics. Colloquia Mathematica Societatis Janos Bolyai 30, 363–379 (1979)MATH Hars, V., Toth, J.: On the inverse problem of reaction kinetics. Colloquia Mathematica Societatis Janos Bolyai 30, 363–379 (1979)MATH
22.
go back to reference Sneddon, M.W., Faeder, J.R., Emonet, T.: Efficient modeling, simulation and coarse-graining of biological complexity with NFsim. Nat. Methods 8, 177–183 (2011)CrossRef Sneddon, M.W., Faeder, J.R., Emonet, T.: Efficient modeling, simulation and coarse-graining of biological complexity with NFsim. Nat. Methods 8, 177–183 (2011)CrossRef
23.
go back to reference Suderman, R., Deeds, E.J.: Machines vs ensembles: effective MAPK signaling through heterogeneous sets of protein complexes. PLoS Comput. Biol. 9, e1003278 (2013)CrossRef Suderman, R., Deeds, E.J.: Machines vs ensembles: effective MAPK signaling through heterogeneous sets of protein complexes. PLoS Comput. Biol. 9, e1003278 (2013)CrossRef
24.
go back to reference Faeder, J.R., Hlavacek, W.S., Reischl, I., Blinov, M.L., Metzger, H., Redondo, A., Wofsy, C., Goldstein, B.: Investigation of early events in Fc\(\varepsilon \)RI-mediated signaling using a detailed mathematical model. J. Immunol. 170, 3769–3781 (2003)CrossRef Faeder, J.R., Hlavacek, W.S., Reischl, I., Blinov, M.L., Metzger, H., Redondo, A., Wofsy, C., Goldstein, B.: Investigation of early events in Fc\(\varepsilon \)RI-mediated signaling using a detailed mathematical model. J. Immunol. 170, 3769–3781 (2003)CrossRef
25.
go back to reference Barua, D., Faeder, J.R., Haugh, J.M.: A bipolar clamp mechanism for activation of jak-family protein tyrosine kinases. PLoS Comput. Biol. 5, e1000364 (2009)CrossRef Barua, D., Faeder, J.R., Haugh, J.M.: A bipolar clamp mechanism for activation of jak-family protein tyrosine kinases. PLoS Comput. Biol. 5, e1000364 (2009)CrossRef
26.
go back to reference Barua, D., Hlavacek, W.S.: Modeling the effect of apc truncation on destruction complex function in colorectal cancer cells. PLoS Comput. Biol. 9, e1003217 (2013)CrossRef Barua, D., Hlavacek, W.S.: Modeling the effect of apc truncation on destruction complex function in colorectal cancer cells. PLoS Comput. Biol. 9, e1003217 (2013)CrossRef
27.
go back to reference Colvin, J., Monine, M.I., Faeder, J.R., Hlavacek, W.S., Hoff, D.D.V., Posner, R.G.: Simulation of large-scale rule-based models. Bioinformatics 25, 910–917 (2009)CrossRef Colvin, J., Monine, M.I., Faeder, J.R., Hlavacek, W.S., Hoff, D.D.V., Posner, R.G.: Simulation of large-scale rule-based models. Bioinformatics 25, 910–917 (2009)CrossRef
28.
go back to reference Kocieniewski, P., Faeder, J.R., Lipniacki, T.: The interplay of double phosphorylation and scaffolding in MAPK pathways. J. Theor. Biol. 295, 116–124 (2012)MathSciNetCrossRef Kocieniewski, P., Faeder, J.R., Lipniacki, T.: The interplay of double phosphorylation and scaffolding in MAPK pathways. J. Theor. Biol. 295, 116–124 (2012)MathSciNetCrossRef
29.
go back to reference Cardelli, L.: Morphisms of reaction networks that couple structure to function. BMC Syst. Biol. 8, 84 (2014)CrossRef Cardelli, L.: Morphisms of reaction networks that couple structure to function. BMC Syst. Biol. 8, 84 (2014)CrossRef
30.
go back to reference Massink, M., Katoen, J., Latella, D.: Model checking dependability attributes of wireless group communication. In: DSN, pp. 711–720 (2004) Massink, M., Katoen, J., Latella, D.: Model checking dependability attributes of wireless group communication. In: DSN, pp. 711–720 (2004)
31.
go back to reference Haverkort, B., Hermanns, H., Katoen, J.P.: On the use of model checking techniques for dependability evaluation. In: SRDS, pp. 228–237 (2000) Haverkort, B., Hermanns, H., Katoen, J.P.: On the use of model checking techniques for dependability evaluation. In: SRDS, pp. 228–237 (2000)
32.
go back to reference Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 234–248. Springer, Heidelberg (2006)CrossRef Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 234–248. Springer, Heidelberg (2006)CrossRef
33.
go back to reference Katoen, J., Khattri, M., Zapreev, I.: A Markov reward model checker. In: QEST, pp. 243–244 (2005) Katoen, J., Khattri, M., Zapreev, I.: A Markov reward model checker. In: QEST, pp. 243–244 (2005)
34.
go back to reference Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007)CrossRef Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007)CrossRef
Metadata
Title
Efficient Syntax-Driven Lumping of Differential Equations
Authors
Luca Cardelli
Mirco Tribastone
Max Tschaikowski
Andrea Vandin
Copyright Year
2016
Publisher
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-49674-9_6

Premium Partner