Skip to main content

2017 | OriginalPaper | Buchkapitel

ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations

verfasst von : Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin

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

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We present ERODE, a multi-platform tool for the solution and exact reduction of systems of ordinary differential equations (ODEs). ERODE supports two recently introduced, complementary, equivalence relations over ODE variables: forward differential equivalence yields a self-consistent aggregate system where each ODE gives the cumulative dynamics of the sum of the original variables in the respective equivalence class. Backward differential equivalence identifies variables that have identical solutions whenever starting from the same initial conditions. As back-end ERODE uses the well-known Z3 SMT solver to compute the largest equivalence that refines a given initial partition of ODE variables. In the special case of ODEs with polynomial derivatives of degree at most two (covering affine systems and elementary chemical reaction networks), it implements a more efficient partition-refinement algorithm in the style of Paige and Tarjan. ERODE comes with a rich development environment based on the Eclipse plug-in framework offering: (i) seamless project management; (ii) a fully-featured text editor; and (iii) importing-exporting capabilities.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Fußnoten
1
Throughout the paper we will work with autonomous ODE systems, which are not dependent on time. Also, we will use the terms ‘variable’ and ‘species’ interchangeably.
 
2
Here output files have been typographically adjusted to improve presentation.
 
Literatur
1.
Zurück zum Zitat Aldini, A., Bravetti, M., Gorrieri, R.: A process-algebraic approach for the analysis of probabilistic noninterference. JCS 12(2), 191–245 (2004)CrossRef Aldini, A., Bravetti, M., Gorrieri, R.: A process-algebraic approach for the analysis of probabilistic noninterference. JCS 12(2), 191–245 (2004)CrossRef
2.
Zurück zum Zitat Aoki, M.: Control of large-scale dynamic systems by aggregation. IEEE Trans. Autom. Control 13(3), 246–253 (1968)CrossRef Aoki, M.: Control of large-scale dynamic systems by aggregation. IEEE Trans. Autom. Control 13(3), 246–253 (1968)CrossRef
4.
Zurück zum Zitat 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(17), 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(17), 3289–3291 (2004)CrossRef
5.
Zurück zum Zitat Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective system behaviour: a tutorial. Perform. Eval. 70(5), 317–349 (2013)CrossRef Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective system behaviour: a tutorial. Perform. Eval. 70(5), 317–349 (2013)CrossRef
6.
Zurück zum Zitat Bortolussi, L., Lanciani, R.: Model checking Markov population models by central limit approximation. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 123–138. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40196-1_9 CrossRef Bortolussi, L., Lanciani, R.: Model checking Markov population models by central limit approximation. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 123–138. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40196-1_​9 CrossRef
8.
Zurück zum Zitat Cardelli, L.: Morphisms of reaction networks that couple structure to function. BMC Syst. Biol. 8(1), 84 (2014)CrossRef Cardelli, L.: Morphisms of reaction networks that couple structure to function. BMC Syst. Biol. 8(1), 84 (2014)CrossRef
9.
Zurück zum Zitat Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Forward and backward bisimulations for chemical reaction networks. In: CONCUR (2015) Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Forward and backward bisimulations for chemical reaction networks. In: CONCUR (2015)
10.
Zurück zum Zitat Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Comparing chemical reaction networks: a categorical and algorithmic perspective. In: LICS (2016) Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Comparing chemical reaction networks: a categorical and algorithmic perspective. In: LICS (2016)
11.
Zurück zum Zitat Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Efficient syntax-driven lumping of differential equations. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 93–111. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_6 CrossRef Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Efficient syntax-driven lumping of differential equations. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 93–111. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49674-9_​6 CrossRef
12.
Zurück zum Zitat Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Symbolic computation of differential equivalences. In: POPL (2016) Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Symbolic computation of differential equivalences. In: POPL (2016)
13.
Zurück zum Zitat 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)
16.
Zurück zum Zitat Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6), 309–315 (2003)MathSciNetCrossRefMATH Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6), 309–315 (2003)MathSciNetCrossRefMATH
17.
Zurück zum Zitat Erhard, F., Friedel, C.C., Zimmer, R.: FERN - a Java framework for stochastic simulation and evaluation of reaction networks. BMC Bioinform. 9(1), 356 (2008)CrossRef Erhard, F., Friedel, C.C., Zimmer, R.: FERN - a Java framework for stochastic simulation and evaluation of reaction networks. BMC Bioinform. 9(1), 356 (2008)CrossRef
18.
Zurück zum Zitat Feret, J., Danos, V., Krivine, J., Harmer, R., Fontana, W.: Internal coarse-graining of molecular systems. Proc. Nat. Acad. Sci. 106(16), 6453–6458 (2009)CrossRef Feret, J., Danos, V., Krivine, J., Harmer, R., Fontana, W.: Internal coarse-graining of molecular systems. Proc. Nat. Acad. Sci. 106(16), 6453–6458 (2009)CrossRef
19.
Zurück zum Zitat Feret, J., Henzinger, T., Koeppl, H., Petrov, T.: Lumpability abstractions of rule-based systems. Theoret. Comput. Sci. 431, 137–164 (2012)MathSciNetCrossRefMATH Feret, J., Henzinger, T., Koeppl, H., Petrov, T.: Lumpability abstractions of rule-based systems. Theoret. Comput. Sci. 431, 137–164 (2012)MathSciNetCrossRefMATH
20.
Zurück zum Zitat Fisher, J., Henzinger, T.A.: Executable cell biology. Nat. Biotechnol. 25(11), 1239–1249 (2007)CrossRef Fisher, J., Henzinger, T.A.: Executable cell biology. Nat. Biotechnol. 25(11), 1239–1249 (2007)CrossRef
22.
Zurück zum Zitat Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81(25), 2340–2361 (1977)CrossRef Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81(25), 2340–2361 (1977)CrossRef
23.
Zurück zum Zitat Gupta, V., Jagadeesan, R., Panangaden, P.: Approximate reasoning for real-time probabilistic processes. Log. Methods Comput. Sci. 2(1), 1–23 (2006) Gupta, V., Jagadeesan, R., Panangaden, P.: Approximate reasoning for real-time probabilistic processes. Log. Methods Comput. Sci. 2(1), 1–23 (2006)
24.
Zurück zum Zitat Hayden, R.A., Bradley, J.T.: A fluid analysis framework for a Markovian process algebra. Theor. Comput. Sci. 411(22–24), 2260–2297 (2010)MathSciNetCrossRefMATH Hayden, R.A., Bradley, J.T.: A fluid analysis framework for a Markovian process algebra. Theor. Comput. Sci. 411(22–24), 2260–2297 (2010)MathSciNetCrossRefMATH
25.
Zurück zum Zitat Iacobelli, G., Tribastone, M.: Lumpability of fluid models with heterogeneous agent types. In: DSN, pp. 1–11 (2013) Iacobelli, G., Tribastone, M.: Lumpability of fluid models with heterogeneous agent types. In: DSN, pp. 1–11 (2013)
26.
Zurück zum Zitat 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). doi:10.1007/978-3-662-48057-1_23 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). doi:10.​1007/​978-3-662-48057-1_​23 CrossRef
27.
Zurück zum Zitat Iwasa, Y., Andreasen, V., Levin, S.: Aggregation in model ecosystems. I. Perfect aggregation. Ecol. Model. 37(3–4), 287–302 (1987)CrossRefMATH Iwasa, Y., Andreasen, V., Levin, S.: Aggregation in model ecosystems. I. Perfect aggregation. Ecol. Model. 37(3–4), 287–302 (1987)CrossRefMATH
28.
29.
Zurück zum Zitat Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243–244 (2005) Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243–244 (2005)
30.
Zurück zum Zitat Kowal, M., Tschaikowski, M., Tribastone, M., Schaefer, I.: Scaling size and parameter spaces in variability-aware software performance models. In: ASE (2015) Kowal, M., Tschaikowski, M., Tribastone, M., Schaefer, I.: Scaling size and parameter spaces in variability-aware software performance models. In: ASE (2015)
32.
Zurück zum Zitat Li, G., Rabitz, H.: A general analysis of exact lumping in chemical kinetics. Chem. Eng. Sci. 44(6), 1413–1430 (1989)CrossRef Li, G., Rabitz, H.: A general analysis of exact lumping in chemical kinetics. Chem. Eng. Sci. 44(6), 1413–1430 (1989)CrossRef
34.
Zurück zum Zitat Pierro, A., Hankin, C., Wiklicky, H.: Quantitative relations and approximate process equivalences. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 508–522. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45187-7_33 CrossRef Pierro, A., Hankin, C., Wiklicky, H.: Quantitative relations and approximate process equivalences. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 508–522. Springer, Heidelberg (2003). doi:10.​1007/​978-3-540-45187-7_​33 CrossRef
35.
Zurück zum Zitat Regev, A., Shapiro, E.: Cellular abstractions: cells as computation. Nature 419(6905), 343–343 (2002)CrossRef Regev, A., Shapiro, E.: Cellular abstractions: cells as computation. Nature 419(6905), 343–343 (2002)CrossRef
36.
Zurück zum Zitat Sneddon, M.W., Faeder, J.R., Emonet, T.: Efficient modeling, simulation and coarse-graining of biological complexity with NFsim. Nat. Methods 8(2), 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(2), 177–183 (2011)CrossRef
37.
Zurück zum Zitat Tribastone, M., Gilmore, S., Hillston, J.: Scalable differential analysis of process algebra models. IEEE Trans. Softw. Eng. 38(1), 205–219 (2012)CrossRef Tribastone, M., Gilmore, S., Hillston, J.: Scalable differential analysis of process algebra models. IEEE Trans. Softw. Eng. 38(1), 205–219 (2012)CrossRef
38.
Zurück zum Zitat 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). doi:10.1007/978-3-642-32940-1_27 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). doi:10.​1007/​978-3-642-32940-1_​27 CrossRef
39.
Zurück zum Zitat Tschaikowski, M., Tribastone, M.: A unified framework for differential aggregations in Markovian process algebra. J. Log. Algebr. Meth. Program. 84(2), 238–258 (2015)MathSciNetCrossRefMATH Tschaikowski, M., Tribastone, M.: A unified framework for differential aggregations in Markovian process algebra. J. Log. Algebr. Meth. Program. 84(2), 238–258 (2015)MathSciNetCrossRefMATH
40.
Zurück zum Zitat Tschaikowski, M., Tribastone, M.: Approximate reduction of heterogenous nonlinear models with differential hulls. IEEE Trans. Autom. Control 61, 1099–1104 (2016)MathSciNetCrossRef Tschaikowski, M., Tribastone, M.: Approximate reduction of heterogenous nonlinear models with differential hulls. IEEE Trans. Autom. Control 61, 1099–1104 (2016)MathSciNetCrossRef
41.
42.
Zurück zum Zitat van Breugel, F., Worrell, J.: Approximating, computing behavioural distances in probabilistic transition systems. Theoret. Comput. Sci. 360(1–3), 373–385 (2006)MathSciNetCrossRefMATH van Breugel, F., Worrell, J.: Approximating, computing behavioural distances in probabilistic transition systems. Theoret. Comput. Sci. 360(1–3), 373–385 (2006)MathSciNetCrossRefMATH
43.
Zurück zum Zitat Vandin, A., Tribastone, M.: Quantitative abstractions for collective adaptive systems. In: Bernardo, M., Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 202–232. Springer, Heidelberg (2016). doi:10.1007/978-3-319-34096-8_7 Vandin, A., Tribastone, M.: Quantitative abstractions for collective adaptive systems. In: Bernardo, M., Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 202–232. Springer, Heidelberg (2016). doi:10.​1007/​978-3-319-34096-8_​7
44.
Metadaten
Titel
ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations
verfasst von
Luca Cardelli
Mirco Tribastone
Max Tschaikowski
Andrea Vandin
Copyright-Jahr
2017
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-54580-5_19

Premium Partner