PaperlayerView exact revision on arXiv

Source-linked AI summary

Mining DTA with SMT by Exploiting Simple Elementary Language and Timed Augmented Prefix Acceptor

Ziran Wang, Jie An, Naijun Zhan

arXiv:2609.16866v1cs.FL

TL;DR

The paper tackles passive mining of deterministic timed automata from positive and negative traces, a challenge for black-box safety-critical systems. It simplifies examples with sEL and tAPTA before SMT-based DTA synthesis, and reports reduced formula complexity and efficient mining on benchmarks and a scheduling case study. The authors note that over-approximation prevents a general minimality guarantee and identify nondeterministic learning as future work.

  • Problem

    Passive DTA mining must infer timed behavior from finite positive and negative traces when black-box systems cannot answer equivalence queries.

  • Method

    The approach preprocesses traces with sEL, incrementally constructs and simplifies a tAPTA, then encodes DTA synthesis as an SMT problem.

  • Results

    The approach significantly reduces encoded SMT-formula complexity and efficiently mines DTAs in randomly sampled benchmarks and a scheduling case study.

  • Takeaways & Limitations

    Trace simplification combines redundancy removal, conflict detection, and timed-language merging before SMT synthesis.

  • Takeaways & Limitations

    Over-approximation prevents the SMT framework from guaranteeing minimality for the full DTA mining problem, and nondeterministic learning requires a distinct encoding scheme.

Abstract

from arXiv · show

Timed automata, which extend finite state automata by introducing clock variables, serve as a popular formalism for specifying and analyzing the timed behaviors of real-time systems. Extracting the timed behaviors of a black-box, safety-critical system is crucial for designing and analyzing its real-time requirements, yet it remains challenging. In this paper, we address this problem by generating a deterministic timed automaton (DTA) consistent with a given set of system behaviors, comprising both positive and negative examples. To this end, we adapt the formalism of simple elementary languages (sEL) and introduce the timed augmented prefix tree acceptor (tAPTA). Our approach proceeds as follows: First, we preprocess samples by translating them into sEL, which discards redundancy and detects conflicts; then, we rewrite the resulting sELs in an incremental form and construct a tAPTA to further simplify the samples; finally, we encode the search for a DTA that accepts the simplified tAPTA as an SMT formula. We evaluate our approach on randomly generated benchmarks and a scheduling case study. The results demonstrate the effectiveness of our simplification method in reducing the size of the encoded SMT formula and the efficiency of our approach in mining a DTA.

I. INTRODUCTION

Mining timed behaviors from black-box safety-critical systems is difficult because passive learning must work from finite traces while SMT encodings of redundant datasets can become intractable. The paper addresses this with sEL-based preprocessing, tAPTA simplification, and SMT-based DTA synthesis.

  • Problem: Passive DTA learning infers models from fixed traces but is sensitive to data quality and quantity, potentially producing over-approximated models.This setting is necessary when equivalence queries are impossible or prohibitively expensive for black-box, legacy, or safety-critical systems.
  • Problem: Directly encoding large redundant trace sets can make SMT constraints computationally intractable, causing solver timeouts or overflow errors.Existing trace-merging strategies are difficult to extend to general DTA because delays must be considered across entire traces.
  • Approach: The approach translates traces into simple elementary languages to remove redundancy and detect conflicts before constructing a timed augmented prefix tree acceptor.The framework then uses an incremental sEL representation to retain accumulated timing constraints at each event.
  • Approach: The simplified tAPTA is encoded as an SMT problem for synthesizing a DTA without losing the expressiveness of normal clock guards.Compared with direct raw-data encoding, the scheme is designed to reduce the computational complexity of synthesis.
  • Evaluation: The work evaluates the implementation against an existing SMT-based DTA synthesis method on randomly generated benchmarks and a scheduling case study.The paper’s stated evaluation scope includes both generated benchmarks and an application case study.

III. OVERVIEW OF DTA MINING

The DTA mining problem seeks an automaton consistent with positive and negative timed examples, while minimal mining seeks one with the fewest states. The proposed workflow preprocesses examples, simplifies them with tAPTA, and searches for a minimal DTA through progressively sized SMT encodings.

  • Problem definition: DTA mining seeks an automaton accepting every positive timed word and rejecting every negative timed word, or reports that no consistent DTA exists.The minimal variant additionally requires the solution to have the least number of states among consistent DTAs.
  • Preprocessing: The workflow first translates traces into sEL, removes redundant examples, and checks for conflicts that make the mining problem unsolvable.If conflicts are found, the set of consistent DTAs is returned as empty.
  • tAPTA simplification: It converts sELs into incremental sequences, constructs a tAPTA, and applies extended merging to simplify the example structure.The incremental representation preserves newly introduced constraints on accumulated delay times at each event.
  • SMT synthesis: The simplified structure is encoded as a minimal-DTA SMT problem for a chosen automaton size, increasing the size after UNSAT until a SAT model yields a DTA.This procedure searches for a consistent automaton through successive size settings.

