Abstract
Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state systems, and has been recently shown to enhance the effectiveness of the reachability computation techniques for hybrid systems. Given a hybrid system with linear dynamics and a set of linear predicates, the verifier performs an on-the-fly search of the finite discrete quotient whose states correspond to the truth assignments to the input predicates. The success of this approach depends on the choice of the predicates used for abstraction. In this paper, we focus on identifying these predicates automatically by analyzing spurious counter-examples generated by the search in the abstract state-space. We present the basic techniques for discovering new predicates that will rule out closely related spurious counter-examples, optimizations of these techniques, implementation of these in the verification tool, and case studies demonstrating the promise of the approach.
This research was supported in part by ARO URI award DAAD19-01-1-0473, DARPA Mobies award F33615-00-C-1707, NSF award ITR/SY 0121431, and European IST project CC (Computation and Control).
Chapter PDF
Keywords
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
R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.
R. Alur, T. Dang, J. Esposito, Y. Hur, F. Ivančić, V. Kumar, I. Lee, P. Mishra, G. Pappas, and O. Sokolsky. Hierarchical modeling and analysis of embedded systems. Proceedings of the IEEE, 91(1), January 2003.
R. Alur, T. Dang, and F. Ivačić. Reachability analysis of hybrid systems via predicate abstraction. In Hybrid Systems: Computation and Control, Fifth International Workshop, LNCS 2289. Springer-Verlag, 2002.
R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
R. Alur, A. Itai, R.P. Kurshan, and M. Yannakakis. Timing verification by successive approximation. Information and Computation, 118(1):142–157, 1995.
E. Asarin, O. Bournez, T. Dang, and O. Maler. Approximate reachability analysis of piecewise-linear dynamical systems. In Hybrid Systems: Computation and Control, Third International Workshop, LNCS 1790, pages 21–31. 2000.
T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN 2000 Workshop on Model Checking of Software, LNCS 1885. 2000.
S. Cameron. A comparison of two fast algorithms for computing the distance between convex polyhedra. IEEE Transactions on Robotics and Automation, 13(6):915–920, 1997.
A. Chutinan and B.K. Krogh. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In Hybrid Systems: Computation and Control, Second International Workshop, LNCS 1569, pages 76–90. 1999.
E. Clarke, A. Fehnker, Z. Han, B. Krogh, O. Stursberg, and M. Theobald. Verification of hybrid systems based on counterexample-guided abstraction refinement. In Tools and Algorithms for the Construction and Analysis of Systems, 2003.
E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, pages 154–169, 2000.
E.M. Clarke and R.P. Kurshan. Computer-aided Verification. IEEE Spectrum, 33(6):61–67, 1996.
J.C. Corbett, M.B. Dwyer, J. Hatcli., S. Laubach, C.S. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proceedings of 22nd International Conference on Software Engineering. 2000.
P. Cousot and R. Cousot. Abstract interpretation: a uniffied lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM Symposium on Principles of Programming Languages, 1977.
G. Das and D. Joseph. The complexity of minimum convex nested polyhedra. In Canadian Conference on Computational Geometry, 1990.
C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool kronos. In Hybrid Systems III: Verification and Control, LNCS 1066. Springer-Verlag, 1996.
D. Dobkin and D. Kirkpatrick. Determining the separation of preprocessed polyhedra — a unified approach. In Proc. of ICALP’90, pages 400–413, 1990.
H. Edelsbrunner and F.P. Preparata. Minimum polygon separation. Information and Computation, 77:218–232, 1987.
T.A. Henzinger, P. Ho, and H. Wong-Toi. HyTech: the next generation. In Proceedings of the 16th IEEE Real-Time Systems Symposium, pages 56–65, 1995.
G.J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, 1997.
G.J. Holzmann and M.H. Smith. Automating software feature Verification. Bell Labs Technical Journal, 5(2):72–87, 2000.
K. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Springer International Journal of Software Tools for Technology Transfer, 1, 1997.
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the Verification of concurrent systems. Formal Methods in System Design Volume 6, Issue 1, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Dang, T., Ivančić1, F. (2003). Counter-Example Guided Predicate Abstraction of Hybrid Systems. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_15
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive