×
Alur, R.; Courcoubetis, C.; Halbwachs, N.; Henzinger, T. A.; Ho, P.-H.

The algorithmic analysis of hybrid systems. (English) Zbl 0874.68206

Theor. Comput. Sci. 138, No. 1, 3-34 (1995).
Summary: We present a general framework for the formal specification and algorithmic analysis of hybrid systems. A hybrid system consists of a discrete program with an analog environment. We model hybrid systems as finite automata equipped with variables that evolve continuously with time according to dynamical laws. For verification purposes, we restrict ourselves to linear hybrid systems, where all variables follow piecewise-linear trajectories. We provide decidability and undecidability results for classes of linear hybrid systems, and we show that standard program-analysis techniques can be adapted to linear hybrid systems. In particular, we consider symbolic model-checking and minimization procedures that are based on the reachability analysis of an infinite state space. The procedures iteratively compute state sets that are definable as unions of convex polyhedra in multidimensional real space. We also present approximation techniques for dealing with systems for which the iterative procedures do not converge.

Cited in 164 Documents

MSC:

68Q45 Formal languages and automata

Keywords:

hybrid systems; finite automata
PDF BibTeX XML Cite
\textit{R. Alur} et al., Theor. Comput. Sci. 138, No. 1, 3--34 (1995; Zbl 0874.68206)
Full Text: DOI
  • logo of hbz
  • logo of WorldCat

References:

