On Synthesis of Metric Interval Temporal Logics

• URL: http://arxiv.org/abs/2609.01032v1
• Date: Tue, 01 Sep 2026 10:30:46 GMT
• Title: On Synthesis of Metric Interval Temporal Logics
• Abstract summary: This paper presents the first framework to tackle emphprecise passive learning for an expressive timed logic.<n>Our approach formally reduces the timed learning problem into a scalable untimed one.<n>We evaluate our implementation across several benchmarks, demonstrating the effectiveness of our approach.
• Score: 0.5505634045241289
• License: http://creativecommons.org/licenses/by/4.0/
• 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 \emph{precise} passive learning for an expressive timed logic, \emph{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

• STAIR: Semantic-Temporal Automaton for Interpretable Reasoning in Temporal Question Answering [7.774935839413563]
  We present STAIR, a textbfSemantic-textbfTemporal textbfAutomaton for textbfInterpretable textbfReasoning.<n>An answer-free LLM adapter maps complex question formulations to normalized temporal intents, while a deterministic temporal automaton executes the corresponding policies over canonicalized evidence.<n> STAIR consistently outperforms strong baselines in the TimeQA-Easy, TimeQA-Hard, TempReason-L2, and TempReason-L3 datasets.
  arXiv  Detail & Related papers  (2026-08-17T07:59:45Z)
• Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions [5.524204636266904]
  Behavior Trees (BTs) are widely adopted for complex task execution in robotics.<n>This letter synthesizes correct-by-construction BTs from Signal Temporal Logic (STL) specifications.
  arXiv  Detail & Related papers  (2026-07-21T05:43:19Z)
• Learning Linear Temporal Specifications from Demonstrations with Uncertainty [0.0]
  We present a framework for learning minimal Linear Temporal Logic formulas from demonstrations with uncertainty.<n>We evaluate our method against state-of-the-art learning approaches and show that it recovers specifications that more closely align with ground-truth formulas under uncertainty.
  arXiv  Detail & Related papers  (2026-07-12T20:43:52Z)
• How LLMs Fail and Generalize in RTL Coding for Hardware Design? [56.361436215029045]
  We introduce a new error taxonomy grounded in problem solvability, inspired by cognitive theory.<n>Our taxonomy categorizes failures into syntactic, semantic, solvable functional, and unsolvable functional types.
  arXiv  Detail & Related papers  (2026-04-26T14:34:49Z)
• Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
  We propose a novel framework for the logical specification of non-Markovian rewards in Decision Processes (MDPs) with large state spaces.<n>Our approach leverages Linear Temporal Logic Modulo Theories over finite traces (LTLfMT)<n>We introduce a method based on reward machines and Hindsight Experience Replay (HER) to translate first-order logic specifications and address reward sparsity.
  arXiv  Detail & Related papers  (2026-02-05T22:11:28Z)
• Fast Controlled Generation from Language Models with Adaptive Weighted Rejection Sampling [90.86991492288487]
  evaluating constraint on every token can be prohibitively expensive.<n> LCD can distort the global distribution over strings, sampling tokens based only on local information.<n>We show that our approach is superior to state-of-the-art baselines.
  arXiv  Detail & Related papers  (2025-04-07T18:30:18Z)
• TLINet: Differentiable Neural Network Temporal Logic Inference [10.36033062385604]
  This paper introduces TLINet, a neural-symbolic framework for learning STL formulas. In contrast to existing approaches, we introduce approximation methods for max operator designed specifically for temporal logic-based gradient techniques. Our framework not only learns the structure but also the parameters of STL formulas, allowing flexible combinations of operators and various logical structures.
  arXiv  Detail & Related papers  (2024-05-03T16:38:14Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
  We study the problem of learning to satisfy temporal logic specifications with a group of agents in an unknown environment. We develop the first multi-agent reinforcement learning technique for temporal logic specifications. We provide correctness and convergence guarantees for our main algorithm.
  arXiv  Detail & Related papers  (2021-02-01T01:13:03Z)
• Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
  We extend implicit learning in PAC-Semantics to handle intervals and threshold uncertainty in the language of linear arithmetic. We show that our implicit approach to learning optimal linear programming objective constraints significantly outperforms an explicit approach in practice.
  arXiv  Detail & Related papers  (2020-10-23T19:08:46Z)
• Temporal Answer Set Programming [3.263632801414296]
  We present an overview on Temporal Logic Programming under the perspective of its application for Knowledge Representation and declarative problem solving. We focus on recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax. In a second part, we focus on practical aspects, defining a syntactic fragment called temporal logic programs closer to ASP, and explain how this has been exploited in the construction of the solver TELINGO.
  arXiv  Detail & Related papers  (2020-09-14T16:13:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.