PaperlayerView exact revision on arXiv

Source-linked AI summary

On Synthesis of Metric Interval Temporal Logics

Hsi-Ming Ho, Shankaranarayanan Krishna, Khushraj Madnani

arXiv:2609.01032v1cs.LOcs.AI

TL;DR

MITL passive learning must recover both temporal structure and timing constraints from positive and negative traces. The paper synthesises timing features, injects them as Boolean propositions, and delegates the resulting untimed problem to LTL learning. It proves soundness, completeness, and progress, and reports practical evaluation across real-time-system scenarios.

  • Problem

    MITL learning requires choosing both nested formula structure and interval parameters, beyond the capabilities of restricted existing passive-learning approaches.

  • Method

    The framework detects timing collisions, synthesises layered timed features, injects them as atomic propositions, and applies untimed LTL learning with proposition minimisation.

  • Results

    The framework is sound and complete: when the timed sample has a solution, the phases yield a separating MITPPL formula.

  • Takeaways & Limitations

    The reduction makes timed specification mining compatible with untimed LTL learners while preserving the timing distinctions captured by synthesized features.

Abstract

from arXiv · show

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.

I. INTRODUCTION

The paper addresses the difficulty of learning precise MITL specifications when timing distinguishes traces that untimed LTL cannot separate. It introduces a feature-engineering reduction to untimed LTL learning and demonstrates the approach on timed-system benchmarks and previously obscured TRE instances.

  • Formal specifications support verification, runtime monitoring, and testing of real-time and cyber-physical systems, but manually writing them is complex and error-prone.
  • MITL learning requires selecting both a temporal structure and integer-bounded interval parameters, making it harder than untimed LTL learning.
  • Untiming traces and applying an LTL learner fails when positive and negative traces have identical untimed projections.No untimed LTL formula can distinguish traces with the same proposition sequence.
  • The framework detects quantitative distinguishability through pivots, which certify that inter-event delays lie on opposite sides of an integer boundary.Formulas such as F[0,c] p are synthesized from these timing differences as separating features.
  • Synthesized MITL features are injected as fresh atomic propositions until every positive-negative pair is propositionally distinguishable, enabling untimed LTL learning after delays are discarded.The feature-engineering pass is guaranteed to make progress on every iteration.
  • The framework includes formal characterisations, subset-projection collision detection, fallback Pnueli modalities, soundness and completeness results, and benchmark evaluation.Experiments cover a timed automaton, parameterised cyber-physical-system patterns, and precise timing constants in a train-gate controller, while examining solver scalability and out-of-sample generalisation.
  • The motivating example shows that Boolean evaluations of synthesized timing features separate behaviours around a critical 4 time unit boundary and allow BOLT to resolve an instance beyond the cited TRE method.The framework handles an instance that requires TRE intersection, which the existing synthesis method forbids.

III. PRELIMINARIES

The preliminaries define timed words, projections, MITPPL syntax and semantics, and the passive learning problems that motivate the timed-to-untimed reduction.

  • Timed words and projections: A timed word is a finite sequence of delayed proposition sets, while its untimed projection removes each delay and retains only the symbol sequence.
  • Timed words and projections: Propositional projection restricts each timed or untimed letter to a chosen subset P of atomic propositions.
  • MITL with Past and Pnueli modalities: MITPPL extends temporal logic with timed until and since operators, using integer-bounded intervals and standard derived future and past modalities.
  • MITL with Past and Pnueli modalities: MITPPL semantics evaluate propositions and temporal operators pointwise over timed words, using delays to constrain the relevant interval.
  • Passive untimed LTL learning: Passive untimed LTL learning seeks a formula accepting every positive word and rejecting every negative word, while avoiding literal encodings that overfit.
  • Passive MITPPL learning: Timed MITPPL learning has a solution exactly when the positive and negative timed samples can be separated by a timed automaton; integer scaling handles known rational precision.

IV. THE SYNTHESIS FRAMEWORK

The synthesis framework detects timing-relevant collisions under proposition subsets, extracts integer pivots, and synthesises features whose injection makes untimed learning applicable.

  • The four-phase architecture seeks localised MITPPL features that make positive and negative untimed projections strictly disjoint.
  • Propositional indistinguishability means two traces have identical projected untimed strings, which prevents every untimed LTL formula over that proposition set from distinguishing them.
  • Quantitative distinguishability guarantees a pivot because timed-automaton-separable traces cannot share the same simple elementary language.
  • A pivot is an integer boundary where accumulated inter-event delays of propositionally indistinguishable traces fall on opposite sides.
  • Subset-projection collision detection enumerates proposition subsets and records conflicting trace pairs together with their pivot mismatches.

