On Continuous Timed Automata with Input-Determined Guards

Fabrice Chevalier, Deepak D'Souza and Pavithra Prabhakar

We consider a general class of timed automata parameterized by a set of ``input-determined'' operators, in a continuous time setting. We show that for any such set of operators, we have a monadic second order logic characterization of the class of timed languages accepted by the corresponding class of automata. Further, we consider natural timed temporal logics based on these operators, and show that they are expressively equivalent to the first-order fragment of the corresponding MSO logics. As a corollary of these general results we obtain an expressive completeness result for the continuous version of MTL.

Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2006
Download: BIB PS PDF