zbMATH — the first resource for mathematics

Folk theorems on the determinization and minimization of timed automata. (English) Zbl 1185.68401
Summary: Timed automata are known not to be complementable or determinizable. Natural questions are, then, could we check whether a given TA enjoys these properties? These problems are not algorithmically solvable. Minimizing the “resources” of a TA (number of clocks or size of constants) are also unsolvable problems. In this paper we provide simple undecidability proofs using a “constructive” version of the problems where we require not just a yes/no answer, but also a “witness”. Proofs are then simple reductions from the universality problem. Recent work of Finkel shows that the corresponding decision problems are also undecidable [O. Finkel, Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 87, 185–190 (2005; Zbl 1169.68467)].

68Q45 Formal languages and automata
Full Text: DOI
[1] Finkel, O., On decision problems for timed automata, Bulletin of the European association for theoretical computer science, 87, 185-190, (2005) · Zbl 1169.68467
[2] Tripakis, S., Folk theorems on the determinization and minimization of timed automata, () · Zbl 1099.68648
[3] Alur, R.; Dill, D., A theory of timed automata, Theoretical computer science, 126, 183-235, (1994) · Zbl 0803.68071
[4] Alur, R.; Courcoubetis, C.; Halbwachs, N.; Dill, D.; Wong-Toi, H., Minimization of timed transition systems, (), 340-354
[5] Yannakakis, M.; Lee, D., An efficient algorithm for minimizing real-time transition systems, Formal methods in system design, 11, 2, (1997)
[6] Tripakis, S.; Yovine, S., Analysis of timed systems using time-abstracting bisimulations, Formal methods in system design, 18, 1, 25-68, (2001) · Zbl 0971.68096
[7] Courcoubetis, C.; Yannakakis, M., Minimum and maximum delay problems in real-time systems, () · Zbl 0777.68045
[8] T. Wilke, Automaten und Logiken zur beschreibung zeitabhängiger Systeme, Ph.D. thesis, Institut Für Informatik und Praktische Mathematik, Christian-Albrechts Universität, Kiel, 1994 (in German)
[9] C. Daws, S. Yovine, Reducing the number of clock variables of timed automata, in: Proc. 17th IEEE Real-Time Systems Symposium, RTSS’96, 1996
[10] Springintveld, J.; Vaandrager, F., Minimizable timed automata, (), 130-147
[11] Berard, B.; Petit, A.; Diekert, V.; Gastin, P., Characterization of the expressive power of silent transitions in timed automata, Fundamenta informaticae, 36, 2-3, 145-182, (1998) · Zbl 0930.68077
[12] D’Souza, D.; Madhusudan, P., Timed control synthesis for external specifications, () · Zbl 1054.93502
[13] P. Bouyer, D. D’Souza, P. Madhusudan, A. Petit, Timed control with partial observability, in: CAV’03, 2003 · Zbl 1278.68160
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.