PaperlayerView exact revision on arXiv

Source-linked AI summary

On Synthesis of Timed Regular Expressions

Ziran Wang, Jie An, Naijun Zhan, Miaomiao Zhang, Zhenya Zhang

arXiv:2509.06262v2cs.FLcs.AI

TL;DR

The paper studies synthesis of timed regular expressions consistent with positive and negative real-time behaviors. It proves decidability and proposes a two-step minimal-synthesis method that enumerates and prunes parametric templates before solving SMT timing constraints. Evaluations include generated behaviors and a scheduling case study, with scope limited by excluding renaming and conjunction.

  • Problem

    The paper addresses synthesizing timed regular expressions from observed behaviors when system models may be unavailable, including nondeterministic behaviors that existing deterministic-model methods do not directly handle.

  • Method

    The method enumerates and prunes parametric timed-expression templates, then encodes consistency with positive and negative examples as an SMT formula to solve timing constraints.

  • Results

    The paper proves decidability of the synthesis problem and reports successful synthesis on benchmarks and a scheduling case study.

  • Takeaways & Limitations

    The approach provides a minimal-length synthesis procedure for consistent timed regular expressions over the evaluated generated behaviors and scheduling case study.

  • Takeaways & Limitations

    The method excludes renaming and conjunction, so it may not apply to real-time scheduling models beyond extended timed regular expressions.

Abstract

from arXiv · show

Timed regular expressions serve as a formalism for specifying real-time behaviors of Cyber-Physical Systems. In this paper, we consider the synthesis of timed regular expressions, focusing on generating a timed regular expression consistent with a given set of system behaviors including positive and negative examples, i.e., accepting all positive examples and rejecting all negative examples. We first prove the decidability of the synthesis problem through an exploration of simple timed regular expressions. Subsequently, we propose our method of generating a consistent timed regular expression with minimal length, which unfolds in two steps. The first step is to enumerate and prune candidate parametric timed regular expressions. In the second step, we encode the requirement that a candidate generated by the first step is consistent with the given set into a Satisfiability Modulo Theories (SMT) formula, which is consequently solved to determine a solution to parametric time constraints. Finally, we evaluate our approach on benchmarks, including randomly generated behaviors from target timed models and a case study.

I. INTRODUCTION

The paper addresses learning timed regular expressions from observed real-time behaviors, especially when system models are unavailable and behaviors may be nondeterministic. It establishes decidability and proposes a minimal-length synthesis process based on candidate enumeration, pruning, and SMT solving.

  • Motivation: Unknown models make it difficult to learn formal real-time specifications from observable behaviors of black-box or gray-box systems.Existing scheduling-analysis and pattern-matching work assumes the models are known beforehand.
  • Challenges: Existing learning and synthesis algorithms do not directly handle timed regular expressions involving nondeterministic behaviors, while minimizing regular expressions is itself difficult.The cited deterministic timed-automata subclasses and the PSPACE-completeness of traditional regular-expression minimization motivate a distinct approach.
  • Contributions: The paper proves decidability of synthesizing a timed regular expression consistent with positive and negative timed-word examples using simple timed regular expressions.Consistency requires accepting every positive example and rejecting every negative example.
  • Contributions: Minimal synthesis enumerates untimed parametric timed-expression templates from increasing length and prunes unnecessary candidates.The templates provide the expression structure before timing constraints are determined.
  • Contributions: The second synthesis step encodes consistency constraints into an SMT formula and solves for parametric timing constraints, with termination and correctness established.If no timing solution exists, the process returns to candidate generation.
  • Evaluation: The method is evaluated on randomly generated behaviors from target timed models and a scheduling case study.The case study concerns inferring task parameters relevant to execution-time feasibility under EDF scheduling.

III. PRELIMINARIES

The preliminaries define timed words, timed regular expressions, their semantics, and the measures used for synthesis. They then formalize consistency and minimal synthesis from positive and negative timed examples.

  • Timed words: A timed word is a finite sequence of events paired with nonnegative delay times, while a timed language is a set of timed words.The functions λ and µ extract delay sequences and untimed event sequences, respectively.
  • Timed regular expressions: Timed regular expressions extend ordinary regular expressions with time restrictions on concatenation, disjunction, and Kleene-star expressions.The syntax includes ε, events, time restriction, concatenation, disjunction, and Kleene star.
  • Semantics: A time restriction ⟨φ⟩I limits the total elapsed time of words in the language of φ to interval I.Nested restrictions can constrain both individual delays and sums of delays.
  • Semantics: Erasing time restrictions from a timed regular expression with µ yields a corresponding ordinary regular expression, so different timed expressions can share the same untimed structure.For example, several expressions over σ1 · σ2 have identical µ images despite different timing constraints.
  • Synthesis problems: The synthesis problem seeks a timed regular expression accepting all positive examples and rejecting all negative examples from a finite timed-word set.The minimal synthesis problem additionally requires minimum syntax-tree length.
  • Synthesis problems: The paper measures timed-expression length by the number of nodes in its syntax tree, treating each time restriction as a property of a node.This measure supports comparing candidate expressions for minimal synthesis.

