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:
Automating Abstract Interpretation Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

A Method for Invariant Generation for Polynomial Continuous Systems

verfasst von : Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, André Platzer

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config
loading …

Abstract

This paper presents a method for generating semi-algebraic invariants for systems governed by non-linear polynomial ordinary differential equations under semi-algebraic evolution constraints. Based on the notion of discrete abstraction, our method eliminates unsoundness and unnecessary coarseness found in existing approaches for computing abstractions for non-linear continuous systems and is able to construct invariants with intricate boolean structure, in contrast to invariants typically generated using template-based methods. In order to tackle the state explosion problem associated with discrete abstraction, we present invariant generation algorithms that exploit sound proof rules for safety verification, such as differential cut (\({\text {DC}}\)), and a new proof rule that we call differential divide-and-conquer (\({\text {DDC}}\)), which splits the verification problem into smaller sub-problems. The resulting invariant generation method is observed to be much more scalable and efficient than the naïve approach, exhibiting orders of magnitude performance improvement on many of the problems.

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 Lipschitz Robustness of Timed I/O Systems
Nächstes Kapitel Hybrid Analysis for Partial Order Reduction of Programs with Arrays
Fußnoten
1
A semi-algebraic set is a subset of \(\mathbb {R}^n\) characterized by a finite boolean combination of sets defined by polynomial equalities and inequalities.
 
2
In the sense of not having an explicit dependence on the time variable t.
 
3
Evolution constraints are often used to define operating modes in hybrid and cyber-physical systems (so-called mode, or location invariants in the parlance of hybrid automata [1, 13]).
 
4
Considering the continuous system \( \dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H\) as a program, the safety assertion \( \psi \rightarrow [ \dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H ] \ \phi \) expresses the (continuous) Hoare triple \( \{ \psi \} \ \dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H \ \{ \phi \}\).
 
5
All three regions are invariant sets in the terminology of dynamical systems [5, Chapter II].
 
6
expression simplified in Mathematica.
 
8
The comparison was performed on an i5-3570 K CPU clocked at 3.40 GHz.
 