A. Phase 1: Subset-Projection Collision Detection

Phase 1 deliberately projects traces onto subsets of atomic propositions to expose structural collisions, then extracts timing pivots that explain how conflicting pairs can be separated.

  • The phase outputs conflicting trace pairs and maps each pair to its list of pivots, using a user-specified minimum subset size k.
  • Phase 1 searches restricted proposition subsets so traces that differ only through discarded atomic propositions become propositionally indistinguishable.
  • The algorithm enumerates subsets in decreasing cardinality, projects traces, detects matching positive-negative strings, and extracts one pivot for each ordered event-index pair.
  • The exponential subset factor is often manageable because practical specifications typically use few atomic propositions.
  • Phase 1 runs in O(2^|APorig| · N^2 · ℓ^2) time for N traces of maximum length ℓ.

B. Phase 2: Template Injection

Phase 2 optionally injects a domain-specific temporal template as a Boolean feature, removing trace pairs it distinguishes before further synthesis. Template evaluation uses sliding-window dynamic programming with linear-time processing in trace length and arity-dependent space.

  • Template Injection: An optional structural template is evaluated across every trace and injected into the atomic-proposition set as a Boolean feature.Pairs distinguished by the template are removed from the unresolved set.
  • Template Injection: Template injection acts as a structural pre-filter, using domain knowledge such as eventual completion after every arrival.The template is intended to accelerate resolution of known specification patterns.
  • Template Evaluation: For features of the form F[0,c] ϕ′, Boolean satisfaction values at all positions can be computed in O(ℓ·k) time and O(k) auxiliary space.Here, ℓ is trace length and k is the Pnueli arity described in the supplied passages.
  • Template Evaluation: The evaluation maintains a backward dynamic-programming state and retreats a right boundary to enforce the strict time-window constraint.The Pnueli modality holds when the earliest valid matching position lies within the maintained boundary.
  • Complexity: For an MITPPL formula with m temporal operators and maximum Pnueli arity k, membership at all positions takes O(ℓ·m·k) time and O(m·(ℓ+k)) space.This extends the feature-evaluation bound compositionally across temporal operators.

C. Phase 3: Layered Feature Synthesis as Set Cover