A. Preprocessing Examples

The preprocessing translates timed traces into simple elementary languages (sELs), preserving their behavior while removing redundancy and detecting conflicts. This produces a simplified, safe representation for subsequent DTA mining.

  • A. Preprocessing Examples: sEL equivalence preserves acceptance by every timed automaton, so traces with the same sEL can be treated identically.This property supports both redundancy removal and conflict detection.
  • A. Preprocessing Examples: The preprocessing removes redundant positive or negative examples when their sEL representations coincide, without changing the consistent automata set.The resulting example sets retain the same DTA solutions and timed-language congruence relation.
  • A. Preprocessing Examples: Matching sEL representations across incompatible labels identify conflicts for which no DTA can satisfy the positive and negative examples.The conflict criterion follows because every timed automaton must classify sEL-equivalent words identically.
  • A. Preprocessing Examples: The translated sets S(Ω) form a safe over-approximation of the original samples, while Theorem 1 preserves both consistent automata and their DTA congruence relations.The paper assumes conflict-free samples after this preprocessing step.
  • A. Preprocessing Examples: sELs replace continuous delay values with integer-bounded intervals, although a timed word can still induce more than wn|Σ|^n possible sELs.The representation is introduced mainly because interval constraints support later simplification.

B. Construction and Simplification of tAPTA

The method rewrites sEL constraints incrementally so each event carries newly introduced accumulated-time conditions, then uses these labeled sequences to construct a timed APTA. This representation preserves event and timing information while enabling prefix-based simplification.

  • B. Construction and Simplification of tAPTA: Each incremental tuple pairs an event with constraints on all delay sums ending at that event.The m-th tuple contains the event σ_m and constraints T_j,m for j=1,…,m.
  • B. Construction and Simplification of tAPTA: For the example trace, the incremental sEL sequence is (a, (1+))(b, (2+, 4+))(a, (0+, 3, 4+)).The ordered constraints encode newly accumulated timing conditions at each successive event.
  • B. Construction and Simplification of tAPTA: The incremental representation converts an elementary language with O(n^2) constraints into a sequential label sequence suitable for prefix construction.Each tuple (σ_m, Λ_m) is treated as one label in an sEL sequence.
  • B. Construction and Simplification of tAPTA: A tAPTA is an APTA whose edges are labeled by incremental event-and-constraint tuples, with states formed from prefixes of positive and negative sEL sequences.The transition combines the prior accumulated constraints with the tuple introduced by the next event.
  • B. Construction and Simplification of tAPTA: Along each tAPTA path, the represented timed language is the elementary language obtained by composing the incremental labels on that path.The state language aggregates the languages of paths reaching the state.

2) Extending States Merging to tAPTA:

The tAPTA simplification extends state merging to transitions carrying timing constraints, then over-approximates merged intervals to reduce encoding complexity. The resulting simplified tAPTA remains a safe over-approximation of the input sELs.

  • 2) Extending States Merging to tAPTA: Extended merging combines equivalent tAPTA states and merges corresponding transitions by disjoining their constraint lists.The merged transition retains branch information and selects the branch matching its sequential position on a path.
  • 2) Extending States Merging to tAPTA: The extended merging operation is safe because it introduces no conflicts between timed languages reaching accepting and rejecting states.Equivalence requires matching acceptance status and recursively equivalent event successors.
  • 2) Extending States Merging to tAPTA: Strict merging avoids over-approximation but permits fewer merges, whereas the extended tAPTA approach preserves more timing information than the cited RTA-mining framework.The comparison concerns simplification flexibility and retained delay-time constraints.
  • 3) Interval Over-approximation for Merged Transitions: After merging, interval over-approximation unions non-overlapping corresponding intervals and the ranges between them to simplify disjunctive transition constraints.Overlapping intervals are left unchanged, while only compatible branches are combined.
  • 3) Interval Over-approximation for Merged Transitions: For a path using an over-approximated transition at position m, only its first m intervals are composed as an over-approximation of a length-m disjunctive branch.The figure example yields (b, (3))(a, ((1, 3), (2, 6))).
  • 3) Interval Over-approximation for Merged Transitions: The interval over-approximation is safe, introducing no conflicts between accepted and rejected timed languages.Together with safe extended merging, this establishes that the simplified tAPTA safely over-approximates the original sELs.

