Repairing Timed Automata Clock Guards through Abstraction and Testing

Angelo Gargantini; \'Etienne Andr\'e; Marco Radavelli; Paolo Arcaini

arxiv: 1907.02133 · v1 · pith:Z47MANSTnew · submitted 2019-06-27 · 💻 cs.LO

Repairing Timed Automata Clock Guards through Abstraction and Testing

\'Etienne Andr\'e , Paolo Arcaini , Angelo Gargantini , Marco Radavelli This is my paper

Pith reviewed 2026-05-25 14:25 UTC · model grok-4.3

classification 💻 cs.LO

keywords timed automataparametric timed automataclock guardsmodel repairtest generationoracleparameter synthesisabstraction

0 comments

The pith

A method abstracts a faulty timed automaton into a parametric one to repair incorrect clock guards using tests and oracle feedback.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Users may specify timed automata with correct structure but incorrect clock constraints on transitions. The approach abstracts the initial automaton into a parametric timed automaton representing possible corrections. Timed traces are generated from this parametric model and checked for acceptance by an oracle. Constraints on the parameters are then synthesized based on the oracle results, allowing the creation of a repaired timed automaton. This process enables partial repair of the user's design when only guards are wrong.

Core claim

The search space for the correct timed automaton is represented by a parametric timed automaton obtained by abstracting the initial faulty one. Test data consisting of timed traces are generated from the parametric model, their acceptance is assessed with the oracle, and constraints on the parameters are synthesized to instantiate the repaired timed automaton.

What carries the argument

The parametric timed automaton (PTA) abstraction of the initial timed automaton, which encodes possible correct clock guard values as parameters, combined with test generation and parameter synthesis from oracle-validated traces.

If this is right

A repaired timed automaton can be instantiated from the synthesized parameter constraints.
The method succeeds in partially repairing the initial design as shown in experiments.
Only guard transitions need to be corrected while preserving the automaton structure.
The process involves abstraction to a parametric model, test generation, oracle assessment, and constraint synthesis.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The technique could be applied to other specification languages where uncertainties are in timing parameters.
Iterative application might allow refining repairs with additional oracle queries.
Combining with different test generation strategies could increase the likelihood of finding consistent repairs.

Load-bearing premise

The structure of the timed automaton is correct, and only the clock guard values on transitions are wrong.

What would settle it

An experiment where the oracle rejects traces in a way that yields no consistent parameter constraints, even though the automaton structure matches the intended system.

read the original abstract

Timed automata (TAs) are a widely used formalism to specify systems having temporal requirements. However, exactly specifying the system may be difficult, as the user may not know the exact clock constraints triggering state transitions. In this work, we assume the user already specified a TA, and (s)he wants to validate it against an oracle that can be queried for acceptance. Under the assumption that the user only wrote wrong guard transitions (i.e., the structure of the TA is correct), the search space for the correct TA can be represented by a Parametric Timed Automaton (PTA), i.e., a TA in which some constants are parametrized. The paper presents a process that i) abstracts the initial (faulty) TA tainit in a PTA pta; ii) generates some test data (i.e., timed traces) from pta; iii) assesses the correct evaluation of the traces with the oracle; iv) uses the IMITATOR tool for synthesizing some constraints phi on the parameters of pta; v) instantiate from phi a TA tarep as final repaired model. Experiments show that the approach is successfully able to partially repair the initial design of the user.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The repair method can fix guard constants in timed automata when the structure is already correct but cannot handle structural errors, and the experiments do not verify the assumption boundary.

read the letter

The key point is that the repair only works if the timed automaton structure is already correct. The method replaces guard constants with parameters to create a PTA while keeping locations and transitions fixed. It then generates traces from this PTA, queries an oracle to see which traces are accepted, and feeds the results to IMITATOR to synthesize constraints on the parameters. From those constraints it instantiates a repaired TA. If the user got the transitions or locations wrong, no choice of parameter values can produce the right model because that model is outside the search space defined by the PTA. What the paper does well is to make this assumption explicit and to build a complete loop around existing components. The abstraction to PTA, the trace generation, the oracle checks, and the use of IMITATOR for synthesis form a coherent process. The experiments, as described, show that partial repairs are possible when the assumption holds. This is a practical contribution for the guard-repair subproblem rather than a claim to fix arbitrary TA errors. The soft spots are in the experimental validation and the scope. The abstract reports success in partial repair but gives no numbers or details on the benchmarks, such as how many cases were tested or whether the oracles differed only in guards. The stress-test note is accurate here: without cases that violate the structure assumption, the results do not demonstrate robustness when that assumption fails. There is also the issue that one author is a primary developer of IMITATOR, which introduces potential circularity in how the tool's performance is evaluated, though this is not uncommon in tool papers. This paper is for people working on verification and repair of real-time systems, particularly those already using parametric timed automata or IMITATOR. A reader interested in model-based testing or automated repair of timing constraints would find the workflow relevant. It is not aimed at readers looking for general TA repair without assumptions. I recommend sending it for peer review. The core idea is sound within its limits, the method is described clearly, and the stated assumption prevents overclaiming. Referees can ask for more boundary experiments and clarification on the evaluation setup, but the work is solid enough to deserve that step rather than a desk reject.

