Abstract
The algorithmic analysis of timed automata is fundamentally limited by the undecidability of the universality problem. For this reason and others, there has been considerable interest in restricted classes of timed automata. In this paper we study the universality problem for two prominent such subclasses: open and closed timed automata. This problem is described as open in [6],[8] in the case of open timed automata. We show here that the problem is undecidable for open timed automata over strongly monotonic time (no two events are allowed to occur at the same time), and decidable over weakly monotonic time. For closed timed automata, we show that the problem is undecidable regardless of the monotonicity assumptions on time. As a corollary, we settle the various language inclusion problems over these classes of timed automata.
The first author was supported by the Defense Advanced Research Project Agency (DARPA) and the Army Research Office (ARO) under contract no. DAAD19-01-1-0485, and the Office of Naval Research (ONR) under contract no. N00014-95-1-0520. The second author was supported by ONR and NSF. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of DARPA, ARO, ONR, NSF, the U.S. Government or any other entity.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
R. Alur, L. Fix, and T. A. Henzinger. Event-clock automata: A determinizable class of timed automata. Theoretical Computer Science, 211:253–273, 1999.
E. Asarin, O. Maler, and A. Pnueli. On discretization of delays in timed automata and digital circuits. In Proceedings of CONCUR 98, volume 1466, pages 470–484. Springer LNCS, 1998.
D. Bosnacki. Digitization of timed automata. In Proceedings of FMICS 99, 1999.
M. Fränzle. Analysis of Hybrid Systems: An ounce of realism can save an infinity of states. In Proceedings of CSL 99, volume 1683, pages 126–140. Springer LNCS, 1999.
V. Gupta, T. A. Henzinger, and R. Jagadeesan. Robust timed automata. In Proceedings of HART 97, volume 1201, pages 331–345. Springer LNCS, 1997.
T. A. Henzinger, Z. Manna, and A. Pnueli. What good are digital clocks? In Proceedings of ICALP 92, volume 623, pages 545–558. Springer LNCS, 1992.
T. A. Henzinger and J.-F. Raskin. Robust undecidability of timed and hybrid systems. In Proceedings of HSCC 00, volume 1790, pages 145–159. Springer LNCS, 2000.
J. Ouaknine and J. B. Worrell. Revisiting digitization, robustness, and decidability for timed automata. Submitted, 2003. Available from http://www.andrew.cmu.edu/~joelo.
J. Ouaknine and J. B. Worrell. Timed CSP = closed timed Automata. Submitted, 2003. Available from http://www.andrew.cmu.edu/~joelo.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ouaknine, J., Worrell, J. (2003). Universality and Language Inclusion for Open and Closed Timed Automata. In: Maler, O., Pnueli, A. (eds) Hybrid Systems: Computation and Control. HSCC 2003. Lecture Notes in Computer Science, vol 2623. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36580-X_28
Download citation
DOI: https://doi.org/10.1007/3-540-36580-X_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00913-9
Online ISBN: 978-3-540-36580-8
eBook Packages: Springer Book Archive