B. Differences from synthesizing regular expressions

Timed regular-expression synthesis differs from untimed synthesis because timing can distinguish words with identical untimed structure, invalidate structural pruning, and make consistency depend on timing constraints. Simple timed expressions and elementary languages provide decidability tools, but expressiveness limitations can prevent a solution even for finite disjoint examples.

  • B. Differences from synthesizing regular expressions: Timing information can make a timed expression reject a word even when its untimed sequence matches, complicating pruning methods inherited from regular-expression synthesis.Negative examples may be rejected because their untimed sequences are unmatched or because their delay times violate the expression's timing restrictions.
  • B. Differences from synthesizing regular expressions: Time restrictions on operations make structurally equivalent regular expressions semantically different, so one concatenation structure cannot be skipped after checking another.For example, (a·b)·c and a·(b·c) constrain timed-word delays differently when each concatenation carries a restriction.
  • B. Differences from synthesizing regular expressions: Unlike untimed regular-expression synthesis, finite disjoint positive and negative sets may still have no consistent TRE because suitable intervals or required operations may be unavailable.Some timed languages require operations such as intersection, which are excluded from the standard TRE considered here.
  • V. DECIDABILITY OF TRE SYNTHESIS PROBLEMS: A simple elementary language captures timed words through tight integer-bounded constraints on sums of consecutive delays, but not every such language is expressible by a timed regular expression.The limitation arises when a delay variable must participate in multiple overlapping constraints, which the TRE syntax does not allow.
  • V. DECIDABILITY OF TRE SYNTHESIS PROBLEMS: If two timed words have the same simple elementary language, no timed regular expression can distinguish them.This equivalence supplies a basis for reasoning about indistinguishability in the synthesis problem.
  • V. DECIDABILITY OF TRE SYNTHESIS PROBLEMS: A solution exists exactly when every positive example is not obscured by the negative examples, and this condition is decidable using finitely many TRE membership decisions.The result follows from bounding corresponding simple timed expressions and testing whether negative examples cover all expressions accepting a positive example.

VI. TRE SYNTHESIS

The minimal-length TRE synthesis procedure replaces infinite interval choices with finitely enumerable parametric structures, then solves timing consistency constraints with SMT. Enumerating these candidates by increasing length guarantees a minimal consistent TRE when a solution is found.

  • VI. TRE SYNTHESIS: Infinite numbers of fixed-length TREs make naïve enumeration impossible, so the method introduces parametric timed regular expressions with interval placeholders.A parametric interval stores integer endpoints and endpoint-inclusion flags, while a placeholder supports further structural enumeration.
  • VI. TRE SYNTHESIS: The number of pTREs of any fixed length is finite, making systematic enumeration possible despite each parametric expression having infinitely many interval instances.Closed pTREs contain no placeholders, and their instances result from assigning values to all parametric intervals.
  • VI. TRE SYNTHESIS: The algorithm enumerates positive-consistent pTREs by increasing syntax-tree length and encodes rejection of all negative examples as an SMT formula.A satisfying assignment determines the parametric timing constraints and yields a TRE recognizing the sample set.
  • VI. TRE SYNTHESIS: Because candidate pTREs are searched in increasing length, the first satisfiable candidate produces a minimal-length TRE.If no solution exists at the current length, enumeration proceeds to the next length.
  • VI. TRE SYNTHESIS: The synthesis procedure combines candidate enumeration with pruning strategies and SMT encoding, with correctness and termination established for the overall process.The SMT constraint can be encoded greedily for each positive-consistent candidate rather than after collecting every candidate of the same length.

B. Enumerating and pruning pTRE

