On Synthesis of Metric Interval Temporal Logics
cs.LO, cs.AI
Submitted: 2026-09-01
Updated: 2026-09-01
Comments: To appear at RTSS 2026
License: http://creativecommons.org/licenses/by/4.0/
The gist: Automated mining of formal specifications is vital for verifying real-time systems.
Terminology
Abstract
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.
Related papers
- Reasoning about Continuous-Variable Quantum Systems
- Formalizing Flag Algebras in Lean
- An Information-Flow Perspective on Explainability Requirements: Specification and Verification
- A programming language combining quantum and classical control
- Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
- Global Convergence of Detailed Balanced Mass Action Systems