Abstract
Analysis algorithms for quantitative automata are complex and hard to validate. Existing approaches — benchmarks, mutation testing, uniform random generation — each fail to expose subtle implementation bugs. We present a framework that repeatedly 1) generates random quantitative automata that are non-degenerate by construction, 2) tests each against a target property, and 3) shrinks any violation to a local minimum, yielding a small, actionable counterexample. We implement the framework for parametric timed automata (PTA) and apply it to Imitator, a mature model checker for PTA, uncovering 5 previously unknown bugs, one of which was exposed by a counterexample with just 2 locations and 1 transition.
1 Introduction↩︎
Quantitative automata (timed, parametric, weighted, probabilistic) underpin a wide range of formal verification tools. Their analysis algorithms are complex and subject to continuous optimisation: as tools mature and acquire new features, subtle bugs can accumulate in corner cases that standard benchmark suites never exercise. Small, actionable counterexamples are crucial for debugging such bugs, but manually crafting them is difficult when the nature of the fault is unknown.
We propose a semantics-respecting random generation framework that avoids degenerate models—unsatisfiable guards, unreachable locations—by construction, paired with a shrinking procedure that iteratively removes structure while verifying the target property is preserved, yielding a small, human-readable witness. While we instantiate the framework for parametric timed automata (PTAs) [1], the design is not specific to them.
We demonstrate that the framework we propose produces them automatically: applying it to Imitator [2], a mature model checker for PTAs, it uncovered 5 previously unknown bugs. One counterexample consists of just two locations and one transition, yet it exposes a fault in the unavoidability synthesis algorithm that had gone undetected until now.
Existing approaches fall short in different ways. Benchmark suites [3] of curated models rarely stress edge cases. Mutation testing requires a collection of good seeds, but any bias in those seeds risks missing entire classes of faults; and when the nature of the bugs is unknown, there is no principled basis for selecting them. Uniform random generation avoids this bias but produces mostly degenerate models with unsatisfiable constraints or unreachable locations that no algorithm can meaningfully distinguish.
1.0.1 Related work↩︎
Property-based testing [4] introduced the generate-and-shrink paradigm for automated counterexample finding. Random generation to stress-test analysis tools is well-established: compiler testing [5] and SMT solver fuzzing [6] demonstrate that random inputs reliably surface subtle implementation faults. Random NFA generation [7] has been used to benchmark algorithm performance rather than find bugs: performance evaluation tolerates degenerate inputs and has no need for small witnesses, goals orthogonal to ours. Most closely related is the work of Manini et al. [8], who generate random timed automata and derive a problem-specific oracle automatically; however, constructing such an oracle requires non-trivial problem-specific theory, limiting applicability to problems where one is available, and they perform no counterexample minimisation. We sidestep the oracle problem entirely via differential testing [9], comparing two algorithm variants on the same input, and reduce any witness to a minimal non-witness example through property-preserving shrinking.
1.0.2 Contributions↩︎
A semantics-respecting random PTA generator that produces non-degenerate models by construction
A shrinker that reduces witnesses to a local minimum while preserving the target property, yielding small actionable counterexamples
An implementation as a meta-tool within Imitator
An empirical evaluation uncovering 5 previously unknown bugs in a mature tool
2 Background↩︎
2.1 Parametric Timed Automata↩︎
A Parametric Timed Automaton (PTA) is a structure based on timed automata (TA). Like classical automata, it has locations connected by discrete transitions. It also has clocks. Locations are associated a condition on clock valuations (invariant) that must be satisfied while staying in the location. An action in a timed automaton is either to take a discrete transition or to let some time pass. Discrete transitions have a guard that must be satisfied in order to take the transition, and a set of clocks to reset. In a parametric setting, these conditions use linear terms over clocks and parameters. Parameters are unspecified but constant during a run.
Throughout this paper, we let \(X\) denote a set of real-valued clocks and \(P\) a set of rational parameters.
Definition 1 (parametric guards). A linear term* over \(P\) has the form \(k\) or \(kp\) or a sum thereof, where \(k \in \mathbb{Q}\) and \(p \in P\). The set of parametric guards \(\mathcal{G}(X,P)\) is defined by the grammar: \[\phi\; := \; \top \; | \; \phi\land \phi\; | \; x \bowtie\tau \; | \; \tau ' \bowtie\tau\] where \(x\inX\), \({\bowtie} \in \mathtt{Cmp}:= \{ <, \leq, =, \geq, > \}\), and \(\tau , \tau '\) are linear terms over \(P\).*
In this paper, parametric guards are treated as syntactic objects. Their semantics will be defined in terms of the set of valuations that satisfy them (6).
Definition 2 (atomic sub-expressions). Let \(\phi \in \mathcal{G}(X,P)\) be a parametric guard. The multiset of atomic sub-expressions* of \(\phi\), denoted \(\mathtt{subexpr}(\phi)\), is the multiset of sub-expressions of \(\phi\) that are of the form \(x \bowtie\tau\) or \(\tau ' \bowtie\tau\).*
Example 1. Consider the parametric guard \(\phi = (x \leq p + 5) \land (y > 2p) \land (x \leq p + 5)\). The multiset of atomic sub-expressions of \(\phi\) is: \[\mathtt{subexpr}(\phi) = \{ x \leq p + 5, x \leq p + 5, y > 2p \}.\]
Definition 3 (Parametric Timed Automaton). A Parametric Timed Automaton* is a tuple of the form \(\mathcal{A}= (L, X, P, T, \ell_0, \mathit{Inv})\) such that*
\(L\), \(X\), \(P\) are disjoint sets of locations, clocks, parameters.
\(T\subseteq L\times \mathcal{G}(X,P) \times 2^{X} \times L\) is the set of transitions* of the form \((\ell,g,Y,\ell')\) where: \(\ell\), \(\ell'\) are source and target locations, \(g\) is the parametric guard, \(Y\) the set of clocks to reset. We write \(\ell\xrightarrow{g,Y} \ell'\) to denote a transition and \(\ell\to \ell'\) when the guard and resets are unimportant.*
\(\ell_0\) is the initial location.
\(\mathit{Inv}\; : \; L\to \mathcal{G}(X,P)\) associates an invariant with each location.
Definition 4 (valuations). A clock valuation* is a function \(v _X\in \mathbb{R}_{\geq 0}^{X}\) assigning a non-negative real value to each clock in \(X\). A parameter valuation \(v _P\in \mathbb{Q}_{\geq 0}^{P}\) assigns a non-negative rational value to each parameter in \(P\).*
A valuation* is a pair \(v = (v _X,v _P)\). The set of all valuations of a PTA with clocks \(X\) and parameters \(P\) is denoted \(V= \mathbb{R}_{\geq 0}^{X} \times \mathbb{Q}_{\geq 0}^{P}\). Since \(X\) and \(P\) are disjoint, we write \(v(y)\) for \(v_{X}(y)\) if \(y \in X\) and \(v_{P}(y)\) if \(y \in P\).*
Definition 5 (clock update). For \(Y \subseteq X\) and \(v \in V\), write \(v [Y \mapsto 0]\) for the valuation that maps each \(x \in Y\) to \(0\) and each \(x \notin Y\) to \(v (x)\). For \(Z \subseteq V\), write \(Z[Y \mapsto 0]^{-1} := \{v \mid v [Y \mapsto 0] \in Z\}\), i.e., the set of valuations that land in \(Z\) after resetting the clocks in \(Y\).
Definition 6 (satisfaction of guards). Let \(g\in \mathcal{G}(X,P)\) be a parametric guard, and \(v = (v _X,v _P)\) a valuation. We say that \(v\) satisfies* \(g\), denoted \(v \models g\), if \(g\) evaluates to true when each clock \(x \in X\) is replaced by \(v _X(x)\) and each parameter \(p \in P\) is replaced by \(v _P(p)\). Let \(\llbracket g \rrbracket\) denote the set of valuations satisfying \(g\): \[\llbracket g \rrbracket = \{v \in V\mid v \models g\}.\]*
2.2 Multigraphs↩︎
We recall the standard notion of directed multigraphs, which we use to describe the graph structure of generated automata.
Definition 7 (multigraph). A directed multigraph is a pair \(G = (L, M)\), where \(L\) is a finite set of locations and \(M : L\times L\to \mathbb{N}\) is an edge multiplicity function. For \(\ell,\ell' \in L\), let the value \(M(\ell,\ell')\) be the number of directed edges from \(\ell\) to \(\ell'\).
The outgoing degree of a location \(\ell\in L\) (counting multiplicities) is defined as \[\deg^+_M(\ell) \;\triangleq\; \sum_{\ell' \in L} M(\ell,\ell').\]
2.3 Probability Distributions↩︎
We use probability distributions to describe and parameterize the random generation of automata.
Definition 8 (Distribution). For a countable set \(A\), let \(\mathcal{D}(A)\) denote the set of probability distributions over \(A\), i.e.functions \(\mu: A \to [0,1]\) such that \(\sum_{a \in A} \mu(a) = 1\). We write \(X \sim \mu\) to denote that \(X\) is sampled according to \(\mu\).
We now introduce several standard constructions on distributions that we use to describe our generation algorithms.
Definition 9 (Standard distributions). We use the following standard distributions on countable sets.
\(\text{Uniform}(A)\): uniform over a non-empty finite set \(A\), assigning probability \(1/|A|\) to each element.
\(\text{Bern}(p)\): Bernoulli, \(p \in [0,1]\): taking \(1\) with probability \(p\) and \(0\) with \(1-p\).
\(\text{Choose}_k(A)\): uniform over \(k\)-element subsets of finite set \(A\), for \(0 \leq k \leq |A|\).
\(\delta_a\) is the Dirac distribution: a point mass at \(a\), with \(\delta_a(a) = 1\).
\(\text{Geom}_{\le m}(q)\): Capped Geometric, for \(q \in (0,1)\) and \(m \in \mathbb{N}_{\ge 1}\), the distribution on \(\{1,\dots,m\}\) with \(P(K{=}k) = (1-q)q^{k-1}\) for \(k < m\) and \(P(K{=}m) = q^{m-1}\).
Definition 10 (Pushforward). Let \(f : A \to B\) and \(\mu\in \mathcal{D}(A)\). The pushforward distribution \(f_{\ast}(\mu) \in \mathcal{D}(B)\) is defined by \[f_{\ast}(\mu)(b) = \sum_{a \in A \,:\, f(a)=b} \mu(a).\] Equivalently, if \(X \sim \mu\) then \(f(X) \sim f_{\ast}(\mu)\).
Definition 11 (Dependent sampling). Let \(\mu\in \mathcal{D}(A)\) and \(f : A \to \mathcal{D}(B)\). The distribution \(\mu\mathbin{\circledast}f \in \mathcal{D}(B)\) is defined by \[(\mu\mathbin{\circledast}f)(b) = \sum_{a \in A} \mu(a)\, f(a)(b).\] Equivalently, sample \(a \sim \mu\) and then sample \(b\) from \(f(a)\).
Definition 12 (Product distribution). Let \(\mu\in \mathcal{D}(A)\) and \(\nu \in \mathcal{D}(B)\). Their product \(\mu\otimes \nu \in \mathcal{D}(A \times B)\) is defined by \[(\mu\otimes \nu)(a,b) = \mu(a)\nu(b).\] Equivalently, sample independently from \(\mu\) and \(\nu\).
Definition 13 (\(n\)-fold product). Let \(\mu\in \mathcal{D}(A)\), \(n \in \mathbb{N}\), and write \(\text{Fin}(n) := \{0,\dots,n-1\}\). The \(n\)-fold product \(\mu^{\otimes n} \in \mathcal{D}(A^{\text{Fin}(n)})\) is defined by \[\mu^{\otimes n}\bigl((a_i)_{i \in \text{Fin}(n)}\bigr) := \prod_{i \in \text{Fin}(n)} \mu(a_i).\] Equivalently, \(\mu^{\otimes n}\) samples \(n\) independent values from \(\mu\).
Definition 14 (Geometric subset choice). For \(q \in (0,1)\) and a finite set \(S\), define \[\text{ChooseGeom}(q,S) \;\triangleq\; \text{Geom}_{\le |S|}(q) \;\mathbin{\circledast}\; (\lambda k.\; \text{Choose}_k(S)).\] Equivalently, draw a random size \(k\) from \(\text{Geom}_{\le |S|}(q)\) and return a uniformly random \(k\)-element subset of \(S\).
3 Framework↩︎
The framework consists of two components: a semantics-respecting random generator (4) and a property-preserving shrinker (5). Together they form the Validator (1), searching for a small counterexample to a property \(\varphi\).
A model specification \(\mathcal{M}\) is a user-supplied configuration controlling the intended size and structure of generated PTAs, and a generator schema \(\Sigma\) is a structured collection of probability distributions over PTA components; both are defined formally in 4. The generator comprises two high-level procedures: ConstructSchema (5), which translates \(\mathcal{M}\) into \(\Sigma\), and AutomatonGen (2), which draws a PTA from \(\Sigma\). The shrinker is Shrink (5), which iteratively removes structure from a violating PTA while preserving the violation. 4 establishes formal requirements for the generator and describes the algorithms that satisfy them by construction; 5 presents the staged shrinking pipeline and its design principles.
4 Semantics-Respecting Generator↩︎
This section develops the semantics-respecting PTA generator in three steps: we first state formal requirements that any meaningful generator must satisfy (4.1), then introduce the generation scheme and AutomatonGen, which samples a PTA from a given schema (4.2), and finally show how ConstructSchema builds a schema from a model specification so that all requirements are met by construction (4.3).
4.1 Generator Requirements↩︎
We adopt a principle of meaningfulness: all components of the generated PTA should be meaningful. This means that we want to avoid generating components that are trivial, unreachable, unsatisfiable, or redundant. We now outline the specific design goals we have for the generator.
4.1.0.1 Graph Structure
The shape of the underlying graph of the generated PTA is an important aspect of generation. A completely random graph structure has a high likelihood of being disconnected or having locations that are unreachable from the initial location. Following the principle of meaningfulness, this is unacceptable as it leads to meaningless locations.
We therefore require all locations to be reachable from the initial location via discrete transitions.
Requirement 1 (Graph Reachability). The underlying directed graph of the generated PTA is such that all locations are reachable from the initial location via discrete transitions, ignoring guards, invariants and time elapsing: \[\psi_{Graph}(\mathcal{A}= (L, X, P, T, \ell_0, \mathit{Inv})) \triangleq \forall \ell\in L, \ell_0 \to^* \ell\] where \(\to^*\) is the transitive closure of \(\to\).
4.1.0.2 Invariants
Invariants are important components of timed automata as they restrict the time that can be spent in a location. However, if an invariant is unsatisfiable, then the location becomes meaningless as no time can be spent there. Following the principle of meaningfulness, we want to avoid generating locations with unsatisfiable invariants.
Requirement 2 (Invariant Satisfiability). All invariants in the generated PTA are satisfiable: \[\psi_{InvSat}(\mathcal{A}= (L, X, P, T, \ell_0, \mathit{Inv})) \triangleq \forall \ell\in L, \llbracket \mathit{Inv}(\ell) \rrbracket \neq \emptyset\]
Furthermore, we want to ensure that the initial location invariant is satisfiable for the initial clock valuation where all clocks are set to 0. This ensures that the system can start executing from the initial location. In a sense, this is the most important requirement for invariants, as if this is not satisfied, the generated PTA is completely meaningless from the start.
Requirement 3 (Initial Invariant Satisfiability). The initial location invariant is satisfiable for the initial clock valuation where all clocks are set to 0:
\[\psi_{InvInit}(\mathcal{A}= (L, X, P, T, \ell_0, \mathit{Inv})) \triangleq \Bigl\llbracket \bigwedge\limits_{x\in X} x = 0 \Bigr\rrbracket \subseteq \llbracket \mathit{Inv}(\ell_0) \rrbracket\]
4.1.0.3 Guards
Similar to invariants, a guard is only meaningful if it is satisfiable, so this is a nice starting point. We can strengthen this even more: even if a guard is satisfiable for some valuations, it might not be satisfiable in any context where the guard is used i.e. on a transition between two locations with certain invariants. There are three components to consider here: the source location invariant, the guard itself, and the target location invariant (after resetting the appropriate clocks). Thus, a first attempt at a meaningfulness requirement for guards is that each guard should be satisfiable within the context of the source location invariant and the target location invariant (after resetting the appropriate clocks):
\[\begin{align} \psi_{GuardSatAttempt}(\mathcal{A}= (L, X, P, T, \ell_0, \mathit{Inv})) \triangleq \forall (\ell_1, g, Y, \ell_2) \in T,\; \\ \llbracket g \rrbracket \cap \llbracket \mathit{Inv}(\ell_1) \rrbracket \cap \llbracket \mathit{Inv}(\ell_2) \rrbracket[Y \mapsto 0]^{-1} \neq \emptyset \end{align}\]
However, this requirement on guards imposes a significant restriction on invariants. Invariant generation is no longer a local problem, since now all pairs of invariants connected by a transition must have a non-empty intersection (taking into account resets). This makes invariant generation significantly more complex, as we can no longer generate invariants independently for each location. Instead, we must consider the entire graph structure and the transitions between locations when generating invariants, introducing a graph exploration aspect to invariant generation. A good middleground between meaningfulness and feasibility is to only consider the source location invariant when checking guard satisfiability. This way, we ensure that the guard is meaningful in the context of where it is used, without overly complicating invariant generation. Thus, we require the following:
Requirement 4 (Guard Satisfiability). All guards in the generated PTA are satisfiable within the context of the source location invariant: \[\begin{align} \psi_{GuardSat}(\mathcal{A}= (L, X, P, T, \ell_0, \mathit{Inv})) \triangleq \forall (\ell_1, g, Y, \ell_2) \in T,\; \\ \llbracket g \rrbracket \cap \llbracket \mathit{Inv}(\ell_1) \rrbracket \neq \emptyset \end{align}\]
4.1.0.4 Redundant sub-expressions
A guard or invariant may contain redundant sub-expressions that do not contribute to the overall meaning of the constraint. For example, the guard \(x \leq 5 \land x \leq 10\) contains the redundant sub-expression \(x \leq 10\) since it is implied by \(x \leq 5\). Following the principle of meaningfulness, we want to avoid generating guards and invariants with redundant sub-expressions. We define a helper predicate over \(\mathcal{G}(X, P)\) to capture the absence of redundant sub-expressions:
\[\psi_{NoRed}(\phi) \triangleq \forall \phi_1, \phi_2 \in \mathtt{subexpr}(\phi), \llbracket \phi_1 \rrbracket \not\subseteq \llbracket \phi_2 \rrbracket\]
and then require that all guards and invariants in the generated PTA satisfy this property:
Requirement 5 (No Redundant Sub-expressions). No guards or invariants in the generated PTA contain redundant sub-expressions: \[\begin{align} \psi_{Redundant}(\mathcal{A}= (L, X, P, T, \ell_0, \mathit{Inv})) \triangleq \; &\forall \ell\in L, \psi_{NoRed}(\mathit{Inv}(\ell)) \; \land \; \\ &\forall (\ell_1, g, Y, \ell_2) \in T, \psi_{NoRed}(g) \end{align}\]
4.2 Generation Scheme↩︎
To describe the generator, we first introduce the notion of a generation schema, which is a collection of probability distributions over the components of a PTA. A generation schema defines how to sample each simple component of a PTA, such as the set of locations, clocks, parameters, the graph structure, invariants, guards, and resets.
Definition 15 (generation schema). A generation schema* is a tuple \(\Sigma= (\mathfrak{L},\mathfrak{X}, \mathfrak{P}, \mathfrak{G}, \mathfrak{I}, \mathfrak{Z}, \mathfrak{Y})\) where:*
\(\mathfrak{L}\) is a probability distribution over finite sets of locations \(L\),
\(\mathfrak{X}\) is a probability distribution over finite sets of clocks \(X\),
\(\mathfrak{P}\) is a probability distribution over finite sets of parameters \(P\),
\(\mathfrak{I}(L, X,P)\) is a probability distribution over invariant functions \(\mathit{Inv}: L\to \mathcal{G}(X,P)\),
\(\mathfrak{G}(L)\) is a probability distribution over multigraphs over \(L\),
\(\mathfrak{Z}(X,P)\) is a probability distribution over \(\mathcal{G}(X,P)\),
\(\mathfrak{Y}(X)\) is a probability distribution over \(2^{X}\).
Since the types of locations, clocks, and parameters are not fixed, we use canonical tagged carriers whose sizes are supplied dynamically.
Definition 16 (Tagged canonical carriers for generation). Let \(Tag\mathrel{\vcenter{:}}= \{\texttt{Loc},\texttt{Clock},\texttt{Param}\}\) be a set of tags. For each \(\alpha\inTag\) and \(n \in \mathbb{N}\), define the tagged carrier \(\text{Fin}^{\texttt{Loc}}(\alpha) := \text{Fin}(n)\times \{\alpha\}\). Distinct tags ensure pairwise disjointness, allowing unambiguous distinction of locations, clocks, and parameters in guards. We write \(\ell_n\), \(x_n\), \(p_n\) as shorthands for \((n,\texttt{Loc})\), \((n,\texttt{Clock})\), \((n,\texttt{Param})\); the initial location is fixed as \(\ell_0 = (0,\texttt{Loc})\).
AutomatonGen (2) samples PTA components in dependency order. The sets \(L\), \(X\), \(P\) are drawn first, since all remaining distributions are parameterized by them. Invariants are sampled before the transition structure, so that the already-sampled source invariant \(\mathit{Inv}(\ell)\) can be passed to \(\mathfrak{Z}\) as context — a dependency that an appropriately instantiated \(\mathfrak{Z}\) can exploit to satisfy 4.
The distributions in \(\Sigma\) are left abstract. The next subsection defines a model specification and the ConstructSchema procedure that instantiates them to satisfy the design goals by construction.
4.3 Instantiation of Generation Schema↩︎
We now instantiate the abstract generation schema: we define two sub-procedures, GraphGen and GuardGen, that enforce the structural requirements, and show how ConstructSchema uses them to assemble a complete, requirements-satisfying schema from a model specification.
4.3.0.1 Graph structure.
To satisfy 1, \(\mathfrak{G}\) must only produce graphs where all locations are reachable from \(\ell_0\). GraphGen (3) achieves this by first building a spanning tree rooted at \(\ell_0\) (guaranteeing reachability), then adding random edges until the desired per-location outdegree is met.
4.3.0.2 Guard generation.
Guards must intersect the invariant of their source location (4), but a uniformly random guard is almost certainly disjoint from any fixed invariant. We therefore restrict generation to Coupled Interval Guards (CIGs), a class of guards structured as interval-and-coupling triples that admit efficient witness-based sampling guaranteeing intersection by construction.
Throughout this section, an interval denotes a closed, open, or half-open interval with non-negative integer endpoints: \([l,u]\), \((l,u]\), \([l,u)\), or \((l,u)\) with \(l,u\in\mathbb{Z}_{\geq 0}\cup\{+\infty\}\). Write \(\mathbb{Z}(I)\) for the set of non-negative integers in \(I\); for example, \(\mathbb{Z}([2,5)) = \{2,3,4\}\) and \(\mathbb{Z}((3,4)) = \emptyset\).
Definition 17 (Coupled Interval Guard (CIG)). Let \(X\) be a finite set of clocks and \(P\) a finite set of parameters. A Coupled Interval Guard* (CIG) over \((X,P)\) is a triple \[C = (B_X, B_P, \kappa)\] where:*
\(B_X : X\to \mathbb{I}_{\geq 0}\) assigns to each clock \(x \in X\) an interval \(B_X(x)\) (closed, open, or half-open) with \(l_x,u_x \in \mathbb{Z}_{\geq 0} \cup \{+\infty\}\),
\(B_P : P\to \mathbb{I}_{\geq 0}\) assigns to each parameter \(p \in P\) an interval \(B_P(p)\) (closed, open, or half-open) with \(l_p,u_p \in \mathbb{Z}_{\geq 0} \cup \{+\infty\}\),
\(\kappa : X\rightharpoonup (P\times \mathtt{Cmp})\) is a partial function (the coupling map), where \(\mathtt{Cmp}= \{<,\le,>,\ge\}\).
4.3.0.3 Interpretation.
Every CIG \(C = (B_X,B_P,\kappa)\) induces a parametric guard \(\phi_C \in \mathcal{G}(X,P)\) by interpreting its components as conjunctions of atomic constraints. Hence CIGs form a syntactic subclass of parametric guards.
In particular, CIGs restrict the guard language to: (i) interval bounds over individual clocks and parameters (closed endpoints give \(\le\)/\(\ge\) constraints; open endpoints give \(<\)/\(>\) constraints), and (ii) at most one clock-parameter comparison per clock. No clock-clock comparisons and no comparisons between linear parameter terms are permitted. From now on, we freely identify a CIG with its induced parametric guard.
Example 2. Let \(X= \{x\}\), \(P= \{p\}\), and let \(C = (B_X, B_P, \kappa)\) with \(B_X(x) = [0,5)\), \(B_P(p) = [0,3]\), and \(\kappa(x) = (p,<)\). The induced guard is \(x \ge 0 \land x < 5 \land p \ge 0 \land p \le 3 \land x < p\). We use this CIG as a running example below.
A CIG \(C\) is integer-satisfiable if \(\llbracket C \rrbracket\) contains a witness whose clock and parameter values are all non-negative integers. Note that for open intervals with integer endpoints, integer-satisfiability is strictly stronger than real-satisfiability: \((3 < x < 4)\) is satisfiable over \(\mathbb{R}\) but not integer-satisfiable. Throughout, we require all CIGs arising in the generation pipeline to be integer-satisfiable.
Definition 18 (tight CIG). A CIG \(C = (B_X,B_P,\kappa)\) is tight if
for every clock \(x \in X\) : \(\mathbb{Z}(B_X(x)) = \{\, v(x) \mid v \text{ is an integer witness of } C \,\},\)
for every parameter \(p \in P\) : \(\mathbb{Z}(B_P(p)) = \{\, v(p) \mid v \text{ is an integer witness of } C \,\}.\)
Intuitively, the integer points of each box exactly span the values the variable takes across all integer witnesses of \(C\).
Example 3. The CIG \(C\) from the previous example is not tight. The strict coupling \(x < p\) and the bound \(p \le 3\) force \(v(x) \le 2\) for every integer witness (since \(v(x) < v(p) \le 3\) and \(v(x) \in \mathbb{Z}_{\geq 0}\)), so \(\{v(x) \mid v \text{ is an integer witness of } C\} = \{0,1,2\} \ne \{0,1,2,3,4\} = \mathbb{Z}(B_X(x))\).
4.3.0.4 Tightening.
Given a CIG \(C=(B_X,B_P,\kappa)\), we write \(\mathrm{tighten}(C)\) for a bound-tightened form of \(C\) whose integer witnesses are exactly those of \(C\). It is defined whenever \(C\) is integer-satisfiable, and the result is itself integer-satisfiable: any integer witness of \(C\) satisfies the coupling constraints and therefore also satisfies the tightened bounds. In our restricted setting, tightening is local and bidirectional: for each coupled clock with \(\kappa(x)=(p,\bowtie)\), the bound of \(B_X(x)\) in the direction of \(\bowtie\) is tightened to match the corresponding bound of \(B_P(p)\) (closed endpoint for \(\le\)/\(\ge\), open for \(<\)/\(>\)); symmetrically, the opposing bound of \(B_P(p)\) is tightened to exclude parameter values for which no compatible integer clock value exists.
Example 4. Tightening \(C\) yields \(\mathrm{tighten}(C) = (B'_X, B'_P, \kappa)\) with \(B'_X(x) = [0,3)\) and \(B'_P(p) = [1,3]\). In the forward direction, \(\kappa(x)=(p,{<})\) propagates \(p\)’s upper bound \(3\) as an open upper endpoint on \(x\). In the backward direction, \(p = 0\) is excluded from \(B'_P\) because no integer \(x \ge 0\) satisfies \(x < 0\); the smallest parameter value with a compatible integer clock is \(p = 1\) (witnessed by \(x = 0\)).
4.3.0.5 Witness generation.
Let \(C=(B_X,B_P,\kappa)\) be integer-satisfiable. \(\mathrm{\small WitnessGen}(C)\) denotes the distribution over integer witnesses \(v=(v_X,v_P)\in\llbracket C\rrbracket\) defined by first computing \(C'=\mathrm{tighten}(C)\), then drawing each \(v_P(p)\) uniformly from \(\mathbb{Z}(B'_P(p))\), and each \(v_X(x)\) uniformly from the integers in the (possibly coupling-restricted) interval \(B'_X(x)\). The joint tight condition on \(B'_P\) ensures that every sampled \(n_p \in \mathbb{Z}(B'_P(p))\) has at least one compatible integer \(n_x\) in the coupling-restricted interval, so the distribution is well-defined; \(v \in \llbracket C \rrbracket\) holds by construction, and every integer witness has positive probability.
GuardGen (4) generates guards satisfying 2 3 4 5 by construction. It samples a witness valuation \(v = (v_X,v_P) \in \llbracket C \rrbracket\) via \(\mathrm{\small WitnessGen}(C)\) (which tightens \(C\) internally). Using this witness, a maximal candidate \(C_{\max}\) is constructed: for each clock and parameter, an interval (with randomly chosen open or closed endpoints) is sampled around the corresponding witness value, and for each clock a clock-parameter comparison is chosen such that it is satisfied by \(v\). Since \(v\) is an integer witness, any combination of open or closed endpoints is valid: an open lower bound samples strictly below \(v\), and an open upper bound samples strictly above \(v\), so \(v\) always lies in the resulting interval. By construction, every atomic constraint in \(C_{\max}\) is satisfied by \(v\).
The final guard is obtained by sampling a geometrically sized random subset of \(\mathtt{subexpr}(C_{\max})\). Since all atomic constraints in \(C_{\max}\) are satisfied by \(v\), any conjunction of a subset of them is also satisfied by \(v\). Hence, for the returned guard \(G\), \(\llbracket C \rrbracket \cap \llbracket G \rrbracket \neq \emptyset.\) In particular, when the procedure is instantiated with the invariant of the source location as seed CIG, 4 holds.
When instantiated with the trivial seed guard \(\top\), the procedure produces satisfiable guards, establishing 2. Instantiating the initial location invariant with \(\bigwedge_{x \in X} x = 0\) ensures that the generated invariant intersects the all-zeros valuation, establishing 3. Finally, the guards induced by CIGs contain no redundant sub-expressions, since they are conjunctions of atomic constraints that are not implied by each other, ensuring 5.
4.3.0.6 Model specification.
A model specification is a user-supplied configuration controlling the intended size and density of generated PTAs; it is the input to ConstructSchema. Here \(\mathbb{I}_{\geq 1}\) denotes the set of non-empty closed intervals \([a,b]\) with \(a,b\in\mathbb{N}_{\geq 1}\), used to specify size ranges.
Definition 19 (model specification). A model specification* is a tuple \(\mathcal{M}= (I_{L}, I_{X}, I_{P}, I_{K}, p_{Inv}, p_{g}, p_{R}, N)\) where:*
\(I_{L}\in \mathbb{I}_{\geq 1}\) is the size interval for locations,
\(I_{X}\in \mathbb{I}_{\geq 1}\) is the size interval for clocks,
\(I_{P}\in \mathbb{I}_{\geq 1}\) is the size interval for parameters,
\(I_{K}\in \mathbb{I}_{\geq 1}\) is the size interval for outgoing transitions per location,
\(p_{Inv}\in [0,1]_{\mathbb{R}}\) is the probability of a non-trivial location invariant,
\(p_{g}\in [0,1]_{\mathbb{R}}\) is the probability of a non-trivial transition guard,
\(p_{R}\in [0,1]_{\mathbb{R}}\) is the probability of a clock reset on a transition,
\(N\in \mathbb{N}_{\geq 1}\) is the maximum constant in linear terms.
4.3.0.7 Schema assembly.
ConstructSchema (5) assembles the component distributions into a generator schema \(\Sigma\), wiring each parameter of \(\mathcal{M}\) to the appropriate distribution constructor.
The set distributions \(\mathfrak{L}, \mathfrak{X}, \mathfrak{P}\) sample finite sets from the specified size intervals. The graph distribution \(\mathfrak{G}\) first samples per-location outdegrees, then delegates to GraphGen. The invariant distributions encode the initial-location constraint (3) by instantiating GuardGen with \(\bigwedge_{x \in X} x = 0\) at the initial location and \(\top\) elsewhere. The guard distribution instantiates GuardGen with the invariant of the source location \(\mathit{Inv}(\ell)\), ensuring guard–invariant intersection (4) by construction. Clock resets complete the schema.
5 Property-Preserving Shrinking↩︎
Once a PTA violating the target property has been identified, the framework applies a shrinking phase inspired by delta debugging [10] and test-case reduction [11]: the model is iteratively reduced while verifying that the target property is preserved. The goal is to quickly obtain a small and comprehensible witness suitable for inspection and debugging, rather than to compute a formally minimal automaton.
The shrinker is intentionally agnostic to the nature of the target property, which is treated as an external oracle. Unlike generation, which enforces global semantic constraints by construction, shrinking is inherently heuristic and oracle-guided. We therefore present the shrinker in terms of design principles and a staged shrinking procedure.
5.1 Shrinker Design Goals↩︎
We adopt a principle of parsimony: the shrinker aims to eliminate components of a witness PTA that are not relevant to satisfying the target property. Parsimony is not understood as formal minimality, but as a practical criterion for removing unnecessary structure while preserving the property of interest.
5.1.0.1 Preservation of Target Property
Every accepted shrinking step must preserve the target property; a shrunk PTA that no longer witnesses the violation is useless.
5.1.0.2 Monotonic Progress
Each shrinking step strictly decreases a chosen measure of model size or complexity, such as the number of locations, transitions, clocks, or constraints. This guarantees progress and termination, and enforces parsimony by ensuring each accepted step removes structure rather than rearranging it.
5.1.0.3 Well-Formedness Preservation
All shrinking operators preserve well-formedness of parametric timed automata. In particular, the shrinker avoids introducing ill-defined models, such as PTAs with inconsistent clock constraints or syntactically invalid components. This ensures parsimony does not produce degenerate or semantically meaningless witnesses.
5.1.0.4 Locality and Modularity
The shrinker is structured as a collection of local and independent operators, each targeting a specific aspect of the PTA. This modular design supports parsimony through fine-grained elimination of unnecessary components without globally restructuring the model, and allows operators to be combined flexibly.
5.2 Shrinking Procedure↩︎
The shrinker applies a staged, deterministic shrinking pipeline, where each stage enforces parsimony at a different structural level. Each stage is applied repeatedly until no further shrinking steps are found; the procedure does not backtrack or reorder stages. The overall procedure is as follows:
Transition Removal. Transitions are removed one at a time, accepting a removal only if the target property is preserved.
Reachability Normalization. After transition removals, all unreachable locations are deterministically eliminated (not property-dependent).
Invariant and Guard Simplification. Guards and invariants are simplified by removing conjuncts, provided the target property remains satisfied.
Location Coalescing. Locations are merged when possible while preserving well-formedness and satisfaction of the target property.
Variable Cleanup. Unused clocks and parameters (not appearing in guards, invariants, or resets) are removed in a final cleanup step (not property-dependent).
6 Implementation and Evaluation↩︎
We instantiate the framework as a differential testing tool [9] for PTA analysis algorithms: two configurations of the same algorithm—or two algorithms whose outputs should agree on a shared model class—are run on each generated PTA, and disagreement serves as the target property \(\varphi\). Concretely, given two analysis procedures \(\Pi_1\) and \(\Pi_2\), we define \[\varphi(\mathcal{A}) \;\triangleq\; \Pi_1(\mathcal{A}) = \Pi_2(\mathcal{A}).\] Whenever \(\varphi\) is violated, the shrinking procedure reduces the witness to a local minimum, yielding a small and actionable counterexample. This strategy is especially effective for testing optimizations and implementation-specific heuristics: if \(\Pi_2\) is a trusted reference and \(\Pi_1\) an optimized variant, any counterexample to \(\varphi\) pinpoints a semantic inconsistency introduced by the optimization.
6.1 Implementation Details↩︎
The framework is implemented as a meta-tool within the Imitator model checker [2]. The generator is realized as a custom random PTA generator adhering to the design principles of 4, while the reducer implements the property-preserving shrinking procedure described in 5.3
Imitator provides multiple PTA analysis procedures; in this section, we focus on three relatively recent additions: a parametric timed game (PTG) algorithm [12], currently under active development; an unavoidability (AF) synthesis algorithm [13], an experimental implementation of an established theory; and an NDFS algorithm [14] for detecting accepting cycles, a mature and well-tested procedure. All three expose numerous toggleable optimizations and features, making them suitable candidates for differential validation.
6.2 Experimental Setup↩︎
All experiments were conducted on a single core of a computer with an Intel Core i5-1135G7 CPU @ 2.40GHz with 16 GB of RAM running Ubuntu 22.04.5 LTS. Each experiment ran with \(r = 100{,}000\) random iterations per seed, repeated over 5 seeds, with a per-run time limit of 0.1 seconds. Each experiment compares two configurations of Imitator on the same randomly generated PTA; a disagreement in their outputs triggers the shrinking procedure. Seeds that did not find a counterexample within \(r\) iterations are included in the average count with a value of \(r\), giving a conservative estimate. 1 summarizes the results.
If a bug was found and later fixed, the experiment is run on an older version of Imitator and the counterexample is confirmed as fixed on the latest version. Three experiments—PTG-Closed-Clock-Bug, PTG-Explore-Bug, and PTG-Invariant-Bug—target distinct bugs in the PTG algorithm by comparing the base implementation against a version with a new convex hull abstraction. The bugs themselves were found to be unrelated to the abstraction, but the difference in state space size and exploration order makes each bug manifest in the comparison. PTG-Double-Inclusion-Bug targets a bug in the double inclusion (two-way subsumption) check of the PTG algorithm, comparing the base implementation against one with the check enabled. This check is still experimental and the bug has not yet been fixed. AF-Bug compares the PTG and AF synthesis algorithms on the same models, exploiting the fact that their outputs should agree on a subclass of PTA; it finds a bug in the AF algorithm that has not yet been fixed. The final two experiments, NDFS-Check and AF-Double-Inclusion-Check, serve as negative controls, comparing two configurations of the same algorithm that should produce identical outputs.
| Experiment | Seeds | Avg.count | Reduction | Final size | Fixed |
|---|---|---|---|---|---|
| PTG-Closed-Clock-Bug | 4/5 | 58624 | 21% / 48% | 4 / 4 | Yes |
| PTG-Explore-Bug | 3/5 | 68081 | 36% / 54% | 5 / 6 | Yes |
| PTG-Double-Inclusion-Bug | 5/5 | 853 | 20% / 60% | 3 / 5 | No |
| PTG-Invariant-Bug | 3/5 | 54374 | 42% / 66% | 4 / 4 | Yes |
| AF-Bug | 5/5 | 14 | 67% / 93% | 2 / 1 | No |
| NDFS-Check | 0/5 | – | – | – | – |
| AF-Double-Inclusion-Check | 0/5 | – | – | – | – |
6.3 Discussion↩︎
The results confirm that the framework reliably exposes semantic disagreements across a range of algorithm configurations. The wide variance in average PTA count (14–68081) reflects differences in bug rarity: AF-Bug is triggered by a common structural pattern, whereas PTG-Explore-Bug requires a more specific combination of features. The shrinking procedure consistently produces substantial reductions, removing up to 93% of transitions and 67% of locations. The two bugs marked as not yet fixed (PTG-Double-Inclusion-Bug and AF-Bug) were confirmed present in the current Imitator release at time of writing, and the generated counterexamples are small and informative enough to be directly actionable for debugging. For instance, the AF-Bug counterexample consists of a PTA with only 2 locations and 1 transition and is most likely an unhandled edge case. The two negative-control experiments produced no counterexamples, confirming the absence of spurious disagreements.
7 Conclusion↩︎
The experiments confirm that analysis algorithms under active development harbour corner-case bugs that standard benchmark suites do not exercise. The proposed generate-and-shrink framework surfaces such bugs reliably and reduces any witness to a small, actionable counterexample; the smallest found consists of just two locations and one transition, yet exposes a fault that had gone undetected in Imitator until now.
The framework has two main limitations. First, differential testing requires that the algorithms under comparison produce deterministic output; non-deterministic implementations may yield spurious disagreements. Second, the shrinking procedure finds a locally minimal witness rather than a globally minimal one: a smaller counterexample may exist. The framework is most naturally positioned as a development tool — cheap to run and requiring no oracle — and extends naturally to other classes of quantitative automata, which we leave to future work.
References↩︎
This work was supported by Innovationsfonden Danmark’s DIREC project SIoT (Secure Internet of Things).↩︎
This preprint has not undergone peer review (when applicable) or any post-submission improvements or corrections. The Version of Record of this contribution is published in TASE 2026, and is available online at https://doi.org/10.1007/978-3-032-30693-7_13.↩︎
Available at github.com/imitator-model-checker/imitator↩︎