nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Decoupling Abstractions of Non-linear Ordinary Differential Equations

verfasst von : Andrew Sogokon, Khalil Ghorbal, Taylor T. Johnson

Erschienen in: FM 2016: Formal Methods

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We investigate decoupling abstractions, by which we seek to simulate (i.e. abstract) a given system of ordinary differential equations (ODEs) by another system that features completely independent (i.e. uncoupled) sub-systems, which can be considered as separate systems in their own right. Beyond a purely mathematical interest as a tool for the qualitative analysis of ODEs, decoupling can be applied to verification problems arising in the fields of control and hybrid systems. Existing verification technology often scales poorly with dimension. Thus, reducing a verification problem to a number of independent verification problems for systems of smaller dimension may enable one to prove properties that are otherwise seen as too difficult. We show an interesting correspondence between Darboux polynomials and decoupling simulating abstractions of systems of polynomial ODEs and give a constructive procedure for automatically computing the latter.

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel An Implementation of Deflate in Coq

Nächstes Kapitel Regression Verification for Unbalanced Recursive Functions

By this we understand a finite expression in terms of polynomials and elementary functions such as \(\sin ,\cos ,\exp ,\ln \), etc.

i.e. p is a first integral if \(\mathfrak {L}_f(p) = \lambda p\) where \(\lambda =0\).

When q is a constant, the Darboux polynomial is trivial [11, Definition 2.14]. In this paper we will generally be interested in the non-trivial case.

Abrial, J.-R., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 178–193. Springer, Heidelberg (2012). doi:10.1007/978-3-642-30885-7_13 CrossRef

Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: HSCC, pp. 128–133. ACM (2015)

Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliable Comput. 4(4), 361–369 (1998)MathSciNetCrossRefMATH

Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975). doi:10.1007/3-540-07407-4_17 CrossRef

Conti, R., Galeotti, M.: Totally bounded cubic systems in \(\mathbb{R}^2\). In: Macki, J.W., Zecca, P. (eds.) Dynamical Systems. LNM, vol. 1822, pp. 103–171. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45204-1_2 CrossRef

Dumortier, F., Llibre, J., Artés, J.C.: Qualitative Theory of Planar Differential Systems. Springer, Heidelberg (2006)MATH

Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 279–294. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_19 CrossRef

Giannakopoulou, D., Méry, D. (eds.): FM 2012. LNCS, vol. 7436. Springer, Heidelberg (2012)MATH

Ginoux, J.M.: Differential Geometry Applied to Dynamical Systems. World Scientific Series on Nonlinear Science, vol. 66. World Scientific, Singapore (2009)MATH

10.

Girard, A., Pappas, G.J.: Approximate bisimulation: a bridge between computer science and control theory. Eur. J. Control 17(5–6), 568–578 (2011)MathSciNetCrossRefMATH

11.

Goriely, A.: Integrability and Nonintegrability of Dynamical Systems. Advanced Series in Nonlinear Dynamics. World Scientific, Singapore (2001)CrossRefMATH

12.

Hale, J.K., LaSalle, J.P.: Differential equations: linearity vs. nonlinearity. SIAM Rev. 5(3), 249–272 (1963)MathSciNetCrossRefMATH

13.

Han, Z., Krogh, B.: Reachability analysis of hybrid control systems using reduced-order models. In: 2004 American Control Conference, Proceedings of the 2004, vol. 2, pp. 1183–1189, June 2004

14.

Jeannin, J.-B., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 21–36. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_2

15.

Matringe, N., Moura, A.V., Rebiha, R.: Generating invariants for non-linear hybrid systems by linear algebraic methods. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 373–389. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15769-1_23 CrossRef

16.

Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: 12th GAMM - IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN), p. 4, September 2006

17.

Neher, M., Jackson, K.R., Nedialkov, N.S.: On Taylor model based integration of ODEs. SIAM J. Numer. Anal. 45(1), 236–262 (2007)MathSciNetCrossRefMATH

18.

Pappas, G.J.: Bisimilar linear systems. Automatica 39(12), 2035–2047 (2003)MathSciNetCrossRefMATH

19.

Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reasoning, 1–47 (2016)

20.

Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: a case study. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 547–562. Springer, Heidelberg (2009). doi:10.1007/978-3-642-05089-3_35 CrossRef

21.

Robinson, J.C.: An Introduction to Ordinary Differential Equations. Cambridge University Press, Cambridge (2004)CrossRefMATH

22.

Sankaranarayanan, S.: Change-of-bases abstractions for non-linear hybrid systems. Nonlinear Anal. Hybrid Syst. 19, 107–133 (2016)MathSciNetCrossRefMATH

23.

Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Formal Methods Syst. Des. 32(1), 25–55 (2008)CrossRefMATH

24.

Sankaranarayanan, S., Tiwari, A.: Relational abstractions for continuous and hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 686–702. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_56 CrossRef

25.

Strogatz, S.H.: Nonlinear Dynamics and Chaos. Westview Press, New York (1994)

26.

Tarski, A.: A decision method for elementary algebra and geometry. In: Bulletin of the American Mathematical Society, vol. 59 (1951)

27.

Teschl, G.: Ordinary Differential Equations and Dynamical Systems. Graduate Studies in Mathematics, vol. 140. American Mathematical Society, Providence (2012)MATH

28.

Zhao, H., Yang, M., Zhan, N., Gu, B., Zou, L., Chen, Y.: Formal verification of a descent guidance control program of a lunar lander. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 733–748. Springer, Heidelberg (2014). doi:10.1007/978-3-319-06410-9_49 CrossRef

29.

Zou, L., Lv, J., Wang, S., Zhan, N., Tang, T., Yuan, L., Liu, Y.: Verifying chinese train control system under a combined scenario by theorem proving. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 262–280. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54108-7_14 CrossRef

Titel: Decoupling Abstractions of Non-linear Ordinary Differential Equations
verfasst von: Andrew Sogokon
Khalil Ghorbal
Taylor T. Johnson
Verlag: Springer International Publishing
Buch: FM 2016: Formal Methods
Print ISBN: 978-3-319-48988-9

Electronic ISBN: 978-3-319-48989-6

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-48989-6_38

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner