Advertisement

Symbolic Model Checking of Hybrid Systems Using Template Polyhedra

  • Sriram Sankaranarayanan
  • Thao Dang
  • Franjo Ivančić
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)

Abstract

We propose techniques for the verification of hybrid systems using template polyhedra, i.e., polyhedra whose inequalities have fixed expressions but with varying constant terms. Given a hybrid system description and a set of template linear expressions as inputs, our technique constructs over-approximations of the reachable states using template polyhedra. Therefore, operations used in symbolic model checking such as intersection, union and post-condition across discrete transitions over template polyhedra can be computed efficiently using template polyhedra without requiring expensive vertex enumeration.

Additionally, the verification of hybrid systems requires techniques to handle the continuous dynamics inside discrete modes. We propose a new flowpipe construction algorithm using template polyhedra. Our technique uses higher-order Taylor series expansion to approximate the time trajectories. The terms occurring in the Taylor series expansion are bounded using repeated optimization queries. The location invariant is used to enclose the remainder term of the Taylor series, and thus truncate the expansion. Finally, we have implemented our technique as a part of the tool TimePass for the analysis of affine hybrid automata.

Keywords

Hybrid System Taylor Series Expansion Remainder Term Hybrid Automaton Abstract Domain 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Alur, R., Dang, T., Ivančić, F.: Counterexample-guided predicate abstraction of hybrid systems. Theor. Comput. Sci. 354(2), 250–271 (2006)zbMATHCrossRefGoogle Scholar
  2. 2.
    Asarin, E., Dang, T., Maler, O.: The d/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365–370. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Bournez, O., Maler, O., Pnueli, A.: Orthogonal polyhedra: Representation and computation. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 46–60. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  4. 4.
    Boyd, S., Vandenberghe, S.: Convex Optimization. Cambridge University Press, Cambridge (2004), http://www.stanford.edu/~boyd/cvxbook.html zbMATHGoogle Scholar
  5. 5.
    Chutinan, A., Krogh, B.: Computing polyhedral approximations to flow pipes for dynamic systems. In: Proceedings of IEEE CDC, IEEE press, Los Alamitos (1998)Google Scholar
  6. 6.
    Clarisó, R., Cortadella, J.: The Octahedron Abstract Domain. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 312–327. Springer, Heidelberg (2004)Google Scholar
  7. 7.
    Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, Dunod, Paris, France, pp. 106–130 (1976)Google Scholar
  8. 8.
    Dantzig, G.B.: Programming in Linear Structures. In: USAF (1948)Google Scholar
  9. 9.
    Fehnker, A., Ivančić, F.: Benchmarks for Hybrid Systems Verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004)Google Scholar
  10. 10.
    Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 258–273. Springer, Heidelberg (2002)Google Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Halbwachs, N., Proy, Y., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11(2), 157–185 (1997)CrossRefGoogle Scholar
  13. 13.
    Hentenryck, P.V., Michel, L., Benhamou, F.: Newton: Constraint programming over nonlinear real constraints. Science of Computer Programming 30(1-2), 83–118 (1998)zbMATHCrossRefGoogle Scholar
  14. 14.
    Henzinger, T.A.: The theory of hybrid automata. In: Logic In Computer Science (LICS 1996), IEEE Computer Society Press, Los Alamitos (1996)Google Scholar
  15. 15.
    Henzinger, T.A., Ho, P.: HYTECH: The Cornell hybrid technology tool. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999, pp. 265–293. Springer, Heidelberg (1995)Google Scholar
  16. 16.
    Ivančić, F. Modeling and Analysis of Hybrid Systems. PhD thesis, University of Pennsylvania (December 2003)Google Scholar
  17. 17.
    Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for reachability analysis. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 202–214. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  18. 18.
    Lanotte, R., Tini, S.: Taylor approximation for hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 402–416. Springer, Heidelberg (2005)Google Scholar
  19. 19.
    Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  20. 20.
    Mitchell, I., Bayen, A., Tomlin, C.: Computing reachable sets for continuous dynamic games using level set methods. IEEE Transactions on Automatic Control 50(7), 947–957 (2005)CrossRefMathSciNetGoogle Scholar
  21. 21.
    Parillo, P.A.: Semidefinite programming relaxation for semialgebraic problems. Mathematical Programming Ser. B 96(2), 293–320 (2003)CrossRefGoogle Scholar
  22. 22.
    Piazza, C., Antoniotti, M., Mysore, V., Policriti, A., Winkler, F., Mishra, B.: Algorithmic algebraic model checking I: Challenges from systems biology. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 5–19. Springer, Heidelberg (2005)Google Scholar
  23. 23.
    Prajna, S., Jadbabaie, A.: Safety verification using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004)Google Scholar
  24. 24.
    Ratschan, S., She, Z.: Benchmarks for safety verification of hybrid systems. cf. (viewed October, 2007), http://hsolver.sourceforge.net/benchmarks
  25. 25.
    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)Google Scholar
  26. 26.
    Rodriguez-Carbonell, E., Tiwari, A.: Generating polynomial invariants for hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 590–605. Springer, Heidelberg (2005)Google Scholar
  27. 27.
    Sankaranarayanan, S., Dang, T., Ivancic, F.: A policy iteration technique for time elapse over template polyhedra (Extended Abstract). In: HSCC 2008. LNCS, vol. 4981, Springer, Heidelberg (to appear, 2008)Google Scholar
  28. 28.
    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–555. Springer, Heidelberg (2004)Google Scholar
  29. 29.
    Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, Springer, Heidelberg (2005)Google Scholar
  30. 30.
    Silva, B., Richeson, K., Krogh, B.H., Chutinan, A.: Modeling and verification of hybrid dynamical system using checkmate. In: ADPM (2000), http://www.ece.cmu.edu/~webk/checkmate
  31. 31.
    Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 514–525. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  32. 32.
    Tiwari, A., Khanna, G.: Non-linear systems: Approximating reach sets. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Sriram Sankaranarayanan
    • 1
  • Thao Dang
    • 2
  • Franjo Ivančić
    • 1
  1. 1.NEC Laboratories AmericaPrincetonUSA
  2. 2.Verimag, GrenobleFrance

Personalised recommendations