Folk Theorems on the Determinization and Minimization of Timed Automata

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, On decision problems for timed automata, Bulletin of the European Association for Theoretical Computer Science 87 (2005) 185–190]. © 2006 Elsevier B.V. All rights reserved.

• Type: Conference
• Year: 2003
• Where: FORMATS
• Authors: Stavros Tripakis
• Keywords: Corresponding Decision Problems, Decision Problems, FORMATS 2003, Timed Automata