Phase 3 synthesises timed features for unresolved positive-negative pairs and selects them greedily as a set-cover problem. Layered feature reuse, global scoring, and a progress guarantee support expressive synthesis while ensuring that unresolved pairs decrease.

  • Set-Cover Synthesis: Candidate features are selected greedily to cover unresolved trace pairs, using each feature’s distinguishing set as a set in a classical set-cover formulation.The process continues until no unresolved pair remains.
  • Layered Synthesis: Layered synthesis lets later features use previously injected features, enabling complex nested timing constraints to be expressed incrementally.This avoids requiring every constraint to be represented as one monolithic formula.
  • MITL Features: Standard MITL candidates are generated from integer timing pivots and evaluated across all trace positions.Strict [0,c) intervals are used when the larger delay equals c.
  • Pnueli Features: When standard candidates fail, bounded subwords are compared to extract a shortest distinguishing subsequence for a Pnueli feature.Breadth-first search solves this SDS problem in O(|w+|·|w−|·|Σ_AP|) time, and the resulting feature is guaranteed to distinguish the pair.
  • Expressiveness: Unilateral [0,u⟩ MITL and Pnueli features retain full MITPPL expressiveness because the downstream LTL learner can compose them into equivalent complex modalities.No user-supplied templates are required for this expressiveness guarantee.
  • Candidate Scoring: Global scoring evaluates distinguishing power across the dataset and can target unresolved pairs, historical collisions, or all positive-negative pairs.Tie-breaking favors features grounded in original propositions and then shorter formulas.
  • Termination: The progress rule chooses a candidate covering at least one unresolved pair, so the undone-pair count strictly decreases and the loop terminates within |Pairsconf| iterations.This guarantee holds because each selected feature removes at least one unresolved pair.

D. Phase 4: Proposition Minimisation

Phase 4 minimises the expanded proposition set by reducing feature selection to set cover. The retained propositions preserve pairwise distinguishability, allowing direct untimed LTL learning after timing is discarded.

  • Proposition Minimisation: Greedy Phase 3 may produce redundant features, so Phase 4 minimises the expanded atomic-proposition set.A feature can become obsolete when later features collectively cover the pairs it distinguished.
  • Algorithm: Algorithm 3 repeatedly adds a selected feature to AP and removes the pairs in its undone distinguishing set until no unresolved pair remains.The algorithm outputs the updated proposition set after this iterative reduction.
  • Set Cover: Phase 4 defines each proposition’s distinguishing set over the universal set of originally conflicting trace pairs and solves the resulting set-cover instance.Exact Petrick minimisation or an approximate greedy hitting-set algorithm can be used.
  • Untimed Reduction: The final projections discard timing data but remain strictly distinct over the minimised proposition set, enabling an off-the-shelf LTL learner to process them directly.The timed constraints are retained through the injected propositions before projection.

V. THEORETICAL ANALYSIS

The theoretical analysis establishes soundness, completeness, termination, and computational bounds for reducing timed synthesis to untimed LTL learning. Under inherent distinguishability, the framework returns a valid separating formula exactly when a timed automaton can separate the sample.

  • Assumptions: The analysis assumes every positive-negative trace pair is either propositionally or quantitatively distinguishable.This is the stated inherent-distinguishability condition for the sample.
  • Soundness: Phase 3 restores propositional distinguishability for all conflicting pairs, and Phase 4 preserves this property in the final proposition set.Every conflicting pair has distinct untimed projections after minimisation.
  • Soundness: The resulting untimed sample can be separated by an LTL formula, which is lifted through the synthesised features to an MITPPL formula over the original propositions.This establishes the reduction from timed synthesis to untimed LTL learning.
  • Completeness: Completeness guarantees that if the instance has a solution, applying Phases 1–4 also yields a separating solution.The framework therefore does not lose solvable instances through its staged construction.
  • Expressiveness: A finite timed-word sample is solvable exactly when it can be distinguished by a timed automaton.For finite collections of timed words, the general expressiveness gap between timed automata and MITPPL disappears.
  • Complexity: The framework runs in O((N + 2^|AP|)·N^4·ℓ^4) time on samples with maximum trace length ℓ and post-Phase-3 proposition set AP.The stated bound aggregates the phase costs under the paper’s parameters.

VI. IMPLEMENTATION AND EXPERIMENTAL EVALUATION

The framework is implemented as a Python toolchain with dedicated synthesis components and an untimed LTL backend, then evaluated across three benchmark settings.

  • The implementation combines subset-projection collision detection, template injection, layered feature synthesis, and proposition minimisation.
  • BOLT serves as the downstream untimed LTL learning backend, while WORDGEN and MIGHTYPPL support timed-word generation and automaton conversion.
  • The evaluation covers a simple timed automaton, CPS specification patterns with domain-knowledge templates, and a train-gate controller with unknown timing constants.

A. A Simple Timed Automaton

The simple timed-automaton benchmark uses balanced positive and negative traces at several lengths and compares the framework with reported reference timings. The approach efficiently synthesises separating formulas while trading proposition count against formula complexity.

  • Positive and negative traces use lengths ℓ∈{6, 7, 8, 9, 10}, expected event delay 2, and balanced sets with |Ω+| = |Ω−| = N for N∈{5, 7, 9, 11, 13, 15}.
  • The timing comparison is reference-only rather than head-to-head because the methods, hardware, and running environments differ.
  • The toolchain efficiently synthesises separating MITPPL formulae that resolve entirely to standard MITL on this benchmark.
  • 8.63 average operators with subset projection versus 9.90 without shows that the strategy adds minor runtime overhead while producing more concise specifications.
  • Table I reports the execution time from [42] first and the framework’s execution time second in each divided cell.

B. Standard Patterns in CPS

The CPS-pattern and train-gate evaluations examine runtime, structural complexity, scalability, and generalisation, including the effects of template injection, subset projection, and proposition minimisation.

  • Benchmark design: The CPS-pattern benchmark evaluates scalability across four representative MITL formulae and trace lengths from 5 to 20, using N = 40 traces per class.Templates corresponding to the target structures are injected before the main synthesis loop for comparison.
  • Template injection: Template injection supplies domain-specific structural features before synthesis, while Tables III and IV compare execution times with and without those templates.The reported comparisons cover configurations both without and with subset projection.
  • CPS-pattern results: Subset projection reduces the average operator count for the CPS patterns from 11.44 to 8.88.The paper presents the reduction as a concision benefit and notes that templates act as pre-computed selective features when domain knowledge is available.
  • Train-gate case study: The train-gate case study learns timing constants from positive traces of the original automaton and negatives from a structurally identical automaton with relaxed guards.The setting assumes that the logical behaviour shape is known while integer time boundaries are learned from traces.
  • Train-gate results: Proposition minimisation can provide up to a 2× performance boost, while subset projection reduces average train-gate formula size from 37.25 to 36.83 when minimisation is disabled.The speed benefit is reported alongside increased formula complexity from minimisation.
  • Scalability and limitations: Feature synthesis and proposition minimisation finish in roughly 9 minutes for up to 750 traces, but downstream BOLT times out at 300 or more traces without minimisation and scales to 600 with it.The bottleneck is BOLT's exact structural search over an exponentially large space; minimisation compresses that search space.
  • Generalisation and formula quality: For shorter traces, extracted timing features consistently match exact internal guards such as 2, 3, 7, and 12 as the sample size increases.For longer traces, larger constants such as 24, 36, and 62 capture accumulated delays across repeated structural loops, with accuracy evaluated on 10,000 unseen traces.

VII. RELATED WORK

The related work spans active and passive timed-automata learning, untimed LTL mining, parameter synthesis, and template-free structure synthesis. The paper separates timing from logical structure to delegate combinatorial search to optimized untimed LTL tools while retaining MITPPL expressiveness.

  • Automata learning: Timed-automata learning is divided into active approaches using oracle queries and passive approaches using supplied positive and negative traces.Passive methods include state-merging, SMT-based constraint solving, and learning deterministic real-time automata.
  • Untimed LTL learning: Untimed LTL mining has mature tools, including Texada for full LTL and specialized or accelerated systems such as SCARLET, GPU-based methods, and BOLT.These tools motivate delegating untimed formula search to existing implementations.
  • Parameter and structure synthesis: Parameter-synthesis methods commonly assume a predefined formula structure and optimize numerical time bounds or signal thresholds.Such methods are often formulated as statistical optimization over robustness semantics.
  • Parameter and structure synthesis: Template-free structure synthesis addresses a larger search space but faces scalability or expressiveness limits in timed regular expressions and monolithic SMT encodings.The cited TRE method restricts the fragment, while the MTL approach jointly encodes syntax and continuous monitoring semantics.
  • Comparison to this approach: The proposed framework separates timed-feature extraction from untimed structural learning, avoiding monolithic SMT encoding and template enumeration while retaining MITPPL expressiveness.Quantitative timing differences become atomic propositions, allowing optimized untimed LTL tools to perform the combinatorial search.
  • Comparison to this approach: The framework combines collision detection, template injection, layered feature synthesis, and proposition minimization with soundness, progress, and completeness guarantees.The conclusion also reports efficiency and practical utility across diverse real-time scenarios.
  • Open limitation: The current approach requires both positive and negative examples to extract separating timing pivots and mathematically bound the learned specification.Future work proposes positive-only learning through one-class classification and alternative feature objectives.

APPENDIX

The appendix presents synthesized formulae for multiple trace-length settings, with rows or entries organized around lengths such as 25, 50, 75, and 100. The displayed formulae illustrate the generated MITL expressions, but the supplied excerpts do not state a concise numerical comparison or interpretation.

  • Formula synthesis comparison: The appendix compares formulae synthesized with and without proposition minimization.The appendix heading explicitly labels these two conditions, although the supplied excerpts do not provide a compact summary of their relative sizes or performance.
  • Formulae by trace length: The appendix lists additional long synthesized formulae for trace-length settings 75 and 100 under the displayed comparison.The excerpts show nested bounded-eventually operators and other temporal constructions, but do not state an outcome beyond presenting the formulae.
  • Interpretive boundary: The supplied appendix excerpts contain formula fragments rather than an explicit result statement about proposition minimization.Accordingly, no performance or formula-size claim is supported by these passages alone.
  • Formula syntax: The displayed expressions use bounded temporal intervals such as [0,25], [0,29], [0,42], and [0,40].These intervals occur within the synthesized formulae shown for the appendix entries.
Loading 2609.01032v1…