Safety verification of hybrid systems by constraint propagation-based abstraction refinement

Abstract

This paper deals with the problem of safety verification of nonlinear hybrid systems. We start from a classical method that uses interval arithmetic to check whether trajectories can move over the boundaries in a rectangular grid. We put this method into an abstraction refinement framework and improve it by developing an additional refinement step that employs interval-constraint propagation to add information to the abstraction without introducing new grid elements. Moreover, the resulting method allows switching conditions, initial states, and unsafe states to be described by complex constraints, instead of sets that correspond to grid elements. Nevertheless, the method can be easily implemented, since it is based on a well-defined set of constraints, on which one can run any constraint propagation-based solver. Tests of such an implementation are promising.

References

1. Alur, R., Dang, T., and Ivančić, F. 2002. Reachability analysis of hybrid systems via predicate abstraction. See Tomlin and Greenstreet {2002}.]]
2. Alur, R., Dang, T., and Ivančić, F. 2003. Counter-example guided predicate abstraction of hybrid systems. In TACAS, H. Garavel and J. Hatcliff, Eds. LNCS, vol. 2619. Springer, New York. 208--223.]]
3. Alur, R. and Pappas, G. J., Eds. 2004. Hybrid Systems: Computation and Control. Number 2993 in LNCS. Springer, New York.]]
4. Apt, K. R. 1999. The essence of constraint propagation. Theoretical Computer Science 221, 1--2, 179--210.]]
5. Asarin, E., Dang, T., and Maler, O. 2002. The d/dt tool for verification of hybrid systems. In CAV'02. Number 2404 in LNCS. Springer, New York. 365--370.]]
6. Benhamou, F. 1996. Heterogeneous constraint solving. In Proc. of the Fifth International Conference on Algebraic and Logic Programming. LNCS, vol. 1139. Springer, New York.]]
7. Benhamou, F. and Older, W. J. 1997. Applying interval arithmetic to real, integer and Boolean constraints. Journal of Logic Programming 32, 1, 1--24.]]
8. Benhamou, F., McAllester, D., and Van Hentenryck, P. 1994. CLP(Intervals) revisited. In International Symposium on Logic Programming. MIT Press, Ithaca, NY. 124--138.]]
9. Caviness, B. F. and Johnson, J. R., Eds. 1998. Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, Wien.]]
10. Chutinan, A. and Krogh, B. H. 1999. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. See Vaandrager and van Schuppen {1999}. 76--90.]]
11. Clarke, E., Fehnker, A., Han, Z., Krogh, B., Ouaknine, J., Stursberg, O., and Theobald, M. 2003a. Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. Journal of Foundations of Comp. Science 14, 4, 583--604.]]
12. Clarke, E., Fehnker, A., Han, Z., Krogh, B., Stursberg, O., and Theobald, M. 2003b. Verification of hybrid systems based on counterexample-guided abstraction refinement. In TACAS 2003, H. Garavel and J. Hatcliff, Eds. Number 2619 in LNCS. Springer, New York. 192--207.]]
13. Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2003c. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 50, 5, 752--794.]]
14. Cleary, J. G. 1987. Logical arithmetic. Future Computing Systems 2, 2, 125--149.]]
15. Collins, G. E. and Hong, H. 1991. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation 12, 299--328. Also in Caviness and Johnson {1998}.]]
16. Damm, W., Pinto, G., and Ratschan, S. 2005. Guaranteed termination in the verification of LTL properties of nonlinear robust discrete time hybrid systems. In Proceedings of the Third International Symposium on Automated Technology for Verification and Analysis, D. A. Peled and Y.-K. Tsay, Eds. Number 3707 in LNCS. Springer, New York. 99--113.]]
17. Davis, E. 1987. Constraint propagation with interval labels. Artificial Intelligence 32, 3, 281--331.]]
18. Fehnker, A. and Ivanćić, F. 2004. Benchmarks for hybrid systems verification. See Alur and Pappas {2004}.]]
19. Fränzle, M. 1999. Analysis of hybrid systems: An ounce of realism can save an infinity of states. In Computer Science Logic (CSL'99), J. Flum and M. Rodriguez-Artalejo, Eds. Number 1683 in LNCS. Springer, New York.]]
20. Frehse, G. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. See Morari and Thiele {2005}.]]
21. Girard, A. 2005. Reachability of uncertain linear systems using zonotopes. See Morari and Thiele {2005}.]]
22. Henzinger, T. A., Kopke, P. W., Puri, A., and Varaiya, P. 1998. What's decidable about hybrid automata. Journal of Computer and System Sciences 57, 94--124.]]
23. Henzinger, T. A., Horowitz, B., Majumdar, R., and Wong-Toi, H. 2000. Beyond HyTech: hybrid systems analysis using interval numerical methods. See Lynch and Krogh {2000}.]]
24. Hickey, T. and Wittenberg, D. 2004. Rigorous modeling of hybrid systems using interval arithmetic constraints. See Alur and Pappas {2004}.]]
25. Hickey, T. J. smathlib. http://interval.sourceforge.net/interval/prolog/clip/clip/smath/README.%html.]]
26. Hickey, T. J. 2000. Analytic constraint solving and interval arithmetic. In Proceedings of the 27th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. ACM Press, New York. 338--351.]]
27. Hickey, T. J. 2001. Metalevel interval arithmetic and verifiable constraint solving. Journal of Functional and Logic Programming 2001, 7 (Oct.).]]
28. Hickey, T. J., van Emden, M. H., and Wu, H. 1998. A unified framework for interval constraint and interval arithmetic. In CP'98, M. Maher and J. Puget, Eds. Number 1520 in LNCS. Springer, New York. 250--264.]]
29. Hickey, T. J., Ju, Q., and van Emden, M. H. 2001. Interval arithmetic: from principles to implementation. Journal of the ACM 48, 5, 1038--1068.]]
30. Jaulin, L., Kieffer, M., Didrit, O., and Walter, É. 2001. Applied Interval Analysis, with Examples in Parameter and State Estimation, Robust Control and Robotics. Springer, Berlin.]]
31. Kurzhanski, A. and Varaiya, P. 2000. Ellipsoidal techniques for reachability analysis. See Lynch and Krogh {2000}. 202--214.]]
32. Lebbah, Y., Rueher, M., and Michel, C. 2002. A global filtering algorithm for handling systems of quadratic equations and inequations. In Proc. of Principles and Practice of Constraint Programming (CP 2002), P. Van Hentenryck, Ed. Number 2470 in LNCS. Springer, New York.]]
33. Lhomme, O. 1993. Consistency techniques for numeric CSPs. In Proc. 13th Intl. Joint Conf. on Artificial Intelligence. Morgan Kaufmann, San Mateo, CA.]]
34. Lhomme, O., Gotlieb, A., and Rueher, M. 1998. Dynamic optimization of interval narrowing algorithms. Journal of Logic Programming 37, 1--3, 165--183.]]
35. Lynch, N. and Krogh, B., Eds. 2000. Proc. HSCC'00. LNCS, vol. 1790. Springer, New York.]]
36. Mackworth, A. K. 1977. Consistency in networks of relations. Artificial Intelligence 8, 99--118.]]
37. Mitchell, I. and Tomlin, C. J. 2000. Level set methods for computation in hybrid systems. See Lynch and Krogh {2000}. 310--323.]]
38. Morari, M. and Thiele, L., Eds. 2005. Hybrid Systems: Computation and Control. LNCS, vol. 3414. Springer, New York.]]
39. Neumaier, A. 1990. Interval Methods for Systems of Equations. Cambridge Univ. Press, Cambridge.]]
40. Older, W. and Benhamou, F. 1993. Programming in CLP(BNR). In 1st Workshop on Principles and Practice of Constraint Programming.]]
41. Preussig, J., Kowalewski, S., Wong-Toi, H., and Henzinger, T. 1998. An algorithm for the approximative analysis of rectangular automata. In 5th Int. School and Symp. on Formal Techniques in Fault Tolerant and Real Time Systems. Number 1486 in LNCS. Springer, New York.]]
42. Preussig, J., Stursberg, O., and Kowalewski, S. 1999. Reachability analysis of a class of switched continuous systems by integrating rectangular approximation and rectangular analysis. See Vaandrager and van Schuppen {1999}.]]
43. Puri, A. and Varaiya, P. 1995. Driving safely in smart cars. In Proc. of the 1995 American Control Conference. 3597--3599.]]
44. Ratschan, S. 2002. Continuous first-order constraint satisfaction. In Artificial Intelligence, Automated Reasoning, and Symbolic Computation, J. Calmet, B. Benhamou, O. Caprotti, L. Henocque, and V. Sorge, Eds. Number 2385 in LNCS. Springer, New York. 181--195.]]
45. Ratschan, S. 2004. RSolver. http://rsolver.sourceforge.net. Software package.]]
46. Ratschan, S. and She, Z. 2004. Hsolver. http://hsolver.sourceforge.net. Software package.]]
47. Ratschan, S. and She, Z. 2005. Safety verification of hybrid systems by constraint propagation based abstraction refinement. See Morari and Thiele {2005}.]]
48. Stursberg, O. and Kowalewski, S. 1999. Approximating switched continuous systems by rectangular automata. In Proc. European Control Conference. Paper-ID: F1014-4.]]
49. Stursberg, O. and Kowalewski, S. 2000. Analysis of controlled hybrid processing systems based on approximation by timed automata using interval arithmetic. In Proceedings of the 8th IEEE Mediterranean Conference on Control and Automation (MED 2000).]]
50. Stursberg, O., Kowalewski, S., Hoffmann, I., and Preussig, J. 1997. Comparing timed and hybrid automata as approximations of continuous systems. In Hybrid Systems, P. J. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, Eds. Number 1273 in LNCS. Springer, New York. 361--377.]]
51. Stursberg, O., Kowalewski, S., and Engell, S. 2000. On the generation of timed discrete approximations for continuous systems. Mathematical and Computer Models of Dynamical Systems 6, 51--70.]]
52. Tiwari, A. 2003. Approximate reachability for linear systems. In Hybrid Systems: Computation and Control (HSCC), O. Maler and A. Pnueli, Eds. LNCS, vol. 2623. Springer, New York.]]
53. Tiwari, A. and Khanna, G. 2002. Series of abstractions for hybrid automata. See Tomlin and Greenstreet {2002}.]]
54. Tomlin, C. J. and Greenstreet, M. R., Eds. 2002. Hybrid Systems: Computation and Control HSCC. Number 2289 in LNCS.]]
55. Vaandrager, F. and van Schuppen, J., Eds. 1999. Hybrid Systems: Computation and Control---HSCC'99. Number 1569 in LNCS. Springer, New York.]]

Index Terms

• Computer systems organization

  • Dependable and fault-tolerant systems and networks

• Computing methodologies

  • Modeling and simulation

    • Model development and analysis

      • Model verification and validation

• General and reference

  • Cross-computing tools and techniques

    • Performance

• Networks

  • Network performance evaluation