Abstract
In this paper we present a semi-algorithm to do compositional model-checking for hybrid systems. We first define a modal logic \(L_{\nu}^h\) which is expressively complete for linear hybrid automata. We then show that it is possible to extend the result on compositional model-checking for parallel compositions of finite automata and networks of timed automata to linear hybrid automata. Finally we present some results obtained with an extension of the tool CMC to handle a subclass of hybrid automata (the stopwatch automata).
Chapter PDF
Similar content being viewed by others
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
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense realtime. Information and Computation 104(1), 2–34 (1993)
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science B 137 (January 1995)
Alur, R., Henziger, T.A., Ho, P.H.: Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering 22(3), 181–201 (1996)
Aceto, L., Laroussinie, F.: Is your model checker on time? In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 125–136. Springer, Heidelberg (1999)
Andersen, H.R.: Partial Model Checking. In: Proc. of LICS 1995(1995)
Arnold, A.: Finite Transition System. Prentice Hall, Englewood Cliffs (1994)
Bérard, B., Fribourg, L.: Automated verification of a parametric realtime program: the ABR conformance protocol. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 96–107. Springer, Heidelberg (1999)
Bérard, B., Fribourg, L.: Reachability analysis of (timed) Petri nets using real arithmetic. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 178–193. Springer, Heidelberg (1999)
Bengtsson, J., David Griffioen, W.O., Kristoffersen, K.J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Verification of an audio protocol with bus collision using uppaal. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 244–256. Springer, Heidelberg (1996)
Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: 11th Computer-Aided Verification, Trento, Italy (July 1999)
Bouajjani, A., Tripakis, S., Yovine, S.: On-the-Fly Symbolic Model Checking for Real-Time Systems. In: Proc. of the 18th IEEE Real-Time Systems Symposium, RTSS 1997. IEEE Computer Society Press, Los Alamitos (1997)
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)
Henzinger, T.A.: The theory of hybrid automata. In: Proceedings, 11thAnnual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, July 27-30, pp. 278–292. IEEE Computer Society Press, Los Alamitos (1996)
Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HYTECH: A model checker for hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, p. 460. Springer, Heidelberg (1997)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decida-ble about hybrid automata? Journal of Computer and System Sciences 57(1), 94–124 (1998)
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation 111(2), 193–244 (1994)
Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking (1998); Full version of the Paper: Dill, D.L. (ed.): CAV 1994. LNCS, vol. 818. Springer, Heidelberg (1994) (accepted for publication in J. ACM)
Laroussinie, F., Larsen, K.G.: Compositional Model-Checking of Real Time Systems. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 27–41. Springer, Heidelberg (1995)
Laroussinie, F., Larsen, K.G.: CMC: A tool for compositional model- checking of real-time systems. In: Proc. IFIP Joint Int. Conf. Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV 1998), pp. 439–456. Kluwer Academic Publishers, Dordrecht (1998)
Larsen, K.G., Pettersson, P., Yi, W.: Compositional and symbolic model-checking of real-time systems. In: Proc. of the 16th IEEE Real-Time Systems Symposium, RTSS 1995 (1995)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. Journal of Software Tools for Technology Transfer 1(1/2), 134–152 (1997)
Maler, O., Yovine, S.: Hardware timing verification using KRONOS. In: Proc. 7th Israeli Conference on Computer Systems and Software Engineering, Herzliya, Israel (June 1996)
Yovine, S.: Kronos: A Verification Tool for real-Time Systems. Journal of Software Tools for Technology Transfer 1(1/2), 123–133 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cassez, F., Laroussinie, F. (2000). Model-Checking for Hybrid Systems by Quotienting and Constraints Solving. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_29
Download citation
DOI: https://doi.org/10.1007/10722167_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive