FORMATS-FTRTFT 2004 START ConferenceManager    

On timed automata with input-determined guards

Deepak D'Souza and Nicolas Tabareau

Presented at Formal Modelling and Analysis of Timed Systems - Formal Techniques in Real-Time and Fault Tolerant System (FORMATS-FTRTFT 2004), Grenoble, France, September 22-24, 2004


We consider a general notion of timed automata with *input-determined* guards and show that they admit a robust logical framework along the lines of [D03], in terms of a monadic second order logic characterisation and an expressively complete timed temporal logic. We then generalize these automata using the notion of recursive operators introduced by Henzinger, Raskin, and Schobbens [HRS98], and show that they admit a similar logical framework. These results hold in the ``pointwise'' semantics. We finally use this framework to show that the real-time logic MITL of Alur et al [AFH96] is expressively complete with respect to an MSO corresponding to an appropriate set of input-determined operators.

START Conference Manager (V2.47.2)