Referee Report

2 major / 2 minor

Summary. The paper proposes a repair method for timed automata (TAs) whose clock guards are incorrect while the underlying structure (locations and transitions) is assumed correct. The initial TA is abstracted to a parametric timed automaton (PTA) by replacing guard constants with parameters; test traces are generated from the PTA, classified by an oracle, and IMITATOR is used to synthesize parameter constraints consistent with the oracle answers; a concrete repaired TA is then instantiated from the constraints. Experiments are reported to show that the method can partially repair the user's initial design.

Significance. If the central assumption holds and the synthesis loop is shown to be sound, the work provides a practical bridge between parameter synthesis tools and oracle-guided repair for timed systems, potentially useful in domains where an executable oracle exists but exact constants are hard to specify. The explicit statement of the structural-correctness assumption is a strength, as is the use of an existing tool (IMITATOR) rather than a new synthesis engine.

major comments (2)

[Experiments] The central claim (successful partial repair) rests on the assumption that faults are confined to guard constants. The experiments section must demonstrate that every benchmark oracle differs from the initial TA solely in guard values; otherwise the reported successes do not address the case in which the assumption is violated and the target lies outside the PTA search space.
[Method overview / Parameter synthesis step] The repair loop is described as generating traces from the PTA, querying the oracle, and synthesizing constraints with IMITATOR. No soundness argument is supplied showing that any TA consistent with the oracle answers on the generated traces is indeed a repair of the original specification (as opposed to an arbitrary PTA that happens to agree on those traces).

minor comments (2)

[Abstract and Experiments] The abstract states that the approach 'partially repair[s]' the design; the experiments section should quantify what 'partial' means (e.g., fraction of guards corrected, remaining distance to oracle).
[Introduction / Method] Notation for the initial TA (tainit), repaired TA (tarep) and synthesized constraint (phi) is introduced without a dedicated preliminaries section; a short table or diagram relating these symbols to the PTA would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments and address each major point below. We will revise the manuscript to strengthen the presentation of the experimental validation and to include an explicit discussion of the method's guarantees.

read point-by-point responses

Referee: [Experiments] The central claim (successful partial repair) rests on the assumption that faults are confined to guard constants. The experiments section must demonstrate that every benchmark oracle differs from the initial TA solely in guard values; otherwise the reported successes do not address the case in which the assumption is violated and the target lies outside the PTA search space.

Authors: We agree that explicit confirmation is required. All benchmarks were constructed so that the oracles differ from the initial TA only in the numerical values of the clock guards while preserving locations, transitions, and clock usage. In the revised version we will add a dedicated paragraph (and an accompanying table) in the Experiments section that states this property for each benchmark and briefly describes how the oracles were obtained. revision: yes
Referee: [Method overview / Parameter synthesis step] The repair loop is described as generating traces from the PTA, querying the oracle, and synthesizing constraints with IMITATOR. No soundness argument is supplied showing that any TA consistent with the oracle answers on the generated traces is indeed a repair of the original specification (as opposed to an arbitrary PTA that happens to agree on those traces).

Authors: The current manuscript does not contain a formal soundness argument. The approach is intended as a practical, oracle-guided procedure that returns a TA inside the user-provided structural envelope that is consistent with the observed traces. In the revision we will insert a short subsection after the description of the synthesis step that states the precise conditions (structural correctness plus sufficient trace coverage) under which the output can be regarded as a partial repair, and we will clarify that full equivalence to an unknown oracle cannot be guaranteed from finite traces alone. revision: yes

Circularity Check

0 steps flagged

No significant circularity; method is a procedural pipeline using external synthesis

full rationale

The described process constructs a PTA by parametrizing constants in the given TA (explicitly under the stated assumption that topology is correct), generates traces from that PTA, queries an external oracle, invokes the independent IMITATOR tool to synthesize parameter constraints, and instantiates a repaired TA from the resulting phi. None of these steps reduces by construction to its inputs (no self-definitional equations, no fitted parameter renamed as prediction, no load-bearing self-citation chain for the core claim). The experimental claim of partial repair is presented as an empirical outcome rather than a tautology. The assumption is stated openly in the abstract; its scope is a correctness issue, not a circularity issue. No uniqueness theorems, ansatzes, or renamings are invoked in the provided derivation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the domain assumption that only guards are faulty and on the availability of an oracle; no free parameters or invented entities are introduced beyond the standard PTA construction.

axioms (1)

domain assumption The structure of the TA is correct; only guard constants are wrong.
Explicitly stated in the abstract as the operating assumption that reduces the search space to a PTA.

pith-pipeline@v0.9.0 · 5749 in / 1214 out tokens · 28870 ms · 2026-05-25T14:25:46.237354+00:00 · methodology

Repairing Timed Automata Clock Guards through Abstraction and Testing

Core claim

What carries the argument

If this is right

Where Pith is reading between the lines

Load-bearing premise

What would settle it

discussion (0)