Abstract
The reachability problem for timed automata is decidable when the coefficients in the guards are rational numbers. We show that the reachability problem is undecidable when the coefficients are chosen from the set \(\left\{ {1,\sqrt 2 } \right\}\). A consequence of this is that the parameter synthesis problem for timed automata with even a single parameter is undecidable. We discuss why such undecidability results arise in timed and hybrid systems, what they mean, and if it is possible to “get around” them.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Alur, R. and Dill, D. 1990. Automata for modeling real-time systems. Proc. 17th ICALP, Lecture Notes in Computer Science 443, Springer-Verlag.
Alur, R., Henzinger, T.A. and Vardi, M.Y. 1993. Parametric Real-time Reasoning, Proceedings of the Twenty-Fifth Annual ACM Symposium on the Theory of Computing.
Hardy, G. H. and Wright, E. M. 1979. An Introduction to the Theory of Numbers, 5th ed. Oxford: Clarendon, p. 30.
Hopcroft, J. E. and Ullman, J. D. 1979. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley.
Puri, A. 1995. Theory of Hybrid Systems and Discrete Event Systems. PhD Thesis, University of California, Berkeley.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Puri, A. An Undecidable Problem for Timed Automata. Discrete Event Dynamic Systems 9, 135–146 (1999). https://doi.org/10.1023/A:1008319830371
Issue Date:
DOI: https://doi.org/10.1023/A:1008319830371