C. Encoding TA Constraints

After simplifying the tAPTA, the method encodes mappings from tAPTA locations and edges to a DTA of specified size as an SMT formula. Satisfiability yields a DTA model, while unsatisfiability triggers a larger state-clock search.

  • C. Encoding TA Constraints: The SMT encoding maps each tAPTA location to a DTA state and each tAPTA edge to corresponding DTA transitions.The target DTA is specified with fixed numbers of states and clocks.
  • C. Encoding TA Constraints: If Φ(P, n, m) is satisfiable, its model is used to construct and return a DTA; if unsatisfiable, the search increases n or m.The formula encodes the intrinsic constraints and state-transition mappings.

1) Basic setting:

The encoding represents a bounded DTA using indexed states, locations, clocks, and transitions, with guards restricted to conjunctions of clock-interval constraints. Intrinsic and language constraints together enforce structural properties and consistency with the tAPTA.

  • 1) Basic setting:: Guards are conjunctions of one interval constraint per clock, with natural lower and upper bounds and a solver cutoff κ representing +∞.The encoding also limits transitions sharing a source, target, and event by E, yielding at most D = n^2E|Σ| transitions.
  • 1) Basic setting:: States, locations, and clocks are integer-indexed, while Boolean and ternary labels mark accepting states and positive or rejecting locations.Each tAPTA edge is represented by its parent, child, and branch information.
  • 1) Basic setting:: Each transition uses source and target states, an event and transition index, clock resets, and lower and upper guard bounds.Guard components specify closed or half-open intervals independently for each clock.
  • 1) Basic setting:: The SMT encoding separates intrinsic constraints on DTA structure from language constraints connecting locations and feasible transitions to the tAPTA.The latter include location-to-state mappings and transition feasibility over tAPTA edges.

2) Intrinsic Constraints:

Intrinsic and feasibility constraints encode determinism, transition limits, location-to-state mappings, and timed-path compatibility. Clock-progress variables and interval-intersection tests determine whether transitions can cover tAPTA paths.

  • 2) Intrinsic Constraints:: Determinism requires guards of transitions sharing a source state and event to be disjoint, while transition multiplicity is bounded for identical source, target, and event combinations.These are encoded as intrinsic structural constraints independent of the particular tAPTA.
  • 2) Intrinsic Constraints:: Accessibility variables map tAPTA locations to DTA states, enforcing accepting and rejecting label consistency, the initial-state mapping, and unique mappings for uniquely reachable locations.A uniquely accessible location cannot map to two different states.
  • 2) Intrinsic Constraints:: Clock-progress vectors track edges since resets, and the pass function tests whether a path interval intersects a transition guard before updating each clock’s progress.Reset clocks return to 1; non-reset clocks increment by one.
  • 2) Intrinsic Constraints:: For every root-to-leaf tAPTA path, the encoding selects feasible interval-list branches and requires at least one compatible transition when multiple branches are possible.The procedure enumerates paths and processes each edge in sequence.
  • 2) Intrinsic Constraints:: Transition-feasibility constraints require mapped tAPTA edges to match a DTA transition’s source, target, event, and guard compatibility across all clocks.The condition is imposed for each path position and relevant location, state, and transition variable.

D. Constructing the Learned TA

The learned TA is obtained by solving the SMT encoding and pruning unused transitions, with theoretical guarantees that the mined DTA is sound and that the search terminates under finite-size enumeration.

  • D. Constructing the Learned TA: After solving Φ(P, n, m), arbitrary solver-induced transitions are removed by simulating positive examples and pruning transitions never traversed.The remaining transitions instantiate the learned automaton without those superfluous assignments.
  • D. Constructing the Learned TA: The mined DTA accepts every positive tAPTA language and rejects every negative tAPTA language, establishing consistency with the simplified sample pair.Lemma 6 states P+ ⊂ L(A(P)) and P− ∩ L(A(P)) = ∅.
  • E. Soundness and Termination: The soundness theorem guarantees that the mined DTA solves the original DTA mining problem by preserving consistency from the tAPTA through sELs to the example set.Mapping constraints handle acceptance labels, while feasibility constraints ensure timed words reach mapped states.
  • E. Soundness and Termination: The approach terminates in finite steps because preprocessing and tAPTA construction are finite and a sufficient DTA size is eventually reached under the specified enumeration order.The required size is bounded by the simplified tAPTA, with state and path-length bounds derived from the examples.
  • E. Soundness and Termination: Without tAPTA simplification, the same search is also guaranteed to terminate and return a solution to the unsimplified problem under an appropriate enumeration order.This establishes termination for the direct encoding of the unsimplified tAPTA as well.

