Undecidable Problems About Timed Automata

We solve some decision problems for timed automata which were raised by S. Tripakis in [Tri04] and by E. Asarin in [Asa04]. In particular, we show that one cannot decide whether a given timed automaton is determinizable or whether the complement of a timed regular language is timed regular. We show that the problem of the minimization of the number of clocks of a timed automaton is undecidable. It is also undecidable whether the shuffle of two timed regular languages is timed regular. We show that in the case of timed B

• Type: Conference
• Year: 2006
• Where: FORMATS
• Authors: Olivier Finkel
• Keywords: Formal Methods, FORMATS 2006, Timed Automata, Timed Automaton, Timed Regular Languages