Abstract
We report on several abstract interpretation strategies that are designed to improve the performance of HyTech, a symbolic model checker for linear hybrid systems. We (1) simultaneously compute the target region from different directions, (2) conservatively approximate the target region by dropping constraints, and (3) iteratively refine the approximation until sufficient precision is obtained. We consider the standard abstract convex-hull operator and a novel abstract extrapolation operator.
This research was supported in part by the National Science Foundation under grant CCR-9200794, by the Air Force Office of Scientific Research under contract F49620-93-1-0056, by the Office of Naval Research under YIP grant N00014-95-1-0520, and by the Defense Advanced Research Projects Agency under grant NAG2-892.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
[ACH+95] R. Alur, C. Coucoubetis, N. Halbwachs, T.A. Henzinger, P.-H. 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, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, Lecture Notes in Computer Science 736, pages 209–229. Springer-Verlag, 1993.
R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. In Proceedings of the 14th Annual Real-time Systems Symposium, pages 2–11. IEEE Computer Society Press, 1993.
[BCM+92] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, California, 1977. ACM Press.
P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2/3):103–179, 1992.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the Fifth Annual Symposium on Principles of Programming Languages. ACM Press, 1978.
P. Cousot. Semantics fundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, pages 303–342. Prentice-Hall, 1981.
N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor, CAV 93: Computer-aided Verification, Lecture Notes in Computer Science 697, pages 333–346. Springer-Verlag, 1993.
T.A. Henzinger and P.-H. Ho. HyTech: The Cornell Hybrid Technology Tool. This volume, 1995.
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.
N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by means of convex approximation. In B. LeCharlier, editor, International Symposium on Static Analysis, SAS'94, Lecture Notes in Computer Science 864, Namur (belgium), September 1994. Springer-Verlag.
G.L. Nemhauser and L.A. Wolsey. Integer and Combinatorial Optimization. Wiley, 1988.
Howard Wong-Toi and David L. Dill. Approximations for verifying timing properties. In Teo Rus and Charles Rattray, editors, Theories and Experiences for Real-Time System Development (Proceedings First AMAST Workshop on Real-Time System Development), chapter 7. World Scientific Publishing, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henzinger, T.A., Ho, PH. (1995). A note on abstract interpretation strategies for hybrid automata. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds) Hybrid Systems II. HS 1994. Lecture Notes in Computer Science, vol 999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60472-3_13
Download citation
DOI: https://doi.org/10.1007/3-540-60472-3_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60472-3
Online ISBN: 978-3-540-47519-4
eBook Packages: Springer Book Archive