×

zbMATH — the first resource for mathematics

The algorithmic analysis of hybrid systems. (English) Zbl 0874.68206
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.

MSC:
68Q45 Formal languages and automata
PDF BibTeX XML Cite
Full Text: DOI
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, (), 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, (), 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, (), to appear. Available as · Zbl 1060.68605
[6] Alur, R.; Henzinger, T.A.; Ho, P.-H., Automatic symbolic verification of embedded systems, (), 2-11
[7] Bouajjani, A.; Fernandez, J.-C.; Halbwachs, N., Minimal model generation, (), 197-203 · Zbl 0765.68114
[8] C̆erãns, K., Decidability of bisimulation equivalences for parallel timer processes, (), 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, () · Zbl 0788.68094
[11] Cousot, P.; Halbwachs, N., Automatic discovery of linear constraints among variables of a program, ()
[12] Halbwachs, N., Delay analysis in synchronous programs, (), 333-346
[13] Halbwachs, N.; Proy, Y.-E.; Raymond, P., Verification of linear hybrid systems by means of convex approximations, (), 223-237
[14] Henzinger, T.A.; Ho, P.-H., Model-checking strategies for linear hybrid systems, (), 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, (), 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, (), 264-274
[20] LeVerge, H., A note on Chernikova’s algorithm, ()
[21] Maler, O.; Manna, Z.; Pnueli, A., From timed to hybrid systems, (), 447-484
[22] Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., An approach to the description and analysis of hybrid systems, (), 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, (), 81-94
[26] Puri, A.; Varaiya, P., Decidability of hybrid systems with rectangular differential inclusions, (), 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.