Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Poling: SMT Aided Linearizability Proofs Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Automatic Verification of Stability and Safety for Delay Differential Equations

verfasst von : Liang Zou, Martin Fränzle, Naijun Zhan, Peter Nazier Mosaad

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Delay differential equations (DDEs) arise naturally as models of, e.g., networked control systems, where the communication delay in the feedback loop cannot always be ignored. Such delays can prompt oscillations and may cause deterioration of control performance, invalidating both stability and safety properties. Nevertheless, state-exploratory automatic verification methods have until now concentrated on ordinary differential equations (and their piecewise extensions to hybrid state) only, failing to address the effects of delays on system dynamics. We overcome this problem by iterating bounded degree interval-based Taylor overapproximations of the time-wise segments of the solution to a DDE, thereby identifying and automatically analyzing the operator that yields the parameters of the Taylor overapproximation for the next temporal segment from the current one. By using constraint solving for analyzing the properties of this operator, we obtain a procedure able to provide stability and safety certificates for a simple class of DDEs.

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 Measuring with Timed Patterns
Nächstes Kapitel Time Robustness in MTL and Expressivity in Hybrid System Falsification
Fußnoten
1
The prototype implementation of the verification tool as well as the examples are available for download from https://​github.​com/​liangdzou/​isat-dde.
 
Literatur
1.
Balachandran, B., Kalmár-Nagy, T., Gilsinn, D.E.: Delay Differential Equations. Springer, (2009)
2.
Richard, B., Cooke, K.L.: Differential-difference equations. Technical report R-374-PR, The RAND Corporation, Santa Monica (1963)
3.
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)MathSciNetCrossRef
4.
Stephen, B., El Ghaoui, L., Feron, E., Balakrishnan, V.: Linear matrix inequalities in system and control theory of studies in applied mathematics. Soc. Ind. Appl. Math. (SIAM) 15, 215–249 (1994)
5.
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) CrossRef
6.
Chutinan, A., Krogh, B.H.: Computing polyhedral approximations to flow pipes for dynamic systems. In: Proceedings of the 37th International Conference on Decision and Control (CDC 1998) (1998)
7.
Daafouz, J., Bernussou, J.: Parameter dependent Lyapunov functions for discrete time systems with time varying parametric uncertainties. Sys. Control Lett. 43(5), 355–359 (2001)MathSciNetCrossRef
8.
Eggers, A., Fränzle, M., Herde, C.: SAT Modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171–185. Springer, Heidelberg (2008) CrossRef
9.
Andreas, E., Nacim, R., Nedialkov, N.S., Fränzle, M.: Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods. Software Systems Modeling 6, 1–28 (2012)
10.
Fort, J., Méndez, V.: Time-delayed theory of the neolithic transition in europe. Phys. Rev. Lett 82(4), 867 (1999)CrossRef
11.
Fränzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. Satisfiability Boolean Model. Comput. Spec. Issue SAT/CP Integr. 1, 209–236 (2007)
12.
Fränzle, M., Teige, T., Eggers, A.: Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. J. Logic Algebraic Programm. 79, 436–466 (2010)CrossRef
13.
Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291–305. Springer, Heidelberg (2005) CrossRef
14.
Glass, L., Mackey, M.C.: From Clocks to Chaos: The Rhythms of Life. Princeton University Press, Princeton (1988)
15.
Gustafson, G.B.: Systems of differential equations. In: Manuscript for Course Eng Math 2250–1 Spring 2014, ch 11. University of Utah, Department of Mathematics (2014)
16.
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)MathSciNetCrossRef
17.
Ikeda, K., Matsumoto, K.: High-dimensional chaotic behavior in systems with time-delayed feedback. Physica D 29(1–2), 223–235 (1987)CrossRef
18.
Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: delta-reachability analysis for hybrid systems. In: TACAS (2015)
19.
Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for hybrid dynamics: the reachability problem. In: Dayawansa, W.P., Lindquist, A., Zhou, Y. (eds.) New Directions and Applications in Control Theory. Lecture Notes in Control and Information Sciences, pp. 193–205. Springer, Heidelberg (2005) CrossRef
20.
Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symbolic Comput. 32(3), 231–253 (2001)MathSciNetCrossRef
21.
Lakshmanan, M., Senthilkumar, D.V.: Dynamics of Nonlinear Time-delay Systems. Springer Science Business Media. Springer, Heidelberg (2011) CrossRef
22.
Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Sys. 4(2), 250–262 (2010)CrossRef
23.
Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT 2011, pp. 97–106. ACM New York (2011)
24.
Liu, J., Zhan, N., Zhao, H.: Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems. Math. Comput. Sci. 6(4), 395–408 (2012)MathSciNetCrossRef
25.
Lohner, R.: Einschließung der Lösung gewöhnlicher Anfangs- und Randwertaufgaben. Ph.D. thesis, Fakultät für Mathematik der Universität Karlsruhe, Karlsruhe (1988)
26.
Mackey, M.C., Glass, L., et al.: Oscillation and chaos in physiological control systems. Science 197(4300), 287–289 (1977)CrossRef
27.
Moore, R.E.: Automatic local coordinate transformation to reduce the growth of error bounds in interval computation of solutions of ordinary differential equations. In: Ball, L.B. (ed.) Error in Digital Computation. volume II, pp. 103–140. Wiley, New York (1965)
28.
Neher, M., Jackson, K.R., Nedialkov, N.S.: On Taylor model based integration of ODEs. SIAM J. Numer. Anal. 45(1), 236–262 (2007)MathSciNetCrossRef
29.
Oehlerking, J.: Decomposition of Stability Proofs for Hybrid Systems. Doctoral dissertation, Carl von Ossietzky Universität Oldenburg, Department of Computing Science (2011)
30.
Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010)MathSciNetCrossRef
31.
Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 176–189. Springer, Heidelberg (2008) CrossRef
32.
Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415–1428 (2007)MathSciNetCrossRef
33.
Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 573–589. Springer, Heidelberg (2005) CrossRef
34.
Ratschan, S., She, Z.: Providing a basin of attraction to a target region by computation of Lyapunov-like functions. In: IEEE International Conference on Computational Cybernetics (ICCC 2006), pp. 1–5 (2006)
35.
Rohn, J., Kreslová, J.: Linear interval inequalities. Linear Multilinear Algebra 38(1–2), 79–82 (1994)CrossRef
36.
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 539–554. Springer, Heidelberg (2004) CrossRef
37.
Stauning, O.: Automatic Validation of Numerical Solutions. Ph.D .thesis, Technical University of Denmark, Lyngby (1997)
38.
Szydłowski, M., Krawiec, A.: The stability problem in the kaldor-kalecki business cycle model. Chaos Solitons Fractals 25(2), 299–305 (2005)MathSciNetCrossRef
39.
Szydłowski, M., Krawiec, A., Toboła, J.: Nonlinear oscillations in business cycle model with time lags. Chaos, Solitons Fractals 12(3), 505–517 (2001)CrossRef
40.
Tang, X., Zou, X.: Global attractivity in a predator-prey system with pure delays. Proc. Edinburgh Math. Soc. 51, 495–508 (2008)MathSciNetCrossRef
41.
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) CrossRef
Metadaten
Titel
Automatic Verification of Stability and Safety for Delay Differential Equations
verfasst von
Liang Zou
Martin Fränzle
Naijun Zhan
Peter Nazier Mosaad
Copyright-Jahr
2015
Buch
Computer Aided Verification

Print ISBN: 978-3-319-21667-6

Electronic ISBN: 978-3-319-21668-3

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-21668-3_20