Counter-Free Input-Determined Timed Automata

We identify a class of timed automata, which we call counter-free input-determined automata, which characterize the class of timed languages definable by several timed temporal logics in the literature, including MTL [1, 11]. We make use of this characterization to show that MTL satisfies an “ultimate stability” property with respect to periodic sequences of timed words. Our results hold for both the pointwise and continuous semantics. Along the way we generalize the result of McNaughton-Papert [10] to show a counter-free automata characterization of FOdefinable finitely varying functions.

• Type: Conference
• Year: 2007
• Where: FORMATS
• Authors: Fabrice Chevalier, Deepak D'Souza, Pavithra Prabhakar
• Keywords: Counter-free Automata Characterization, Counter-free Input-determined Automata, FORMATS 2007, Timed Words