An approximation algorithm for box abstraction of transition systems on real state spaces
- 177 Downloads
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.
KeywordsHybrid 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.
- 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
- 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
- 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.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.Clarke EM Jr., Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge Google Scholar
- 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