Top

Published in:

2017 | OriginalPaper | Chapter

Counterexample-Guided Refinement of Template Polyhedra

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

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

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata

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\}\).

For \(M \in \mathbb {R}^{m\times n}\) and \(X \subseteq \mathbb {R}^{n}\), MX denotes the linear transformation \(\{ Mx \mid x \in X\}\).

We exclude the pathological cases of disjoint convex sets w/o separating hyperplane.

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)\).

\(\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)\}\).

GLPK (GNU linear programming kit). www.gnu.org/software/glpk

Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 313–329. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_22 CrossRef

Alizadeh, F., Goldfarb, D.: Second-order cone programming. Math. Program. 95(1), 3–51 (2003)MathSciNetCrossRefMATH

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

Alur, R., Henzinger, T.A., Ho, P.: Automatic symbolic verification of embedded systems. In: RTSS. IEEE Computer Society (1993)

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

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

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

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.

Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31954-2_17 CrossRef

22.

Frehse, G., Bogomolov, S., Greitschus, M., Strump, T., Podelski, A.: Eliminating spurious transitions in reachability with support functions. In: HSCC (2015)

23.

Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_30 CrossRef

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.

McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006). doi:10.1007/11817963_14 CrossRef

33.

MOSEK ApS: The MOSEK C optimizer API manual, Version 7.1 (Revision 53) (2015). http://docs.mosek.com/7.1/capi/

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.

Rockafellar, R.T.: Convex Analysis. Princeton University Press, Princeton (1970)CrossRefMATH

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

Title: Counterexample-Guided Refinement of Template Polyhedra
Authors: Sergiy Bogomolov
Goran Frehse
Mirco Giacobbe
Thomas A. Henzinger
Publisher: Springer Berlin Heidelberg
Book: 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 Year: 2017
DOI: https://doi.org/10.1007/978-3-662-54577-5_34

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner