Affiliations: LSV, ENS Cachan, CNRS, France.
bouyer@lsv.ens-cachan.fr | LSV, ENS Cachan, CNRS, France.
haddad@lsv.ens-cachan.fr | LIF, Université de Provence, CNRS, France.
pierre-alain.reynier@lif.univ-mrs.fr
Note: [] Address for correspondence: LSV, ENS Cachan, 61, avenue du
Président Wilson, 94230 Cachan, France
Abstract: In this work, we study decision problems related to timed automata
with silent transitions (TA_{ϵ}) which strictly extend the expressiveness of timed
automata (TA). We first answer negatively a central question raised by the
introduction of silent transitions: can we decide whether the language
recognized by a TA_{ϵ} can be recognized by some TA? Then we establish in the
framework of TA_{ϵ} some old open conjectures that O. Finkel has recently solved
for TA. His proofs follow a generic scheme which relies on the fact that only a
finite number of configurations can be reached by a TA while reading a timed
word. This property does not hold for TA_{ϵ}, the proofs in the framework of
TA_{ϵ}
thus require more elaborated arguments. We establish undecidability of
complementability, minimization of the number of clocks, and closure under
shuffle. We also show these results in the framework of infinite timed
languages.
