Eventual Timed Automata
Deepak D'Souza and Raj Mohan M
IISc-CSA-TR-2005-8
(June 2005) Available formats: [ps] [ps.gz]
Filed on July 1, 2005
Updated on July 4, 2005
We study the class of timed automata obtained using guards based on the operator <>. These automata, which we call Eventual Timed Automata, are a special case of the generic class of ``input determined automata'' studied in [DT04] which were shown to have robust logical properties. It was also shown that the well known timed temporal logic Metric Temporal Logic (MTL) corresponds to the first-order fragment of eventual timed automata. In this paper we show that ETA's form a decidable class of timed automata. This is done in two steps: we first show that the general class of ETA's which allow ``recursion'' can be ``flattened'' to a non-recursive version. We then show how non-recursive ETA's can be decided via a reduction to one-clock alternating timed automata which have been shown to be decidable. We also study the expressiveness of the class of ETA's and show that they compare favourably with other classes in the literature. ETA's are incomparable with timed automata and are strictly more expressive than the class of Event Predicting Automata. Finally we show that class obtained using the dual operator <-> is also decidable, though the two together lead to an undecidable class of languages.
Please bookmark this technical report as http://aditya.csa.iisc.ernet.in/TR/2005/8/.Problems ? Contact techrep@csa.iisc.ernet.in
[Updated at 2009-10-22T06:42Z]