The method enumerates parametric TRE templates by increasing length, then accelerates search through recursive generation and pruning strategies.

  • Minimal TRE synthesis excludes ε, because any pTRE containing it has the semantics of a shorter pTRE without ε.
  • Trivial enumeration: Trivial enumeration generates pTRE structures from placeholders, substitutes alphabet symbols, and retains candidates accepting all positive examples.
  • Recursive Generation with Edge Pruning: Recursive generation constructs closed pTREs by substitution steps rather than length order and checks candidates when they reach the required length.
  • Recursive Generation with Edge Pruning: Edge pruning replaces an edge placeholder with ⟨Σ∗⟩[0,∞) and prunes the edge when this over-approximation fails to accept every positive example.
  • Containment Pruning: Containment pruning stores doomed pTREs and removes newly generated candidates contained by them, but containment checking is PSPACE-complete and potentially expensive.

C. Encoding and solving time restrictions

The second synthesis stage converts candidate pTRE consistency into SMT constraints by analyzing accepting paths and their timing restrictions.

  • SMT solving determines interval instances that reject negative examples while preserving acceptance of positive examples for a pTRE+ candidate.
  • For a negative example matching the untimed expression, each accepting path receives timing constraints, and all paths must be filtered by the synthesized intervals.
  • The method labels expression symbols by syntax-tree positions, builds a Glushkov NFA, and uses accepting paths to represent possible symbol-to-leaf matches.
  • Positive examples contribute disjunctions of accepting-path formulas, whereas negative examples contribute conjunctions of negated path formulas.
  • Theorem 3 states that a consistent TRE instance exists for a pTRE+ candidate if and only if the constructed SMT formula ΦΩ is satisfiable.

VII. EXPERIMENTS AND IMPLEMENTATION.

The authors implemented the synthesis and pruning methods in Python with Z3 and evaluated them through strategy, scalability, and case-study experiments.

  • Implementation: The prototype implements pTRE enumeration, pruning strategies, and timed-constraint encoding in Python 3.8 using Z3 as the SMT solver.
  • Experimental setup: Experiments were conducted on a laptop with an 11th Gen Intel Core i5-11300H processor, four cores, eight logical processors, and 16GB RAM.
  • Evaluation: The evaluation covers comparisons among synthesis strategies, scalability on randomly generated timed words, and a train-gate case study.

A. The Comparison of Strategies

The strategy comparison evaluates pruning methods on randomly generated timed words labeled by a one-clock, full-reset timed automaton.

  • The comparison uses alphabet Σ = {a, b}, delays t ∈ [0, 4), and randomly generated words labeled positive or negative by a timed automaton.
  • About 40% of randomly generated timed words are marked positive, and the synthesized TRE is not required to exactly match the automaton's TRE.
  • Longer examples produce more complex minimal TREs, causing the number of enumerated and verified pTREs to grow exponentially and computational time to increase.
  • Pruning strategies generally outperform trivial enumeration, but sophisticated containment pruning does not necessarily improve search efficiency.
  • Containment checks can offset their pruning benefit because their cost increases as the set of identified pTREs expands.

B. Scalability

The scalability experiments show that synthesis remains feasible, while alphabet size and target-expression length dominate runtime and larger expressions require substantially more examples for exact recovery.

  • Scalability: The scalability experiment varies TRE length from 6 to 9, alphabet size from 2 to 5, and samples positive and negative examples from corresponding timed automata.The time intervals are randomly assigned valid integer bounds, and the resulting TREs are transformed into target timed automata.
  • Scalability: Synthesis completes in reasonable time, but runtime grows strongly with alphabet size and target TRE length while example length has only slight influence.These factors increase the number of parametric TREs enumerated, whereas longer examples exert a smaller effect.
  • Scalability: The synthesized TRE need not equal the target: minimal consistency can yield a shorter expression or different intervals when the examples do not distinguish them.A shorter candidate is rejected only when a negative example belongs to it but not to the target language.
  • Scalability: With fixed example counts, exact target recovery becomes less likely as example length and alphabet size increase because distinguishing negative examples are less likely to appear.The input experiment reports that 300 examples are insufficient for exact matching and that required examples increase significantly with TRE length and alphabet size.
  • Scalability: The input experiment records average runtime and the number of trials producing matching TREs across increasing positive and negative sample counts.The tested counts are 300, 450, 600, and 750 examples for each polarity.

C. Case study

