A Logical Characterisation of Event Clock Automata

Abstract

We show that the class of Event Clock Automata [2] admit a logical characterisation via an unrestricted monadic second order logic interpreted over timed words. The result is interesting in that it provides an unrestricted yet decidable logical characterisation of a non-trivial class of timed languages. A timed temporal logic considered earlier in the literature [11] is shown to be expressively complete with respect to the monadic logic.