Revisiting Digitization, Robustness, and Decidability for Timed Automata

We consider several questions related to the use of digitization techniques for timed automata. These very successful techniques reduce dense-time language inclusion problems to discrete time, but are applicable only when the implementation is closed under digitization and the specification is closed under inverse digitization. We show that, for timed automata, the former (whether the implementation is closed under digitization) is decidable, but not the latter. We also investigate digitization questions in connection with the robust semantics for timed automata. The robust modelling approach introduces a timing fuzziness through the semantic removal of equality testing. Since its

• Type: Conference
• Year: 2003
• Where: LICS
• Authors: Joël Ouaknine, James Worrell
• Keywords: Computer Science, Digitization, Digitization Techniques, LICS 2003, Timed Automata