Revisiting Timed Logics with Automata Modalities

Abstract

It is well known that (timed) \(\omega\)-regular properties such as `p holds at every even position' and `p occurs at least three times within the next 10 time units' cannot be expressed in Metric Interval Temporal Logic (\(\mathsf{MITL}\)) and Event Clock Logic (\(\mathsf{ECL}\)). A standard remedy to this deficiency is to extend these with modalities defined in terms of automata. In this paper, we show that the logics \(\mathsf{EMITL}_{0,\infty}\) (adding non-deterministic finite automata modalities into the fragment of \(\mathsf{MITL}\) with only lower- and upper-bound constraints) and \(\mathsf{EECL}\) (adding automata modalities into \(\mathsf{ECL}\)) are already as expressive as \(\mathsf{EMITL}\) (full \(\mathsf{MITL}\) with automata modalities). In particular, the satisfiability and model-checking problems for \(\mathsf{EMITL}_{0,\infty}\) and \(\mathsf{EECL}\) are PSPACE-complete, whereas the same problems for \(\mathsf{EMITL}\) are EXPSPACE-complete. We also provide a simple translation from \(\mathsf{EMITL}_{0,\infty}\) to diagonal-free timed automata, which enables practical satisfiability and model checking based on off-the-shelf tools.