# Revisiting Timed Logics with Automata Modalities

arXiv: https://arxiv.org/abs/1812.10146 · HTML: https://mlsanity.com/paper/1812.10146/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Dec 2018.

## Built on by (most cited first, 1 of 1)

- [Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete](https://mlsanity.com/paper/2309.00386/) (2023)

## Abstract (arXiv)

It is well known that (timed) ω-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 (mathsfMITL) and Event Clock Logic (mathsfECL). 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 mathsfEMITL0,∞ (adding non-deterministic finite automata modalities into the fragment of mathsfMITL with only lower- and upper-bound constraints) and mathsfEECL (adding automata modalities into mathsfECL) are already as expressive as mathsfEMITL (full mathsfMITL with automata modalities). In particular, the satisfiability and model-checking problems for mathsfEMITL0,∞ and mathsfEECL are PSPACE-complete, whereas the same problems for mathsfEMITL are EXPSPACE-complete. We also provide a simple translation from mathsfEMITL0,∞ to diagonal-free timed automata, which enables practical satisfiability and model checking based on off-the-shelf tools.