Literatur
1.
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993)CrossRef
2.
Alur, R., Dang, T., Ivančić, F.: Progress on reachability analysis of hybrid systems using predicate abstraction. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 4–19. Springer, Heidelberg (2003)CrossRef
3.
Alur, R., Dang, T., Ivančić, F.: Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embed. Comput. Syst. 5(1), 152–199 (2006)CrossRef
4.
Arrowsmith, D., Place, C.: Dynamical Systems. Differential Equations, Maps and Chaotic Behaviour. Chapman & Hall, London (1992)
5.
Bhatia, N.P., Szegő, G.P.: Stability Theory of Dynamical Systems. Springer, Heidelberg (1970)MATHCrossRef
6.
7.
Dumortier, F., Llibre, J., Artés, J.C.: Qualitative Theory of Planar Differential Systems. Springer, Berlin (2006)MATH
8.
Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 279–294. Springer, Heidelberg (2014)CrossRef
9.
Ghorbal, K., Sogokon, A., Platzer, A.: A hierarchy of proof rules for checking differential invariance of algebraic sets. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 431–448. Springer, Heidelberg (2015)
10.
Goriely, A.: Integrability and Nonintegrability of Dynamical Systems. Advanced series in nonlinear dynamics. World Scientific, Singapore (2001)MATH
11.
Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190–203. Springer, Heidelberg (2008)CrossRef
12.
13.
Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278–292. IEEE Computer Society Press (1996)
14.
Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) EMSOFT, pp. 97–106. ACM (2011)
15.
Liu, J., Zhan, N., Zhao, H., Zou, L.: Abstraction of elementary hybrid systems by variable transformation. In: Bjørner, N., Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 360–377. Springer, Heidelberg (2015)CrossRef
16.
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)CrossRef
17.
Papachristodoulou, A., Prajna, S.: Analysis of non-polynomial systems using the sum of squares decomposition. In: Henrion, D., Garulli, A. (eds.) Positive Polynomials in Control. Lecture Notes in Control and Information Science, vol. 312, pp. 23–43. Springer, Berlin (2005)
18.
19.
Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010)MATHMathSciNetCrossRef
20.
Platzer, A.: The complete proof theory of hybrid systems. In: LICS, pp. 541–550. IEEE (2012)
21.
Platzer, A.: The structure of differential invariants and differential cut elimination. LMCS 8(4), 1–38 (2012)
22.
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
23.
Powers, J.E.: Elimination of special functions from differential equations. Commun. ACM 2(3), 3–4 (1959)MATHCrossRef
24.
Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004)CrossRef
25.
Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embed. Comput. Syst., vol. 6(1), Febuary 2007
26.
Richardson, D.: Some undecidable problems involving elementary functions of a real variable. J. Symb. Log. 33(4), 514–520 (1968)MATHCrossRef
27.
Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: HSCC, pp. 221–230 (2010)
28.
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. FMSD 32(1), 25–55 (2008)MATH
29.
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)CrossRef
30.
Savageau, M.A., Voit, E.O.: Recasting nonlinear differential equations as S-systems: a canonical nonlinear form. Math. Biosci. 87(1), 83–115 (1987)MATHMathSciNetCrossRef
31.
Schlomiuk, D.: Algebraic and geometric aspects of the theory of polynomial vector fields. In: Schlomiuk, D. (ed.) Bifurcations and Periodic Orbits of Vector Fields. NATO ASI Series, vol. 408, pp. 429–467. Springer, Heidelberg (1993)CrossRef
32.
Schlomiuk, D.: Algebraic particular integrals, integrability and the problem of the center. Trans. Am. Math. Soci. 338(2), 799–841 (1993)MATHMathSciNetCrossRef
33.
Strogatz, S.H.: Nonlinear Dynamics and Chaos. Westview Press, New York (1994)
34.
Stursberg, O., Kowalewski, S., Hoffmann, I., Preußig, J.: Comparing timed and hybrid automata as approximations of continuous systems. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1996. LNCS, vol. 1273. Springer, Heidelberg (1997)CrossRef
35.
Tarski, A.: A decision method for elementary algebra and geometry. Bull. Am. Math. Soci. 59, 91–93 (1951)
36.
Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, p. 465. Springer, Heidelberg (2002)CrossRef
37.
Tiwari, A.: Abstractions for hybrid systems. FMSD 32(1), 57–83 (2008)MATH
38.
Tiwari, A.: Generating box invariants. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 658–661. Springer, Heidelberg (2008)CrossRef
39.
Tiwari, A., Khanna, G.: Nonlinear systems: approximating reach sets. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 600–614. Springer, Heidelberg (2004)CrossRef
40.
Wang, T.C., Lall, S., West, M.: Polynomial level-set method for polynomial system reachable set estimation. IEEE Trans. Autom. Control 58(10), 2508–2521 (2013)MathSciNetCrossRef
41.
Wiggins, S.: Introduction to Applied Nonlinear Dynamical Systems and Chaos. Texts in Applied Mathematics, 2nd edn. Springer, New York (2003)MATH
42.
Wu, Z.: Tangent cone and contingent cone to the intersection of two closed sets. Nonlinear Anal.: Theor., Methods Appl. 73(5), 1203–1220 (2010)MATHCrossRef
43.
Zaki, M.H., Tahar, S., Bois, G.: A symbolic approach for the safety verification of continuous systems. In: Proceedings of the International Conference on Computational Sciences, pp. 93–100 (2007)
44.
Zhao, H., Zhan, N., Kapur, D.: Synthesizing switching controllers for hybrid systems by generating invariants. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 354–373. Springer, Heidelberg (2013)CrossRef
Metadaten
Titel
A Method for Invariant Generation for Polynomial Continuous Systems
verfasst von
Andrew Sogokon
Khalil Ghorbal
Paul B. Jackson
André Platzer
Copyright-Jahr
2016
Verlag
Springer Berlin Heidelberg
Buch
Verification, Model Checking, and Abstract Interpretation

Print ISBN: 978-3-662-49121-8

Electronic ISBN: 978-3-662-49122-5

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-662-49122-5_13