×

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)].

MSC:

68Q45 Formal languages and automata

Citations:

Zbl 1169.68467
PDFBibTeX XMLCite
Full Text: DOI

References:

[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, (Formal Modeling and Analysis of Timed Systems (FORMATS’03). Formal Modeling and Analysis of Timed Systems (FORMATS’03), Lecture Notes in Computer Science, vol. 2791 (2004), Springer: Springer Berlin) · 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, (3rd Conference on Concurrency Theory CONCUR’92. 3rd Conference on Concurrency Theory CONCUR’92, Lecture Notes in Computer Science, vol. 630 (1992), Springer-Verlag: Springer-Verlag Berlin), 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, (CAV’91. CAV’91, Lecture Notes in Computer Science, vol. 575 (1991), Springer: Springer Berlin) · 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); 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; 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, (FTRTFT’96. FTRTFT’96, Lecture Notes in Computer Science, vol. 1135 (1996), Springer: Springer Berlin), 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, (STACS’02. STACS’02, Lecture Notes in Computer Science, vol. 2285 (2002), Springer: Springer Berlin) · Zbl 1054.93502
[13] P. Bouyer, D. D’Souza, P. Madhusudan, A. Petit, Timed control with partial observability, in: CAV’03, 2003; 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.