The case studies apply synthesis to parameter extraction and a train-gate model, showing recovery of scheduling parameters and evaluation on a more complex TRE while noting a restricted expression scope.

  • Scheduling case study: The scheduling study samples predefined parametric TRE templates, labels traces accepted by the timed automaton as positive, and uses the remaining traces as negative.It tests example lengths l ≤11, 15, and 19 while synthesizing intervals directly from the templates.
  • Scheduling case study: The scheduling case study recovers p1 = D1 = 8, p2 = 14, D2 − D1 = 12, and D2 = 20 from synthesized intervals.For Template 1 with l ≤11 and nop = 300, the recovery takes 42.4 seconds.
  • Train-gate case study: The train-gate case uses a TRE of length L = 12 over an alphabet of size |Σ| = 5, with events representing train-gate actions.The model includes starts, train approaches, train halts, train entry, and train departure.
  • Case-study scope: The framework was implemented with three pTRE enumeration and pruning strategies, compared experimentally, and evaluated for scalability on sampled timed-automaton behaviors of varying complexity.The case studies complement the benchmark evaluation with parameter-learning and train-gate applications.
  • Limitations: The method excludes renaming and conjunction, so it may not apply to real-time scheduling models beyond extended timed regular expressions.The expressive relationship between timed automata and the restricted expression class remains unclear.

APPENDIX A PROOFS OF LEMMAS AND THEOREMS

The appendix proves structural properties of simple timed regular expressions, showing that their semantics can be represented through action sequences and time constraints and bounding the relevant candidate space.

  • Structural proofs: For a timed word, the semantics of a simple TRE can be expressed as matching its action sequence while satisfying a conjunction of time constraints.The proof establishes this representation inductively over concatenation and interval operations.
  • Structural proofs: Concatenation preserves the semantic representation by combining the constraints of the two components after renaming the second component’s indices.The resulting constraints remain drawn from the constraint set associated with the concatenated timed word.
  • Structural proofs: Applying an interval restriction intersects the underlying simple expression’s language with the additional time constraint.The proof reduces the restricted case to the already established concatenation form.
  • Candidate bound: The number of distinct simple TREs for an n-length timed word is bounded by 2^((n^2+n)/2).This follows from the possible pairwise time constraints over positions in the word.

C. Proof of Lemma 3

The proof of Lemma 3 connects timed-word constraints to simple TREs, establishing bounded acceptance-query complexity and a construction that separates positive examples from negatives when they are not obscured.

  • Proof of Lemma 3: For a timed word, the semantic set formed from all simple TREs contains precisely the words sharing its action sequence and satisfying the relevant time constraints.The construction begins with individual constraints and combines them into the semantic characterization.
  • Query bound: Checking whether any simple TRE distinguishes a timed word from a set of examples requires at most 2^((n^2+n)/2) acceptance queries per word.For m timed words, the bound becomes 2^((n^2+n)/2) · m queries.
  • Proof of Lemma 3: A timed word’s acceptance constraints can be represented by a simple TRE with the same structure and suitably adjusted interval bounds.The proof compares inequalities generated by parsing the word under the target TRE and the corresponding simple TRE.
  • Consistency condition: If every positive example is not obscured by the negative set, selecting one separating simple TRE per positive example and taking their union yields a consistent solution.Conversely, a positive example obscured by a negative example contradicts the existence of any consistent solution.

G. Proof of Lemma 6

Lemma 6 establishes that the candidate-generation procedure enumerates all parametric timed regular expressions of a given length, supporting complete systematic search.

  • G. Proof of Lemma 6: The number of pTREs is finite for every fixed length because each longer expression arises from finitely many shorter expressions through finitely many generation rules.The proof proceeds by induction from length 1 to length k+1.
  • G. Proof of Lemma 6: Expressions containing ε are not minimal because ε-star, ε-concatenation, and ε-union can each be replaced by shorter semantically equivalent structures.These replacements preserve the denoted timed language while reducing pTRE length.
  • G. Proof of Lemma 6: The procedure generates all pTREs by separating structural expansions from terminal event substitutions and rearranging feasible generation sequences.Structural rules are applied first, followed by event-generation rules; commutativity preserves feasibility and yields the same result.
  • G. Proof of Lemma 6: The construction therefore supplies the complete finite candidate space needed for subsequent consistency checking over positive and negative examples.The related consistency argument requires positive examples to have accepting paths and negative examples to have none under the selected interval parameters.
  • G. Proof of Lemma 6: For a pTRE of length k, the generation counts satisfy k = 2a + b + 1, where a counts binary expansions and b counts star expansions.Binary concatenation or union increases length by 2, star increases it by 1, and event substitution leaves length unchanged.
Loading 2509.06262v2…