Formal Methods in System Design

, Volume 42, Issue 2, pp 175–192 | Cite as

An approximation algorithm for box abstraction of transition systems on real state spaces

  • Kunihiko Hiraishi
  • Koich Kobayashi


Predicate abstraction is a powerful technique for extracting finite-state models from infinite-state systems such as computer software, and is applied to verification of safety properties. Predicate abstraction is also applied to verification of dynamical systems on real state spaces such as hybrid dynamical systems. In this paper, we propose a fast algorithm for computing entire abstract state spaces of transition systems on real state spaces. The method is based on the box abstraction of state spaces, and requires a relatively smaller number of reachability checks and Boolean operations. We also propose a fast method for computing the set of boxes that intersect a given convex polyhedron. This computation is a part of the proposed state-space generation algorithm. Effectiveness of the algorithm is evaluated by the computation time and by the difference of the approximated state space from the exact state space.


Hybrid dynamical systems Predicate abstraction Safety verification 



The research is partly supported by the Grant-in-Aid for Scientific Research of the Ministry of Education, Science, Sports and Culture of Japan, under Grant Nos. 21500009 and 20760278, and also by the Mitsutoyo Association for Science and Technology.


  1. 1.
    Alur R et al. (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138:3–34 MathSciNetMATHCrossRefGoogle Scholar
  2. 2.
    Guèhuen H, Lefebvre M, Zaytoon J, Nasri O (2009) Safety verification and reachability analysis for hybrid systems. Annu Rev Control 33:25–36 CrossRefGoogle Scholar
  3. 3.
    Alur R, Henzinger TA, Ho P-H (1996) Automatic symbolic verification of embedded systems. IEEE Trans Softw Eng 22:181–201 CrossRefGoogle Scholar
  4. 4.
    Larsen KG, Petterson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transf 1(1–2):134–152 MATHCrossRefGoogle Scholar
  5. 5.
    Yovine S (1997) Kronos: a verification tool for real-time systems. Int J Softw Tools Technol Transf 1(1–2):123–133 MATHCrossRefGoogle Scholar
  6. 6.
    Bjørner N, Manna Z, Sipma H, Utribe T (1997) Deductive verification of real-time systems using STeP. In: Proc international AMAST workshop in real-time systems. Lecture notes in computer science, vol 1231, pp 22–43 Google Scholar
  7. 7.
    Chutinan A, Krough BH (2003) Computational techniques for hybrid system verification. IEEE Trans Autom Control 48(1):64–75 CrossRefGoogle Scholar
  8. 8.
    Asarin E, Bournez O, Dang T, Maler O (2000) Approximate reachability analysis of piecewise linear dynamical systems. In: Proc 3rd int workshop on hybrid systems: computation and control. Lecture notes in computer science, vol 1790, pp 21–31 Google Scholar
  9. 9.
    Alur R, Henzinger TA, Lafferriwre G, Pappas GJ (2000) Discrete abstraction of hybrid systems. Proc IEEE 88(7):971–984 CrossRefGoogle Scholar
  10. 10.
    Alur R, Dang T, Ivanc̆ić F (2002) In: Reachability analysis of hybrid systems via predicate abstraction 5th international workshop on hybrid systems: computation and control. Lecture note in computer science, vol 2289, pp 35–48 CrossRefGoogle Scholar
  11. 11.
    Alur R, Dang T, Ivanc̆ić F (2006) Counterexample-guided predicate abstraction of hybrid systems. Theor Comput Sci 354:250–271 MATHCrossRefGoogle Scholar
  12. 12.
    Geyer T, Torrisi FD, Morari M (2004) Optimal complexity reduction of piecewise affine models based on hyperplane arrangement. In: Proc 2004 American control conference, pp 1190–1195 Google Scholar
  13. 13.
    Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Transactions on Embedded Computing Systems 6(1): Article No. 8 Google Scholar
  14. 14.
    Clarke EM Jr., Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge Google Scholar
  15. 15.
    Lenstra HW (1981) Integer programming with a fixed number of variables. Math Oper Res 8:538–548 MathSciNetCrossRefGoogle Scholar
  16. 16.
    De Loera JA, Hemmecke R, Tauzer J, Yoshida R (2003) Effective lattice point counting in rational convex polytopes. J Symb Comput 38:1273–1302 CrossRefGoogle Scholar
  17. 17.
    Hertel S, Mäntylä M, Mehlhorn K, Nievergelt J (1984) Space sweep solves intersection of convex polyhedra. Acta Inform 21:501–519 MathSciNetMATHCrossRefGoogle Scholar
  18. 18.
  19. 19.
  20. 20.
    Hiraishi K (2006) KCLP-HS: a rapid prototyping tool for implementing algorithms on hybrid systems. JAIST research report IS-RR-2006-012 Google Scholar

Copyright information

© Springer Science+Business Media New York 2012

Authors and Affiliations

  1. 1.School of Information ScienceJapan Advanced Institute of Science and TechnologyIshikawaJapan

Personalised recommendations