IV. COMPARISON WITH EXISTING WORK

The approach differs from Tappler’s method in its input representation, use of positive and negative traces, trace merging, and guard expressiveness. Experiments compare their encoding size and mining scalability across sample sizes and clock counts.

  • IV. COMPARISON WITH EXISTING WORK: Unlike Tappler’s method, our approach uses input traces with both positive and negative examples, while Tappler uses input-and-output traces and positive samples only.Using negative traces removes the need for additional delay-time assumptions described for Tappler’s approach.
  • IV. COMPARISON WITH EXISTING WORK: Our approach merges timed languages through sEL preprocessing and tAPTA simplification, reducing SMT clauses compared with direct trace encoding.The comparison attributes this reduction to redundancy removal, conflict detection, over-approximation, and merging within the tAPTA.
  • IV. COMPARISON WITH EXISTING WORK: Our encoding supports normal clock constraints, whereas Tappler’s independent-clock restriction allows at most one inequality and one reset per transition.The paper presents this as a difference in guard expressiveness between the two approaches.
  • B. Experiments: Experiments evaluate encoding size, scalability over positive and negative traces, and scheduling-task DTA mining using randomly generated benchmarks and a case study.The evaluation varies target DTAs from 2 to 6 states, 1 to 3 clocks, and 2 to 4 events, with trace sets ranging from 50 to 600 samples.
  • 2) Scalability Tests:: Passive learning may return a simpler DTA than the target when traces are limited, and the number of clocks is the most influential factor in computation time.The paper reports that the mined model may not be isomorphic to the target and can have fewer states or differing guards.

3) Case Study:

The case study mines a DTA from scheduling traces generated for two tasks under a FIFO scheduler, showing that the approach captures task timing constraints while handling closely similar positive and negative examples.

  • 3) Case Study:: The scheduling evaluation uses two tasks with configured execution, deadline, and interarrival parameters, generating traces through stochastic task triggering and FIFO scheduling.The dataset contains 600 positive and 600 negative traces with lengths from 4 to 10.
  • 3) Case Study:: The mined DTA has 5 states and 3 clocks that represent queued-job scheduler states and monitor task interarrival and execution times.Its guards enforce minimum interarrival times of 5 and 12 time units and execution limits of 2 and 5 time units; deadlines are not covered because the parameter settings prevent misses.
  • 3) Case Study:: Negative traces are structurally close to positive traces because they share event sequences and can differ by only a minimal temporal distance, producing a more complex synthesized DTA.Such closely separated traces occur rarely in the randomly sampled scalability tests.
  • 3) Case Study:: The approach is evaluated against existing SMT-based DTA synthesis on randomly generated benchmarks and a scheduling case study.The broader evaluation includes target DTAs with one, two, and three clocks and alphabet sizes of two, three, and four.
  • 3) Case Study:: The paper reports that simplifying examples with sEL and tAPTA reduces the complexity of the SMT formulas used for DTA synthesis.The approach is evaluated on uniformly sampled traces from target DTAs and simulated scheduling-system outputs.

APPENDIX A PROOFS OF AUXILIARY RESULTS

The appendix proves auxiliary properties underlying the timed-language construction and tAPTA simplification, including preservation of acceptance behavior and conflict freedom under merging.

  • APPENDIX A PROOFS OF AUXILIARY RESULTS: The proof extends a partial run over one timed word to a corresponding run over another by matching clock valuations within the same integer-bounded regions.An induction establishes that each clock valuation is either equal or lies between the same consecutive integers, allowing the transition guard to remain enabled.
  • APPENDIX A PROOFS OF AUXILIARY RESULTS: If the constructed run reaches an accepting state, the corresponding timed word is accepted by the timed automaton, completing the acceptance-direction argument.The proof identifies the final state as accepting and associates the second timed word with the constructed run.
  • APPENDIX A PROOFS OF AUXILIARY RESULTS: A single-clock construction separates selected timed-word positions and uses integer-bounded guards to show that equivalent symbolic timing preserves the relevant timed-language relation.The constructed automaton accepts one word and therefore accepts the related word whose selected timing lies in the same integer point or interval.
  • APPENDIX A PROOFS OF AUXILIARY RESULTS: The extended-merging proof shows that merging states with positive and negative descendants introduces no conflict, because any merged branch can be mapped back to a compatible pre-merge path.States without both positive and negative descendants are also safe to merge directly.
  • APPENDIX A PROOFS OF AUXILIARY RESULTS: The pre-merge and post-merge language relationships ensure that positive and negative descendant languages remain separated after merging.The contradiction argument rules out an intersection between the relevant accepting and rejecting languages.
Loading 2609.16866v1…