On timed automata with input-determined guards
Deepak D'Souza and Nicolas Tabareau
IISc-CSA-TR-2004-1
(April 2004) Available formats: [ps] [ps.gz]
Filed on May 13, 2004
Updated on May 13, 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.
Please bookmark this technical report as http://aditya.csa.iisc.ernet.in/TR/2004/1/.Problems ? Contact techrep@csa.iisc.ernet.in
[Updated at 2009-10-22T06:42Z]