# On Synthesis of Metric Interval Temporal Logics

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 14 of its 44 references that are in the map.
- First posted on arXiv 1 Sep 2026.

## Builds on (most cited first, 14 of 14)

- [Reinforcement Learning With Temporal Logic Rewards](https://mlsanity.com/paper/1612.03471/) (2016)
- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [Transfer of Temporal Logic Formulas in Reinforcement Learning](https://mlsanity.com/paper/1909.04256/) (2019)
- [Interpretable Classification of Time-Series Data using Efficient Enumerative Techniques](https://mlsanity.com/paper/1907.10265/) (2019)
- [Learning Interpretable Temporal Properties from Positive Examples Only](https://mlsanity.com/paper/2209.02650/) (2022)
- [How Effective are Large Language Models in Generating Software Specifications?](https://mlsanity.com/paper/2306.03324/) (2023)
- [Interval Temporal Logic Decision Tree Learning](https://mlsanity.com/paper/2003.04952/) (2020)
- [LTL learning on GPUs](https://mlsanity.com/paper/2402.12373/) (2024)
- [Differentiable Inference of Temporal Logic Formulas](https://mlsanity.com/paper/2208.05440/) (2022)
- [Active learning of timed automata with unobservable resets](https://mlsanity.com/paper/2007.01637/) (2020)
- [Active Learning of One-Clock Timed Automata using Constraint Solving](https://mlsanity.com/paper/2208.00412/) (2022)
- [Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic](https://mlsanity.com/paper/2310.17410/) (2023)
- [On Synthesis of Timed Regular Expressions](https://mlsanity.com/paper/2509.06262/) (2025)
- [LTLf Learning Meets Boolean Set Cover](https://mlsanity.com/paper/2509.24616/) (2025)

## Abstract (arXiv)

Automated mining of formal specifications is vital for verifying real-time systems. However, existing passive learning approaches remain restricted to deterministic specifications or limited fragments of Timed Regular Expressions (TRE). To our knowledge, this paper presents the first framework to tackle precise passive learning for an expressive timed logic, Metric Interval Temporal Logic (MITL) without relying on predefined templates or restricted logic fragments. Our approach formally reduces the timed learning problem into a scalable untimed one. By identifying quantitative timing differences between positive and negative traces, we synthesise precise timed constraints and inject them as new Boolean atomic propositions. This embeds timing into the alphabet, delegating the complex formula evaluation to highly optimised, off-the-shelf untimed LTL tools. Crucially, our framework is complete, guaranteeing a separating specification can always be found. We evaluate our implementation across several benchmarks, demonstrating the effectiveness of our approach.