[1] Alur, R.; Courcoubetis, C.; Dill, D. L., Model checking in dense real time, Inform. and Comput., 104, 2-34 (1993) · Zbl 0783.68076
[2] Alur, A.; Courcoubetis, C.; Dill, D.; Halbwachs, N.; Wong-Toi, H., Minimization of timed transition systems, (Cleaveland, W. R., CONCUR 92: Theories of Concurrency. CONCUR 92: Theories of Concurrency, Lecture Notes in Computer Science, Vol. 630 (1992), Springer: Springer Berlin), 340-354
[3] Alur, R.; Courcoubetis, C.; Henzinger, T. A.; Ho, P.-H., Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, (Grossman, R. L.; Nerode, A.; Ravn, A. P.; Rischel, H., Workshop on Theory of Hybrid Systems. Workshop on Theory of Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin), 209-229
[4] Alur, R.; Dill, D. L., A theory of timed automata, Theoret. Comput. Sci., 126, 183-235 (1994) · Zbl 0803.68071
[5] Alur, R.; Henzinger, T. A., Real-time system = discrete system + clock variables, (Rus, T., Proc. 1st AMAST Workshop on Real-time Systems. Proc. 1st AMAST Workshop on Real-time Systems, Tech. Report CSD-TR-94-1403 (January 1994), Cornell University), to appear. Available as · Zbl 1060.68605
[6] Alur, R.; Henzinger, T. A.; Ho, P.-H., Automatic symbolic verification of embedded systems, (Proc. 14th Ann. Real-time Systems Symposium (1993), IEEE Computer Soc. Press: IEEE Computer Soc. Press Silver Spring, MD), 2-11
[7] Bouajjani, A.; Fernandez, J.-C.; Halbwachs, N., Minimal model generation, (Clarke, E. M.; Kurshan, R. P., Proc. 2nd Ann. Workshop on Computer-Aided Verification. Proc. 2nd Ann. Workshop on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 531 (1990), Springer: Springer Berlin), 197-203 · Zbl 0765.68114
[8] C̆erãns, K., Decidability of bisimulation equivalences for parallel timer processes, (Bochman, G.v.; Probst, D. K., Proc. 4th Ann. Workshop on Computer-Aided Verification. Proc. 4th Ann. Workshop on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 663 (1992), Springer: Springer Berlin), 269-300
[9] Chaochen, Z.; Hoare, C. A.R.; Ravn, A. P., A calculus of durations, Inform. Processing Lett., 40, 269-276 (1991) · Zbl 0743.68097
[10] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (Proc. 4th Ann. Symp. on Prnciples of Programming Languages (1977), ACM Press: ACM Press New York) · Zbl 0788.68094
[11] Cousot, P.; Halbwachs, N., Automatic discovery of linear constraints among variables of a program, (Proc. 5th Ann. Symp. on Principles of Programming Languages (1978), ACM Press: ACM Press New York)
[12] Halbwachs, N., Delay analysis in synchronous programs, (Courcoubetis, C., Proc. 5th Ann. Conf. on Computer-Aided Verification. Proc. 5th Ann. Conf. on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 697 (1993), Springer: Springer Berlin), 333-346
[13] Halbwachs, N.; Proy, Y.-E.; Raymond, P., Verification of linear hybrid systems by means of convex approximations, (Proc. Internat. Symp. on Static Analysis. Proc. Internat. Symp. on Static Analysis, Lecture Notes in Computer Science, Vol. 818 (1994), Springer: Springer Berlin), 223-237
[14] Henzinger, T. A.; Ho, P.-H., Model-checking strategies for linear hybrid systems, (Presented at the 7th Internat. Conf. on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems. Presented at the 7th Internat. Conf. on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, May 1994. Presented at the 7th Internat. Conf. on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems. Presented at the 7th Internat. Conf. on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, May 1994, Technical Report CSD-TR-94-1437 (July 1994), Cornell University), Available as
[15] Henzinger, T. A.; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model checking for real-time systems, Inform. and Comput., 111, 193-244 (1994) · Zbl 0806.68080
[16] Jaffe, M.; Leveson, N.; Heimdahl, M.; Melhard, B., Software requirements analysis for real-time process-control systems, IEEE Trans. Software Eng., 17, 241-258 (1991)
[17] Kesten, Y.; Pnueli, A.; Sifakis, J.; Yovine, S., Integration graphs: a class of decidable hybrid systems, (Grossman, R. L.; Nerode, A.; Ravn, A. P.; Rischel, H., Hybrid Systems. Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin), 179-208
[18] Lamport, L., A fast mutual-exclusion algorithm, ACM Trans. Comput. Systems, 5, 1-11 (1987)
[19] Lee, D.; Yannakakis, M., Online minimization of transition systems, (Proc. 24th Ann. Symp. on Theory of Computing (1992), ACM Press: ACM Press New York), 264-274
[20] LeVerge, H., A note on Chernikova’s algorithm, (Research Report 635 (February 1992), IRISA)
[21] Maler, O.; Manna, Z.; Pnueli, A., From timed to hybrid systems, (de Bakker, J. W.; Huizing, K.; de Roever, W.-P.; Rozenberg, G., Proc. REX Workshop Real-Time: Theory in Practice. Proc. REX Workshop Real-Time: Theory in Practice, Lecture Notes in Computer Science, Vol. 600 (1992), Springer: Springer Berlin), 447-484
[22] Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., An approach to the description and analysis of hybrid systems, (Grossman, R. L.; Nerode, A.; Ravn, A. P.; Rischel, H., Hybrid Systems. Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin), 149-178
[23] Nicollin, X.; Sifakis, J.; Yovine, S., Compiling real-time specifications into extended automata, IEEE Trans. Software Eng., 18, 794-804 (1992)
[24] Nicollin, X.; Sifakis, J.; Yovine, S., From ATP to timed graphs and hybrid systems, Acta Inform., 30, 181-202 (1993) · Zbl 0790.68067
[25] Olivero, A.; Sifakis, J.; Yovine, S., Using abstractions for the verification of linear hybrid systems, (Dill, D., Proc. 6th Ann. Conf. on Computer-Aided Verification. Proc. 6th Ann. Conf. on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 818 (1994), Springer: Springer Berlin), 81-94
[26] Puri, A.; Varaiya, P., Decidability of hybrid systems with rectangular differential inclusions, (Dill, D., Proc. 6th Ann. Conf. on Computer-Aided Verification. Proc. 6th Ann. Conf. on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 818 (1994), Springer: Springer Berlin), 95-104
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.