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:
Validation, Synthesis and Optimization for Cyber-Physical Systems Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Counterexample-Guided Refinement of Template Polyhedra

verfasst von : Sergiy Bogomolov, Goran Frehse, Mirco Giacobbe, Thomas A. Henzinger

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

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config
loading …

Abstract

Template polyhedra generalize intervals and octagons to polyhedra whose facets are orthogonal to a given set of arbitrary directions. They have been employed in the abstract interpretation of programs and, with particular success, in the reachability analysis of hybrid automata. While previously, the choice of directions has been left to the user or a heuristic, we present a method for the automatic discovery of directions that generalize and eliminate spurious counterexamples. We show that for the class of convex hybrid automata, i.e., hybrid automata with (possibly nonlinear) convex constraints on derivatives, such directions always exist and can be found using convex optimization. We embed our method inside a CEGAR loop, thus enabling the time-unbounded reachability analysis of an important and richer class of hybrid automata than was previously possible. We evaluate our method on several benchmarks, demonstrating also its superior efficiency for the special case of linear hybrid automata.

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 HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata
Fußnoten
1
For \(X \subseteq \mathbb {R}^{n}\), \({{\mathrm{coni}}}X\) denotes the conical combination \(\{ 0 \} \cup \{ \alpha x \mid \alpha > 0 \wedge x \in X\}\) and for \(Y \subseteq \mathbb {R}^{n}\), \(X \oplus Y\) denotes the Minkowski sum \(\{ x + y \mid x \in X \wedge y \in Y\}\).
 
2
For \(M \in \mathbb {R}^{m\times n}\) and \(X \subseteq \mathbb {R}^{n}\), MX denotes the linear transformation \(\{ Mx \mid x \in X\}\).
 
3
We exclude the pathological cases of disjoint convex sets w/o separating hyperplane.
 
4
The union of the abstractions \(\mathcal {A}_1, \dots , \mathcal {A}_i\) for \(\mathcal {H}\) and resp. the precisions \(\mathsf {prec}_1, \dots , \mathsf {prec}_i\) is the abstraction for \(\mathcal {H}\) and the precision \(\lambda v.\mathsf {prec}_1(v) \cup \dots \cup \mathsf {prec}_i(v)\).
 
5
\(\rho _{X \oplus Y}(d) = \rho _X(d) + \rho _Y(d)\), \(\rho _{MX}(d) = \rho _X(M^\mathsf {T}d)\), and \(\rho _{X \cap Y}(d) = \inf \{ \rho _X(a) + \rho _Y(d-a)\}\).
 
Literatur
1.
2.
3.
4.
Alur, R., Dang, T., Ivančić, F.: Counter-example guided predicate abstraction of hybrid systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 208–223. Springer, Heidelberg (2003). doi:10.​1007/​3-540-36577-X_​15 CrossRef
5.
Alur, R., Henzinger, T.A., Ho, P.: Automatic symbolic verification of embedded systems. In: RTSS. IEEE Computer Society (1993)
6.
Asarin, E., Dang, T., Maler, O., Testylier, R.: Using redundant constraints for refinement. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 37–51. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-15643-4_​5 CrossRef
7.
Bogomolov, S., Frehse, G., Greitschus, M., Grosu, R., Pasareanu, C., Podelski, A., Strump, T.: Assume-guarantee abstraction refinement meets hybrid systems. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 116–131. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-13338-6_​10
8.
Bogomolov, S., Frehse, G., Grosu, R., Ladan, H., Podelski, A., Wehrle, M.: A box-based distance between regions for guiding the reachability analysis of SpaceEx. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 479–494. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-31424-7_​35 CrossRef
9.
Bogomolov, S., Herrera, C., Steiner, W.: Benchmark for verification of fault-tolerant clock synchronization algorithms. In: ARCH (2016)
10.
Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2004)CrossRefMATH
11.
Bu, L., Zhao, J., Li, X.: Path-oriented reachability verification of a class of nonlinear hybrid automata using convex programming. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 78–94. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-11319-2_​9 CrossRef
12.
Chen, X., Ábrahám, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: RTSS (2012)
13.
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). doi:10.​1007/​978-3-642-39799-8_​18 CrossRef
14.
Cimatti, A., Mover, S., Tonetta, S.: A quantifier-free SMT encoding of non-linear hybrid automata. In: FMCAD (2012)
15.
Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14, 583–604 (2003)MathSciNetCrossRefMATH
16.
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). doi:10.​1007/​10722167_​15 CrossRef
17.
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
18.
Dang, T., Salinas, D.: Image computation for polynomial dynamical systems using the Bernstein expansion. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 219–232. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-02658-4_​19 CrossRef
19.
Doyen, L., Henzinger, T.A., Raskin, J.-F.: Automatic rectangular refinement of affine hybrid systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 144–161. Springer, Heidelberg (2005). doi:10.​1007/​11603009_​13 CrossRef
20.
Dreossi, T., Dang, T., Piazza, C.: Parallelotope bundles for polynomial reachability. In: HSCC (2016)
21.
22.
Frehse, G., Bogomolov, S., Greitschus, M., Strump, T., Podelski, A.: Eliminating spurious transitions in reachability with support functions. In: HSCC (2015)
23.
24.
Frehse, G., Kateja, R., Guernic, C.L.: Flowpipe approximation and clustering in space-time. In: HSCC (2013)
25.
Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 540–554. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-02658-4_​40 CrossRef
26.
Henzinger, T.A.: The theory of hybrid automata. In: LICS (1996)
27.
Henzinger, T.A., Ho, P.-H.: A note on abstract interpretation strategies for hybrid automata. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1994. LNCS, vol. 999, pp. 252–264. Springer, Heidelberg (1995). doi:10.​1007/​3-540-60472-3_​13 CrossRef
28.
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)
29.
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: STOC (1995)
30.
Jha, S.K., Krogh, B.H., Weimer, J.E., Clarke, E.M.: Reachability for linear hybrid automata using iterative relaxation abstraction. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 287–300. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-71493-4_​24 CrossRef
31.
Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. (TOCS) 5(1), 1–11 (1987)CrossRef
32.
33.
34.
Ramana, M.V.: An exact duality theory for semidefinite programming and its complexity implications. Math. Program. 77, 129–162 (1997)MathSciNetMATH
35.
Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., Grosu, R.: XSpeed: accelerating reachability analysis on multi-core processors. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 3–18. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-26287-1_​1 CrossRef
36.
37.
Sankaranarayanan, S., Dang, T., Ivančić, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 188–202. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-78800-3_​14 CrossRef
38.
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005). doi:10.​1007/​978-3-540-30579-8_​2 CrossRef
39.
Ben Sassi, M.A., Testylier, R., Dang, T., Girard, A.: Reachability analysis of polynomial systems using linear programming relaxations. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 137–151. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-33386-6_​12 CrossRef
Metadaten
Titel
Counterexample-Guided Refinement of Template Polyhedra
verfasst von
Sergiy Bogomolov
Goran Frehse
Mirco Giacobbe
Thomas A. Henzinger
Copyright-Jahr
2017
Verlag
Springer Berlin Heidelberg
Buch
Tools and Algorithms for the Construction and Analysis of Systems

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

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

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-662-54577-5_34