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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 1/2014

01.02.2014

Safety verification of non-linear hybrid systems is quasi-decidable

verfasst von: Stefan Ratschan

Erschienen in: Formal Methods in System Design | Ausgabe 1/2014

Einloggen

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

search-config
loading …

Abstract

Safety verification of hybrid systems is undecidable, except for very special cases. In this paper, we circumvent undecidability by providing a verification algorithm that provably terminates for all robust problem instances, but need not necessarily terminate for non-robust problem instances. A problem instance x is robust iff the given property holds not only for x itself, but also when x is perturbed a little bit. Since, in practice, well-designed hybrid systems are usually robust, this implies that the algorithm terminates for the cases occurring in practice. In contrast to earlier work, our result holds for a very general class of hybrid systems, and it uses a continuous time model.
Vorheriger Artikel Automata-based symbolic string analysis for vulnerability detection
Nächster Artikel Some notes on the abstraction operation for multi-terminal binary decision diagrams

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 "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

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
Fußnoten
1
In fact, in the special case of timed automata, there is a whole stream of work on avoiding the verification of non-robust properties, see for example [20, 25].
 
2
For a function \(f: \mathbb{R}^{n}\rightarrow \mathbb{R}\), compact intervals I 1,…,I n , we need to be able to compute an interval J⊇f(I 1,…,I n ) such that the over-approximation of J over f(I 1,…,I n ) can be made arbitrarily small. Note that this requires continuity of f but not Lipschitz continuity. For example, we could include \(\sqrt{|x|}\), which is not Lipschitz continuous.
 
3
Here it does not suffice to perturb hybrid systems without regard to the constraint language they are described in. The reason for this can be seen in the example of a constraint 0=0. This constraint has the same solution set as the constraint 1≥0. However, in the case 0=0 small perturbations of the constraint itself change the solution set essentially [22] whereas in the case 1≥0 they do not. The solution we take here, is to not only consider perturbations on the semantic level, but to also take into account syntactic perturbations. Another solution is, to base the definition of hybrid systems on set-valued functions, and then to perturb those functions. See, for-example, Definition 6.27 in the book by Goebel and others [12].
 
Literatur
1.
Asarin E, Bouajjani A (2001) Perturbed Turing machines and hybrid systems. In: Proc LICS’01, pp 269–278
2.
Aubin J-P, Frankowska H (1990) Set-valued analysis. Birkhäuser, Boston MATH
3.
Bhatia A, Frazzoli E (2007) Sampling-based resolution-complete safety falsification of linear hybrid systems. In: 46th IEEE conference on decision and control, pp 3405–3411
4.
Bournez O, Campagnolo ML (2008) A survey on continuous time computations. In: Cooper S, Löwe B, Sorbi A (eds) New computational paradigms. Springer, New York, pp 383–423 CrossRef
5.
Caviness BF, Johnson JR (eds) (1998) Quantifier elimination and cylindrical algebraic decomposition. Springer, Berlin MATH
6.
Cheng P, Kumar V (2008) Sampling-based falsification and verification of controllers for continuous dynamic systems. Int J Robot Res 27(11–12):1232–1245 CrossRef
7.
Collins P (2005) Continuity and computability of reachable sets. Theor Comput Sci 341:162–195 CrossRefMATH
8.
9.
Damm W, Pinto G, Ratschan S (2007) Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. Int J Found Comput Sci 18(1):63–86 CrossRefMATHMathSciNet
10.
Fränzle M (1999) Analysis of hybrid systems: an ounce of realism can save an infinity of states. In: Flum J, Rodriguez-Artalejo M (eds) Computer science logic (CSL’99). LNCS, vol 1683. Springer, Berlin
11.
Fränzle M (2001) What will be eventually true of polynomial hybrid automata. In: Kobayashi N, Pierce BC (eds) Theoretical aspects of computer software (TACS 2001). LNCS, vol 2215. Springer, Berlin
12.
Goebel R, Sanfelice RG, Teel AR (2012) Hybrid dynamical systems: modeling, stability, and robustness. Princeton University Press, Princeton
13.
Goebel R, Teel A (2006) Solutions to hybrid inclusions via set and graphical convergence with stability theory applications. Automatica 42(4):573–587 CrossRefMATHMathSciNet
14.
Henzinger TA, Ho P-H, Wong-Toi H (1998) Algorithmic analysis of nonlinear hybrid systems. IEEE Trans Autom Control 43:540–554 CrossRefMATHMathSciNet
15.
16.
Henzinger TA, Raskin J-F (2000) Robust undecidability of timed and hybrid systems. In: Lynch N, Krogh B (eds) Proc HSCC’00. LNCS, vol 1790. Springer, Berlin
17.
Khalil HK (2002) Nonlinear systems, 3rd edn. Prentice Hall, New York MATH
18.
Moore RE (1966) Interval analysis. Prentice Hall, Englewood Cliffs MATH
19.
Neumaier A (1990) Interval methods for systems of equations. Cambridge University Press, Cambridge MATH
20.
21.
Puri A, Borkar V, Varaiya P (1996) ε-Approximation of differential inclusions. In: Alur R, Henzinger TA, Sontag ED (eds) Hybrid systems. LNCS, vol 1066. Springer, Berlin
22.
23.
Ratschan S (2010) Safety verification of non-linear hybrid systems is quasi-semidecidable. In: TAMC 2010: 7th annual conference on theory and applications of models of computation. LNCS, vol 6108. Springer, Berlin, pp 397–408
24.
Richardson D (1968) Some undecidable problems involving elementary functions of a real variable. J Symb Log 33:514–520 MATH
25.
Swaminathan M, Fränzle M, Katoen J-P (2008) The surprising robustness of (closed) timed automata against clock-drift. In: 5th Ifip int conf on theoretical comp sc, pp 537–553
26.
Tarski A (1951) A decision method for elementary algebra and geometry. University of California Press, Berkeley. Also in [5] MATH
Metadaten
Titel
Safety verification of non-linear hybrid systems is quasi-decidable
verfasst von
Stefan Ratschan
Publikationsdatum
01.02.2014
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 1/2014
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-013-0196-2

Premium Partner

    Bildnachweise