×
Henzinger, Thomas A.; Kopke, Peter W.; Puri, Anuj; Varaiya, Pravin

What’s decidable about hybrid automata? (English) Zbl 0920.68091

J. Comput. Syst. Sci. 57, No. 1, 94-124 (1998).
Summary: Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify a boundary between decidability and undecidability for the reachability problem of hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow independent trajectories within piecewise- linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves \(\omega\)-languages of initialized rectangular automata with bounded nondeterminism. On the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. In particular, we prove that the reachability problem is undecidable for timed automata augmented with a single stopwatch. \(\copyright\) Academic Press.

Cited in 112 Documents

MSC:

68Q45 Formal languages and automata

Keywords:

hybrid automata model; reachability problem

Software:

HyTech
PDF BibTeX XML Cite
\textit{T. A. Henzinger} et al., J. Comput. Syst. Sci. 57, No. 1, 94--124 (1998; Zbl 0920.68091)
Full Text: DOI Link
  • logo of hbz
  • logo of WorldCat

References:

[1] Alur, R.; Courcoubetis, C.; Halbwachs, N.; Henzinger, T. A.; Ho, P.-H.; Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., The algorithmic analysis of hybrid systems, Theor. Comput. Sci., 138, 3-34 (1995) · Zbl 0874.68206
[2] Alur, R.; Courcoubetis, C.; Henzinger, T. A., Computing accumulated delays in real-time systems, Formal Methods System Design, 11, 137-156 (1997)
[3] Alur, R.; Courcoubetis, C.; Henzinger, T. A.; Ho, P.-H., Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems, Hybrid Systems. Hybrid Systems, Lecture Notes in Computer Science, 736 (1993), Springer-Verlag: Springer-Verlag New York/Berlin, p. 209-229
[4] Alur, R.; Dill, D. L., A theory of timed automata, Theor. Comput. Sci., 126, 183-235 (1994) · Zbl 0803.68071
[5] Alur, R.; Henzinger, T. A.; Ho, P.-H., Automatic symbolic verification of embedded systems, IEEE Trans. Software Eng., 22, 181-201 (1996)
[6] Alur, R.; Henzinger, T. A.; Vardi, M. Y., Parametric real-time reasoning, Proceedings of the 25th Annual Symposium on Theory of Computing (1993), ACM Press: ACM Press New York, p. 592-601 · Zbl 1310.68139
[7] Bouajjani, A.; Echahed, R.; Robbana, R., Verifying invariance properties of timed systems with duration variables, (Langmaack, H.; de Roever, W.-P.; Vytopil, J., FTRTFT 94: Formal Techniques in Real-time and Fault-tolerant Systems. FTRTFT 94: Formal Techniques in Real-time and Fault-tolerant Systems, Lecture Notes in Computer Science, 863 (1994), Springer-Verlag: Springer-Verlag New York/Berlin), 193-210
[8] Bouajjani, A.; Echahed, R.; Sifakis, J., On model checking for real-time properties with durations, Proceedings of the Eighth Annual Symposium on Logic in Computer Science (1993), IEEE Comput. Soc. Press: IEEE Comput. Soc. Press New York, p. 147-159
[9] Bouajjani, A.; Robbana, R., Verifying \(ω\), (Wolper, P., CAV 95: Computer-aided Verification. CAV 95: Computer-aided Verification, Lecture Notes in Computer Science, 939 (1995), Springer-Verlag: Springer-Verlag New York/Berlin), 437-450
[10] Čerans, K., Algorithmic Problems in Analysis of Real-time System Specifications (1992), University of Latvia
[11] Corbett, J. C., Timing analysis of Ada tasking programs, IEEE Trans. Software Eng., 22, 461-483 (1996)
[12] Henzinger, T. A.; Ho, P.-H.; Wong-Toi, H., HyTech, Proceedings of the 16th Annual Real-time Systems Symposium (1995), IEEE Comput. Soc. Press: IEEE Comput. Soc. Press New York, p. 56-65
[13] Henzinger, T. A.; Ho, P.-H.; Wong-Toi, H., HyTech, Software Tools Technology Transfer, 1, 110-122 (1997)
[14] Henzinger, T. A.; Ho, P.-H.; Wong-Toi, H., Algorithmic analysis of nonlinear hybrid systems, IEEE Trans. Automatic Control, 43, 540-554 (1998) · Zbl 0918.93019
[15] Henzinger, T. A.; Manna, Z.; Pnueli, A., What good are digital clocks?, (Kuich, W., ICALP 92: Automata, Languages, and Programming. ICALP 92: Automata, Languages, and Programming, Lecture Notes in Computer Science, 623 (1992), Springer-Verlag: Springer-Verlag New York/Berlin), 545-558 · Zbl 1425.68255
[16] Henzinger, T. A.; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model checking for real-time systems, Inform. & Comput., 111, 193-244 (1994) · Zbl 0806.68080
[17] Halbwachs, N.; Raymond, P.; Proy, Y.-E., Verification of linear hybrid systems by means of convex approximation, (LeCharlier, B., SAS 94: Static Analysis Symposium. SAS 94: Static Analysis Symposium, Lecture Notes in Computer Science, 864 (1994), Springer-Verlag: Springer-Verlag New York/Berlin), 223-237
[18] Ho, P.-H.; Wong-Toi, H., Automated analysis of an audio control protocol, (Wolper, P., CAV 95: Computer-aided Verification. CAV 95: Computer-aided Verification, Lecture Notes in Computer Science, 939 (1995), Springer-Verlag: Springer-Verlag New York/Berlin), 381-394
[19] Henzinger, T. A.; Wong-Toi, H., Using HyTech to synthesize control parameters for a steam boiler, (Abrial, J.-R.; Börger, E.; Langmaack, H., Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control. Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, Lecture Notes in Computer Science, 1165 (1996), Springer-Verlag: Springer-Verlag New York/Berlin), 265-282
[20] Kopke, P. W., The Theory of Rectangular Hybrid Automata (1996), Cornell University
[21] 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, 736 (1993), Springer-Verlag: Springer-Verlag New York/Berlin), 179-208
[22] Lynch, N. A.; Vaandrager, F., Forward and backward simulations, Part II: Timing-based systems, Inform. & Comput., 128, 1-25 (1996) · Zbl 0856.68103
[23] McManis, J.; Varaiya, P., Suspension automata: A decidable class of hybrid automata, (Dill, D. L., CAV 94: Computer-aided Verification. CAV 94: Computer-aided Verification, Lecture Notes in Computer Science, 818 (1994), Springer-Verlag: Springer-Verlag New York/Berlin), 105-117
[24] 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, 736 (1993), Springer-Verlag: Springer-Verlag New York/Berlin), 149-178
[25] Nadjm-Tehrani, S.; Strömberg, J.-E., Proving dynamic properties in an aerospace application, Proceedings of the 16th Annual Real-time Systems Symposium (1995), IEEE Comput. Soc. Press: IEEE Comput. Soc. Press New York, p. 2-10
[26] Olivero, A.; Sifakis, J.; Yovine, S., Using abstractions for the verification of linear hybrid systems, (Dill, D. L., CAV 94: Computer-aided Verification. CAV 94: Computer-aided Verification, Lecture Notes in Computer Science, 818 (1994), Springer-Verlag: Springer-Verlag New York/Berlin), 81-94
[27] Puri, A.; Borkar, V.; Varaiya, P., \(ε\), (Alur, R.; Henzinger, T. A.; Sontag, E. D., Hybrid Systems III. Hybrid Systems III, Lecture Notes in Computer Science, 1066 (1996), Springer-Verlag: Springer-Verlag New York/Berlin), 362-376
[28] Puri, A.; Varaiya, P., Decidability of hybrid systems with rectangular differential inclusions, (Dill, D. L., CAV 94: Computer-aided Verification. CAV 94: Computer-aided Verification, Lecture Notes in Computer Science, 818 (1994), Springer-Verlag: Springer-Verlag New York/Berlin), 95-104
[29] Stauner, T.; Müller, O.; Fuchs, M., UsingHyTech, (Maler, O., HART 97: Hybrid and Real-time Systems. HART 97: Hybrid and Real-time Systems, Lecture Notes in Computer Science, 1201 (1997), Springer-Verlag: Springer-Verlag New York/Berlin), 139-153
[30] Vardi, M. Y.; Wolper, P., An automata-theoretic approach to automatic program verification, Proceedings of the First Annual Symposium on Logic in Computer Science (1986), IEEE Comput. Soc. Press: IEEE Comput. Soc. Press New York, p. 322-331
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.