Revisiting Timed Logics with Automata Modalities

TL;DR

This paper demonstrates that certain automata-extended timed logics are as expressive as full versions, with lower computational complexity for satisfiability and model checking, and provides practical translation methods for implementation.

Contribution

It shows that restricted automata-based extensions of MITL and ECL are as expressive as their full counterparts, simplifying analysis and enabling practical verification.

Findings

$ extsf{EMITL}_{0, Infty}$ and $ extsf{EECL}$ are as expressive as $ extsf{EMITL}$.

Satisfiability and model checking are PSPACE-complete for these logics.

Provides translation to diagonal-free timed automata for practical verification.

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.