# Efficient Convex Zone Merging in Parametric Timed Automata

Étienne André, Dylan Marinho, Laure Petrucci, Jaco van de Pol

► To cite this version:

Étienne André, Dylan Marinho, Laure Petrucci, Jaco van de Pol. Efficient Convex Zone Merging in Parametric Timed Automata. 20th International Conference on Formal Modeling and Analysis of Timed Systems, Sep 2022, Warsaw, Poland. pp.200-218, 10.1007/978-3-031-15839-1_12. hal-03772708

HAL Id: hal-03772708

https://hal.science/hal-03772708v1

Submitted on 20 Mar 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Efficient Convex Zone Merging
in Parametric Timed Automata*

Étienne André¹, Dylan Marinho¹, Laure Petrucci², and Jaco van de Pol³

¹ Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

² LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord, Villetaneuse, France

³ Aarhus University, Aarhus, Denmark

**Abstract.** Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. Reducing their state space is a significant way to reduce the inherently large analysis times. We present here different merging reduction techniques based on convex union of constraints (parametric zones), allowing to decrease the number of states while preserving the correctness of verification and synthesis results. We perform extensive experiments, and identify the best heuristics in practice, bringing a significant decrease in the computation time on a benchmarks library.

**Keywords:** parametric timed model checking · parameter synthesis · convex merging.

# 1 Introduction

Parametric timed automata (PTAs) [AHV93] are a powerful extension of timed automata (TAs) [AD94] with timing parameters, allowing to reason on concurrent real-time systems with unknown or uncertain timing constants. PTAs go beyond the expressiveness of the classical model checking problem of TAs (with a binary "yes"/"no" answer), and can address *parameter synthesis*, i.e. the exhibition of valuations for these timing parameters s.t. a given property holds. A common problem (addressed here) is that of *reachability synthesis*: "synthesize parameter valuations such that a given location is reachable".

PTAs are an inherently expressive but hard formalism, in the sense that most decision problems are undecidable (see e.g. [And19] for a survey), while verification and parameter synthesis are subject to the infamous state space explosion in practice. Reducing the state space, built on-the-fly when performing parameter synthesis, is a significant way to reduce the sometimes large computation times.

<footnote>* This is the author version of the manuscript of the same name published in the proceedings of the 20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2022). The final version is available at 10.1007/978-3-031-15839-1_12. This work is partially supported by the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015) and CNRS-INS2I project TrAVAIL.</footnote>
The symbolic semantics of TAs is often represented as *zones*, i.e. linear con-
straints over the clocks with a special form. In [Dav05], a convex zone merging
technique is presented for UPPAAL, that preserves reachability properties. This
merging technique was extended to PTAs in [AFS13], and applied to the symbolic
semantics of PTAs in the form of parametric zones, i.e. linear constraints over
the clocks and the parameters, obeying to a special form [Hun+02]. In [AFS13],
the analysis is only performed in the framework of the “inverse method” (IM,
also called “trace preservation synthesis” [ALM20]); no other properties are con-
sidered.

*Contributions.* We propose here different merging techniques for PTAs, with the goal to reduce the state space size and/or the analysis time. We implement our techniques in *IMITATOR* [And21], and we perform extensive experiments on a standard benchmarks set [AMP21]. It turns out that these various heuristics have very different outcomes in terms of size of the state space and analysis speed. We then identify the best heuristics in practice, allowing to significantly decrease the number of states and the computation time, while preserving the correctness of the parameter synthesis for the whole class of reachability properties. The two main differences with [AFS13] are *i*)* the definition of merging for reachability synthesis (and not only for IM), and *ii*)* the systematic investigation of new heuristics, leading to a largely increased efficiency w.r.t. the original merging of [AFS13].

*Related work.* As said above, merging was first proposed for TAs in [Dav05], and then extended to the “inverse method” for PTAs in [AFS13]. In [BBM06], Ben Salah et al. show that it is safe to perform the convex merging of various constraints, when they are the result of an interleaving. The exploration is done in a BFS (breadth-first search) manner, and states are merged at each depth level.

Beyond merging, various heuristics were proposed to efficiently reduce the
state space of TAs. Extrapolation and abstractions were proposed in [AD94;
Beh+06; HSW13; HSW16] for TAs, and then extended to PTAs in [ALR15;
Bez+16]. Exploration orders were discussed in [HT15] and then in [ANP17]
for PTAs. The efficiency of model checking liveness properties for TAs is dis-
cussed notably in [HSW12; Her+20]. Zone inclusion (subsumption) for liveness
checking is discussed for TAs in [Laa+13] and for PTAs in [And+21]. Inclu-
sion/subsumption is a special case of merging. The other mentioned techniques
are orthogonal to the merging technique, and they can be combined.

In addition, computing efficiently exact or over-approximated successors of
"zones" in the larger class of *hybrid automata* (HAs) [Hen96] is an active field
of research (e.g. [CÁF11; CSÁ14; SNÁ17; Bog+20]). Beyond the target formal-
ism (PTAs instead of HAs), a main difference is that we are concerned here
exclusively with an *exact* analysis.

*Outline* We recall the necessary concepts in Section 2. Several merging heuristics are proposed in Section 3 and evaluated in Section 4. We conclude in Section 5.
## 2 Preliminaries

We assume a set $\mathbb{X} = \{x_1, \dots, x_H\}$ of clocks, i.e. real-valued variables that evolve over time at the same rate. A clock valuation is a function $\mu : \mathbb{X} \to \mathbb{R}_{\ge 0}$. The clock valuation $\bar{0}$ assigns 0 to all clocks. Given a delay $d \in \mathbb{R}_{\ge 0}$, $\mu + d$ denotes the valuation $(\mu + d)(x) = \mu(x) + d$, for $x \in \mathbb{X}$. Given $R \subseteq \mathbb{X}$, we define the reset of valuation $\mu$ by $[\mu]_R(x) = 0$ if $x \in R$, and $[\mu]_R(x) = \mu(x)$, otherwise.

We assume a set $\mathbb{P} = \{p_1, \dots, p_M\}$ of parameters, i.e. unknown constants. A linear term is of the form $\sum_{1 \le i \le H} \alpha_i x_i + \sum_{1 \le j \le M} \beta_j p_j + d$, with $\alpha_i, \beta_j, d \in \mathbb{Z}$. A constraint $\mathbf{C}$ (i.e. a convex polyhedron) over $\mathbb{X} \cup \mathbb{P}$ is a conjunction of inequalities of the form $\text{lt} \succcurlyeq 0$, where $\text{lt}$ is a linear term and $\succcurlyeq \in \{<, \le, =, \ge, >\}$.

A parameter valuation $v$ is a function $v : \mathbb{P} \to \mathbb{Q}_{\ge 0}$. Given a parameter valuation $v$, $v(\mathbf{C})$ denotes the constraint over $\mathbb{X}$ obtained by replacing each parameter $p$ in $\mathbf{C}$ with $v(p)$. Likewise, given a clock valuation $\mu$, $\mu(v(\mathbf{C}))$ denotes the expression obtained by replacing each clock $x$ in $v(\mathbf{C})$ with $\mu(x)$. We write $\mu \models v(\mathbf{C})$ if $\mu(v(\mathbf{C}))$ evaluates to true. We say that $\mathbf{C}$ is satisfiable if $\exists \mu, v \text{ s.t. } \mu \models v(\mathbf{C})$.

**Definition 1 (PTA [AHV93]).** A PTA $\mathcal{A}$ is a tuple $\mathcal{A} = (\Sigma, L, \ell_0, \mathbb{X}, \mathbb{P}, I, E)$, where: i) $\Sigma$ is a finite set of actions, ii) $L$ is a finite set of locations, iii) $\ell_0 \in L$ is the initial location, iv) $\mathbb{X}$ is a finite set of clocks, v) $\mathbb{P}$ is a finite set of parameters, vi) $I$ is the invariant, assigning to every $\ell \in L$ a constraint $I(\ell)$, vii) $E$ is a finite set of edges $e = (\ell, g, a, R, \ell')$ where $\ell, \ell' \in L$ are the source and target locations, $a \in \Sigma$, $R \subseteq \mathbb{X}$ are the set of clocks to be reset, and the guard $g$ is a constraint.

Given a parameter valuation $v$, $v(\mathcal{A})$ denotes the non-parametric TA [AD94], where all occurrences of any parameter $p_i$ have been replaced by $v(p_i)$.

**Definition 2 (Concrete semantics).** Given PTA $\mathcal{A} = (\Sigma, L, \ell_0, \mathbb{X}, \mathbb{P}, I, E)$, and a parameter valuation $v$, the concrete semantics of $v(\mathcal{A})$ is given by the timed transition system (TTS) [HMP91; AD94] $T_{v(\mathcal{A})} = (S, s_0, \xrightarrow{e} \cup \xrightarrow{d})$, with

- $S = \{(\ell, \mu) \in L \times \mathbb{R}_{\ge 0}^H \mid \mu \models v(I(\ell))\}$,

- initial state $s_0 = (\ell_0, \bar{0})$,

- discrete transitions: $(\ell, \mu) \stackrel{e}{\mapsto} (\ell', \mu')$, if $(\ell, \mu), (\ell', \mu') \in S$, and there exists $e = (\ell, g, a, R, \ell') \in E$, such that $\mu' = [\mu]_R$, and $\mu \models v(g)$.

- delay transitions: $(\ell, \mu) \stackrel{d}{\mapsto} (\ell, \mu+d)$ for $d \in \mathbb{R}_{\ge 0}$, if $\forall d' \in [0, d], (\ell, \mu+d') \in S$.

We write $(\ell, \mu) \xrightarrow{(d,e)} (\ell', \mu')$ for a combined step: $\exists \mu'' : (\ell, \mu) \stackrel{d}{\mapsto} (\ell, \mu'') \stackrel{e}{\mapsto} (\ell', \mu')$.

Given a TA $v(\mathcal{A})$ with concrete semantics $T_{v(\mathcal{A})} = (S, s_0, \rightarrow)$, we refer to the states of $T_{v(\mathcal{A})}$ as the concrete states of $v(\mathcal{A})$. A run of $v(\mathcal{A})$ is a (finite or infinite) alternating sequence of concrete states of $v(\mathcal{A})$ and pairs of delay and discrete transitions starting from the initial state $s_0$ of the form $s_0, (d_0, e_0), s_1, \dots$ with $i = 0, 1, \dots, e_i \in E, d_i \in \mathbb{R}_{\ge 0}$ and $s_i \xrightarrow{(d_i, e_i)} s_{i+1}$.

Given a state $s = (\ell, \mu)$, we say that $s$ is reachable in $v(\mathcal{A})$ if $s$ appears in a run of $v(\mathcal{A})$. By extension, we say that $\ell$ is reachable in $v(\mathcal{A})$.
**Symbolic Semantics.** We now recall the symbolic semantics of PTAs (see e.g. [Hun+02; And+09; JLR15]). Define the *time elapsing* of $\mathbf{C}$, denoted by $\mathbf{C}^\rightarrow$, as the constraint over $\mathcal{X}$ and $\mathbb{P}$ obtained by delaying all clocks in $\mathbf{C}$ by an arbitrary amount of time. That is, $\mu' \models v(\mathbf{C}^\rightarrow)$ if $\exists \mu : \mathcal{X} \to \mathbb{R}_{\ge 0}, \exists d \in \mathbb{R}_{\ge 0} \text{ s.t. } \mu \models v(\mathbf{C}) \wedge \mu' = \mu + d$. Given $R \subseteq \mathcal{X}$, define the *reset* of $\mathbf{C}$, denoted by $[\mathbf{C}]_R$, as the constraint obtained from $\mathbf{C}$ by resetting the clocks in $R$ to 0, keeping other clocks unchanged. That is,

$$ \mu' \models v([\mathbf{C}]_R) \text{ if } \exists \mu : \mathcal{X} \to \mathbb{R}_{\ge 0} \text{ s.t. } \mu \models v(\mathbf{C}) \wedge \forall x \in \mathcal{X} \begin{cases} \mu'(x) = 0 & \text{if } x \in R \\ \mu'(x) = \mu(x) & \text{otherwise.} \end{cases} $$

We denote by $\mathbf{C} \downarrow_P$ the projection of $\mathbf{C}$ onto $\mathbb{P}$, i.e. obtained by eliminating the variables not in $\mathbb{P}$ (e.g. using Fourier-Motzkin). The application of one of these operations (time elapsing, reset, projection) to a constraint yields a constraint; existential quantification can be handled, e.g. by adding variables and subsequently eliminating them using, e.g. Fourier-Motzkin.

A symbolic state is a pair $(\ell, \mathbf{C})$ where $\ell \in L$ is a location, and $\mathbf{C}$ its associated constraint over $\mathcal{X} \cup \mathbb{P}$ called *parametric zone*.

**Definition 3 (Symbolic semantics).** Given a PTA $\mathcal{A} = (\Sigma, L, \ell_0, \mathcal{X}, \mathbb{P}, I, E)$, the symbolic semantics of $\mathcal{A}$ is the labelled transition system called parametric zone graph $\mathbf{PZG} = (E, \mathbf{S}, \mathbf{s}_0, \Rightarrow)$, with

$$ - \mathbf{S} = \{(\ell, \mathbf{C}) \mid \mathbf{C} \subseteq I(\ell)\}, $$

$$ - \mathbf{s}_0 = (\ell_0, (\bigwedge_{1 \le i \le H} x_i = 0)^\rightarrow \wedge I(\ell_0)), \text{ and} $$

$$ - ((\ell, \mathbf{C}), e, (\ell', \mathbf{C}')) \in \Rightarrow \text{ if } e = (\ell, g, a, R, \ell') \in E \text{ and } \mathbf{C}' = (([\mathbf{C} \wedge g])_R \wedge I(\ell'))^\rightarrow \wedge I(\ell') \text{ with } \mathbf{C}' \text{ satisfiable.} $$

That is, in the parametric zone graph, nodes are symbolic states, and arcs are labeled by *edges* of the original PTA. Given a symbolic state $\mathbf{s}$ reachable in $\mathbf{PZG}$, we define *SuccE($\mathbf{s}$)*, successors with edges, by $\{(e, \mathbf{s}') \mid (\mathbf{s}, e, \mathbf{s}') \in \Rightarrow\}$. We also write $\mathbf{s} \Rightarrow \mathbf{s}'$ to denote that for some $e$, $(\mathbf{s}, e, \mathbf{s}') \in \Rightarrow$. Given $\mathbf{t} = (\mathbf{s}, e, \mathbf{s}') \in \Rightarrow$, *t.source* denotes $\mathbf{s}$ while *t.target* denotes $\mathbf{s}'$. Given $\mathbf{s} = (\ell, \mathbf{C})$, *s.constr* denotes $\mathbf{C}$ while *s.loc* denotes $\ell$. Note that we usually use bold font to denote anything symbolic, i.e. (sets of) symbolic states, and constraints.

A well-known result [Hun+02] is that, given a PTA $\mathcal{A}$ and a reachable symbolic state $(\ell, \mathbf{C})$, if a parameter valuation $v$ belongs to the projection onto the parameters of $\mathbf{C}$ (i.e. $v \in \mathbf{C} \downarrow_P$), then $\ell$ is reachable in the TA $v(\mathcal{A})$.

The (*symbolic*) state space of a PTA is its parametric zone graph. This structure is in general infinite, due to the intrinsic undecidability of most decision problems for PTAs. However, for semi-algorithms for parameter synthesis (without a guarantee of termination), it is of utmost importance to *reduce* the size of this state space, so as to perform synthesis more efficiently.
# 3 Efficient State Merging in Parametric Timed Automata

## 3.1 Merging Algorithm

We recall the notion of merging from [AFS13]. Two states are mergeable if 1) they share the same location, and 2) the union of their constraints is convex.

**Definition 4 (Merging [AFS13]).** Two symbolic states $s_1 = (\ell_1, C_1)$, $s_2 = (\ell_2, C_2)$ are mergeable, denoted by the predicate is_mergeable($s_1, s_2$), if $\ell_1 = \ell_2$ and $C_1 \cup C_2$ is convex.

In that case, we define their merging as $(\ell_1, C_1 \cup C_2)$.

Merging is a generalisation of inclusion abstraction (also known as subsumption). Note that if $s_2$ includes $s_1$, i.e. $C_1 \subseteq C_2$, then $C_1 \cup C_2 = C_2$ is convex, so the states can be merged, and the result will be $s_2$.

**Example 1.** We display examples of 2-dimensional zones in Fig. 2c. (These box-shaped parametric zones are fictitious and displayed for the purpose of illustration; similar zones, sometimes using “diagonal” edges, can be obtained from actual PTAs.) Zone $C_1$ can be merged with $C_4$; $C_2$ can also be merged with $C_4$. The result of these two merging operations is shown in Fig. 2g. These two new zones can also be merged together, leading to the zone in Fig. 2h.

**Example 2.** Let us now consider the PTA in Fig. 1a, with two clocks ($x$ and $y$) and two parameters ($p$ and $q$). Both clocks and parameters are initially bound to be non-negative (clocks initially different from 0 can be simulated using an appropriate gadget, omitted here).

The PZG of this PTA is shown in Fig. 1b. It features two separate infinite executions which depend on the first chosen transition. In the upper branch, the first state with location $\ell_1$ has constraint $p + x \ge y$ (which can read $y - x \le p$) since, although we have $y \le p$ when taking the transition from $\ell_0$, time can then elapse in $\ell_1$—but only up to $p$ time units, due to invariant $x \le p$. Then coefficients on $p$ (i.e. $2p$ then $3p$, etc.) start to appear from the second state with location $\ell_1$ due to the self-loop on $\ell_1$ that resets $x$.

Inclusion reduces one of these two symbolic executions, which exhibits decreasing zones, as in Fig. 1c. Even using inclusion, the PZG remains infinite.

Finally, Fig. 1d displays the graph obtained with the *merging* approach: the two states obtained after taking a single transition can be merged. Here, the PZG with merging becomes finite, which illustrates the importance of merging.

**Algorithm 1** constructs the state space for a given PTA $\mathcal{A}$ by breadth-first search (BFS) from the initial state $s_0$. It computes the set of reachable states *Visited* by repeatedly adding the next layer of successor states $Q_{new}$ (line 6), maintaining the transitions (line 7). Note that each iteration (line 9) calls a merging function *mergeSets* (given in Algorithm 2), which may reduce both **Visited** and **Queue**. This call to the merging function is the crux of our approach.

**Algorithm 1** can be extended, depending on the analysis or parameter synthesis problem. For instance, an invariant property can be checked for each reachable
<figure><img src="image_2.png" /><figcaption>Fig. 1: Example with infinite PZG that becomes finite by merging</figcaption></figure>

<table><thead><tr><th colspan="2">Algorithm 1: BFS by layer layerBFS(A)</th></tr></thead><tbody><tr><td colspan="2">/* Building PZG = (E, Visited, s<sub>0</sub>, ⇒) */</td></tr><tr><td>1</td><td>Visited ← {s<sub>0</sub>} ; Queue ← {s<sub>0</sub>} ; ⇒ ← ∅</td></tr><tr><td>2</td><td>while Queue ≠ ∅ do</td></tr><tr><td>3</td><td>Q<sub>new</sub> ← ∅</td></tr><tr><td>4</td><td>foreach s ∈ Queue do</td></tr><tr><td>5</td><td>foreach (e, s') ∈ SuccE(s) do</td></tr><tr><td>6</td><td>Q<sub>new</sub> ← Q<sub>new</sub> ∪ ({s'} \ Visited)</td></tr><tr><td>7</td><td>⇒ ←⇒ ∪ ({s, e, s'})</td></tr><tr><td>8</td><td>Visited ← Visited ∪ Q<sub>new</sub></td></tr><tr><td>9</td><td>Visited, Queue ← mergeSets(PZG, Visited, Q<sub>new</sub>)</td></tr></tbody></table>

symbolic state and terminate as soon as the property is violated. For reachability synthesis, one may accumulate all solutions as a set of constraints that lead to a state satisfying a property (this algorithm, EFsynth, was formalized in e.g. [JLR15]).

Then, Algorithm 2 “simply” calls recursively the `mergeOneState` function (given in Algorithm 3) on each state of `Queue`, using additional arguments `PZG` and `Visited` and/or `Queue`. The heuristics to select arguments for calls to `mergeOneState` will be discussed later. Note that `mergeOneState` modifies its arguments, notably `PZG` (in the implementation, we use a call by reference).

Algorithm 3 attempts at merging a state `s` while looking for candidate states in `SiblingCandidates`. We first look for the siblings of `s` (states with same location) within `SiblingCandidates` (line 3). We use a function `getSiblings((ℓ, C), S)` that returns the siblings, as in `{(ℓ', C') ∈ S | ℓ = ℓ'}`. If the union of the constraints is convex (line 5), state `s` becomes the result of
<table><caption>**Algorithm 2:** Heuristics to merge states within *Q* and/or *V*</caption><thead><tr><th>State</th><th>Algorithm</th></tr></thead><tbody><tr><td>Visited</td><td><code>mergeSets(PZG, V, Q)</code></td></tr><tr><td>Queue</td><td><code>foreach s ∈ Q do</code></td></tr><tr><td>Ordered</td><td><pre><code>mergeOneState(s, PZG, Q)</code></pre><pre><code>mergeOneState(s, PZG, V)</code></pre></td></tr><tr><td>4</td><td><code>return (V, Q)</code></td></tr></tbody></table>

merging *s* with the candidate *y* (line 6). The candidate *y* is deleted (line 11), as well as all transitions leading to or coming from it (lines 8 to 10). We finally modify the initial state *s*₀ of **PZG**, in case it was merged (line 12).

## 3.2 Heuristics for Merging

We now introduce and discuss several heuristics for merging states, leading to various options in the merging algorithm. There is no provably best option that is guaranteed to be superior over all other possible options. We will perform extensive experiments in Section 4 to find out what works well on a number of benchmarks. The two main driving forces to select between these options are: 1) a maximal reduction of the state space; and 2) a minimisation of the computation time. Although usually smaller state spaces tend to require less computation time, this is not always the case: Sometimes one might need extra effort to check if states can be merged, in order to perform even more reduction. Subsequent computations might profit from the smaller state space, but if one is checking properties on-the-fly, the extra effort might not be justifiable. The discussion on the options will be guided by some questions. A question that we have not investigated is if it is advantageous to merge triples of states.

The subsequent **Example 3** will show that different choices can indeed lead to state spaces of different size. Note that, even when we fix the answers to the questions, the result is still non-deterministic, since the result of merging depends on the *order* in which we would consider the siblings.

**Question 1:** *What to merge with what?* Assume that we are computing the next level of reachable states in a BFS process (Algorithm 1). Assuming that the states in **Visited** have been properly merged, we clearly still need to merge the new states in *s* ∈ **Queue**. What to merge them with? Do we only compare *s* with other states in the **Queue**? Or also with **Visited**? If we merge with **Visited** states, the final state space could become smaller. On the other hand, since time was spent to compute those states already, is it worth looking at them? The different strategies considered merge a new state with its siblings:

- only in the queue (**Queue**), or

- in all visited states (**Visited**) (including the queue), or
<table><caption>**Algorithm 3:** Merging a state with an update of the statespace $\mathbf{PZG} = (E, \mathbf{S}, \mathbf{s}_0, \Rightarrow)$ on-the-fly. The variant with restart after a merge is indicated as in **Restart**</caption><thead><tr><th></th><th></th><th></th></tr></thead><tbody><tr><td>1</td><td>Function <i>mergeOneState</i>(s, PZG, SiblingCandidates)</td><td></td></tr><tr><td>2</td><td><i>isMerged</i> &leftarrow; false</td><td></td></tr><tr><td>3</td><td>Candidates &leftarrow; <i>getSiblings</i>(s, SiblingCandidates)</td><td></td></tr><tr><td>4</td><td>foreach y &isin; Candidates do</td><td></td></tr><tr><td>5</td><td><i>/* Mergeability test */</i></td><td></td></tr><tr><td>6</td><td>&nbsp;&nbsp;&nbsp;&nbsp;if <i>is_mergeable</i>(s, y) then</td><td></td></tr><tr><td>7</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<i>s.constr</i> &leftarrow; <i>s.constr</i> &cup; <i>y.constr</i></td><td></td></tr><tr><td>7</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<i>isMerged</i> &leftarrow; true</td><td></td></tr><tr><td>8</td><td><i>/* Update transition targets and source */</i></td><td></td></tr><tr><td>9</td><td>foreach t &isin; &rarr; do</td><td></td></tr><tr><td>10</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<i>if</i> t.target = y then t.target &leftarrow; s;<br/>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<i>if</i> t.source = y then t.source &leftarrow; s;</td><td></td></tr><tr><td>11</td><td><i>/* Delete y */</i></td><td></td></tr><tr><td>11</td><td><i>S</i> &leftarrow; <i>S</i> \ {y}</td><td></td></tr><tr><td>12</td><td><i>/* Handle initial state */</i></td><td></td></tr><tr><td>12</td><td>&nbsp;&nbsp;&nbsp;&nbsp;if <math><mrow><msub><mi>s</mi><mn>0</mn></msub><mo>=</mo><mi>y</mi><mo>then</mo><msub><mi>s</mi><mn>0</mn></msub><mo>&larr;</mo><mi>s</mi></mrow></math></td><td></td></tr><tr><td>13</td><td><i>if</i> <i>isMerged</i> then <i>mergeOneState</i>(s, PZG, SiblingCandidates);</td><td></td></tr></tbody></table>

– first in the queue and, after that, in the visited list (Ordered).

These different possibilities are pictured by different colours in Algorithm 2.

**Question 2: Restart after a merge?** The next question is what to do if we find that **s** could be merged with some **s'** into the (larger) **s**<sub>m</sub>? We have already searched through some set **Q**' of states before we found **s'**. Those states in **Q**' could not be merged with **s**. However, it could be possible that a state in **s''** ∈ **Q**' can be merged with **s**<sub>m</sub>. So should we restart the search (and lose some time to find more reduction), or should we just resume the search, and only find merge candidates for **s**<sub>m</sub> in the remaining states that we have not yet considered? So, if a state can be merged with one of its siblings, should we restart or not restart the search through all candidate siblings?

**Question 3: When to update the statespace?** Assume that we find a successful merge of a state **s** ∈ **Queue** with some other state **s'** ∈ **Visited**, leading to a larger state **s**<sub>m</sub>. How do we now modify the already computed part of the state space? We replace **s'** by **s**<sub>m</sub>, redirecting all transitions going to **s'** to **s**<sub>m</sub>. This could make the successors of **s'** unreachable, so we could also redirect transitions from **s'** to transitions from **s**<sub>m</sub>. Alternatively, we could just remove the successors of **s'**. This is valid, since we will still compute all successors of **s**<sub>m</sub> in the next level. Similar considerations apply to all states reachable from successors of **s'**.
These approaches can have unforeseen effects: First of all, if we remove suc-
cessor states, they cannot act anymore as merge candidates, thus potentially
blocking future merges. Second, removing transitions may change the “short-
est path” to reachable states, leading to wrong answers for depth-bounded and
shortest-path searches. Third, not removing states leads to a larger state space
than necessary. Finally, doing a full reachability analysis is linear in the size of the
state space generated so far (but does not involve any polyhedra computations).

So one question is how often we should update the computed part of the
state space? The options we considered are to do “garbage collection” after:

- each merge with each sibling, or

- having processed the whole candidate list of a state, or

- having processed all states in a complete level.

*Question 4: How to update the statespace?* The “garbage collection” can be implemented in two ways: If we can merge a state, we update the statespace:

- reconstruct: with a copy of the reachable part of the statespace, or

- on-the-fly: deleting the merged state and updating its transitions *in situ*.

Deleting states on-the-fly is cheaper than running a separate algorithm to mark
and copy the reachable part of the state space. However, note that when updating
transitions on-the-fly, some unnecessary successor states may stay in the state
space. These unnecessary states and transitions lead to a waste of memory. On
the other hand, they might still be useful as merge candidates for future merges.

*Example 3.* Recall that Fig. 2 presents a fictitious example summarising the effect of the options discussed in this section. The parametric zone graph (with five states) is shown in Fig. 2a, the corresponding projections of the zones on the parameters in Fig. 2c and the legend for the different colours in Fig. 2b. All states have the same location, hence may be candidates for merging. Two states ($s_0$ and $s_1$) are in the visited set, while two are in the queue ($s_2$ and $s_3$), and the last one, $s_4$, is currently being handled.

Let us first consider that the merge is only done with states in the queue.
Then $s_4$ is merged with $s_2$ and no merge with $s_3$ can occur. This leads to the
zones depicted in Fig. 2d.

Let us now consider that the merge is done with all visited states. Then the
following execution becomes possible: State $s_4$ could be first merged with $s_1$, leading to the zones in Fig. 2e. Now, if the restart option is used, this newly computed zone could be merged with $s_0$, leading to the zones in Fig. 2f. Note that we cannot merge the result with $s_2$ anymore.

Finally, let us consider the case where we merge with the queue first and
then with visited. State $s_4$ is then merged with $s_2$, as in Fig. 2d. Then no merge
with $s_3$ nor with $s_0$ can be performed, but a merge with $s_1$ is possible, leading
to Fig. 2g. If furthermore the state space is updated immediately after a merge,
the new state (instead of $s_4$) is merged with $s_1$, leading to Fig. 2h.
<figure><img src="image_3.png" /><figcaption>Fig. 2: Illustration of the merging options</figcaption></figure>

3.3 Preservation of Properties

**Proposition 1.** *Given a PTA *A*, let *PZG* and *PZG'* be the parametric zone graph before and after merging. Then *PZG'* simulates *PZG*.*

Proof (sketch). Consider the relation s ⊑ s' if and only if s.loc = s'.loc and s.constr ⊑ s'.constr. It is well-known [NPV18] that this forms a simulation relation, i.e. if s ⊑ s' and s ⇒ s₀, then for some s'₀, we have s₀ ⊑ s'₀ and s' ⇒ s'₀.

Note that while merging, we repeatedly replace a state (`l`, `C`) by a state (`l`, `C` ∪ `C'`), in which case (`l`, `C`) ⊑ (`l`, `C` ∪ `C'`). So indeed, merged states can simulate the behaviour of all original states that were merged.

**Corollary 1.** *Given a PTA *A*, let **PZG** and **PZG'** be the parametric zone graph before and after merging. Let $\varphi$ be a property in $\forall \text{CTL}^*$ with atomic propositions defined in terms of state locations only. Then **PZG**' $\models \varphi$ implies **PZG** $\models \varphi$.*

*Proof (sketch).* All universal properties (in $\forall \text{CTL}^*$) are preserved by simulation
$[BK08, \text{Thm 7.76}]$. In this case, the simulation $\sqsubseteq$ also implies that related states
have the same locations, so they satisfy the same atomic properties.

The next proposition shows that we do not add arbitrary new behaviour. Although merging can add behaviour, it cannot add unreachable locations and, more precisely, the set of locations reachable for each parameter valuation remains unchanged. This guarantees that merging preserves reachability synthesis. (A version of this result was shown in a different context in [AFS13, Thm. 1].)
**Proposition 2 (preservation of reachability properties).** Given a PTA $\mathcal{A}$, let $\mathbf{PZG}'$ be the parametric zone graph after merging. Let $\ell$ be a location, let $v$ be a parameter valuation.

$\ell$ is reachable in $v(\mathcal{A})$ iff $\exists (\ell, \mathbf{C}') \in \mathbf{PZG}'$ such that $v \in \mathbf{C}' \downarrow_P$.

Note that path properties in $\mathbf{PZG}$ are not always preserved in $\mathbf{PZG}'$, as the following example shows. Also, liveness properties in $\mathbf{PZG}$ (such as “every path visits location $\ell$ infinitely often”) are not necessarily preserved in $\mathbf{PZG}'$.

*Example 4.* Fig. 3b shows the parametric zone graph of the PTA in Fig. 3a. The maximal paths are $\ell_0, \ell_1, \ell_3, \ell_4$ and $\ell_0, \ell_1, \ell_3, \ell_2$ (for $p \le 1$) and $\ell_0, \ell_2, \ell_3$ (for $p > 1$). All maximal paths satisfy the LTL property $\mathbf{G}(\ell_2 \to \mathbf{G} \neg \ell_4)$ (“no $\ell_4$ after an $\ell_2$”). Also, there is no loop (infinite run) containing $\ell_2$. However, the result after merging in Fig. 3c introduces the spurious path $\ell_0, \ell_2, \ell_3, \ell_4$, violating the first property. It also introduces a spurious loop $\ell_0, (\ell_2, \ell_3)^\omega$, around $\ell_2$.

This example uses parameters, but no clocks. [Laa+13, Fig. 4] shows an example with only clocks (i.e. a timed automaton) where a spurious loop is introduced by zone inclusion (subsumption), which is just a special case of zone merging.

# 4 Experiments

We evaluate here the effect of the merging heuristics on reachability synthesis, i.e. the synthesis of the parameter valuations for which a given reachability property holds. The synthesis algorithm explores the PZG to find all valid parameter valuations.

We implemented all our heuristics in the IMITATOR parametric timed model checker [And21]. The parametric zones in the symbolic states are encoded using polyhedra. All operations on polyhedra, and notably the mergeability test, are performed using the Parma Polyhedra Library [BMZ08]. We also reimplemented and compared with the original merging technique of IMITATOR 2.12, which was an upgrade of the merging technique (in IMITATOR 2.6.1) of [AFS13].

<figure><img src="image_4.png" /><figcaption>Fig. 3: The original PZG satisfies $\mathbf{G}(\ell_2 \to \mathbf{G} \neg \ell_4)$, which is violated after merging. Similarly, merging introduces a spurious infinite loop containing $\ell_2$.</figcaption></figure>
## 4.1 Dataset and Experimental Environment

We use the full set of models with reachability properties from the IMITATOR benchmark library [AMP21]. The library is made of a set of *benchmarks*. Each benchmark may have different *models* and each model comes with one or more *properties*. For example, *Gear* comes with ten models, of different sizes, named *Gear-1000* to *Gear-10000*; each of them may have one or more properties.

Our dataset comprises 124 pairs made of a model and a reachability property (i.e. 124 possible executions of IMITATOR). We set a timeout of 120s; only 102 executions terminate within this time bound for at least one of the merging heuristics. For 42 of these executions, at least one of the heuristics performs at least one successful merge. Full statistics on our dataset are given in Table 1.

Experiments were run on an Intel Xeon Gold 5220 (Cascade Lake-SP, 2.20GHz, 1 CPU/node, 18 cores/CPU) with 96 GiB running Linux Ubuntu 20.4

## 4.2 Description of the Experiments

We compare each combination of the heuristics proposed in Section 3.2. We reference each merge heuristic as a combination of three or four letters:

1. R or O: the state-space is updated by reconstruction (R) or on-the-fly (O);

2. V,Q or O: the selected candidates are *Visited* (V), *Queue* (Q) or *Ordered* (O);

3. M or C: state-space is updated for each merge (M) or after all candidates (C);

4. r: the restart option is enabled (nothing otherwise).

These algorithms are compared according to: i) the total computation time needed for a property; and ii) the size of the generated state space.

Our results are obtained over the 102 executions of the dataset for which at least one algorithm ends before reaching the 120s timeout. We do not use any penalty on executions that do not end: their execution time is set to the timeout (120s) in the subsequent analyses. The metrics tagged by “(merge)” in Table 2 are computed over the 42 executions where some states can be merged, while the “(no merge)” only consider the 60 executions where no merge can be made.

We present in Table 2 some of the experimental results obtained for the different merge heuristics that allow the best reduction of computation time or in the state-space size. The results for all the heuristics are presented in Appendix A. In order to allow a good visualization of the results, the best result in each cell

<table><caption>Table 1: Size of our dataset</caption><thead><tr><th></th><th># benchmarks</th><th># models</th><th># properties</th></tr></thead><tbody><tr><td>Whole reachability dataset</td><td>49</td><td>84</td><td>124</td></tr><tr><td>Where at least one execution ends within 120s</td><td>35</td><td>68</td><td>102</td></tr><tr><td>Where at least one merge is performed</td><td>24</td><td>35</td><td>42</td></tr></tbody></table>

<footnote n="4">4 We used IMITATOR 3.3-beta-2 “Cheese Caramel au beurre salé”. Sources, binaries, models, raw results and full experiments tables are available at 10.5281/zenodo.6806915.</footnote>
<table><caption>Table 2: Partial results comparing merge heuristics</caption><thead><tr><th></th><th>Nomerge</th><th>M2.12</th><th>RVMr</th><th>OQM</th></tr></thead><tbody><tr><td rowspan="7">Time</td><td># wins</td><td>24</td><td>20</td><td>22</td><td>42</td></tr><tr><td>Avg (s)</td><td>10.0</td><td>5.47</td><td>4.56</td><td>3.77</td></tr><tr><td>Avg (merge) (s)</td><td>18.8</td><td>7.83</td><td>5.57</td><td>3.63</td></tr><tr><td>Avg (no merge) (s)</td><td>3.83</td><td>3.82</td><td>3.85</td><td>3.88</td></tr><tr><td>Median (s)</td><td>1.39</td><td>1.2</td><td>1.14</td><td>1.12</td></tr><tr><td>Norm. avg</td><td>1.0</td><td>0.91</td><td>0.91</td><td>0.87</td></tr><tr><td>Norm. avg (merge)</td><td>1.0</td><td>0.75</td><td>0.74</td><td>0.64</td></tr><tr><td></td><td>Norm. avg (no merge)</td><td>1.0</td><td>1.02</td><td>1.03</td><td>1.03</td></tr><tr><td rowspan="5">States</td><td># wins</td><td>0</td><td>19</td><td>37</td><td>16</td></tr><tr><td>Avg</td><td>11443.08</td><td>11096.54</td><td>11064.37</td><td>11120.79</td></tr><tr><td>Avg (merge)</td><td>1512.02</td><td>670.43</td><td>592.31</td><td>729.33</td></tr><tr><td>Median</td><td>2389.5</td><td>703.5</td><td>604.5</td><td>905.0</td></tr><tr><td>Norm. avg</td><td>1.0</td><td>0.86</td><td>0.84</td><td>0.88</td></tr></tbody></table>

is given in **bold**, while the level of green denotes the “quality” of the value in each cell (white is worst, and 100% green is best).

The different lines tabulate the following information: i) the number of wins over the computation time, i.e. the number of executions for which the current heuristics gives the smallest execution time; ii) the average time (in s) over all executions; iii) the average time (in s), excluding executions where no states can be merged for any heuristics; iv) the average time (in s) for only the executions where no states can be merged for any heuristics; v) the median time (in s) over all executions; vi) the normalized time average, compared to the Nomerge results, i.e. the ratio between the heuristic execution time and the Nomerge one; vii) the normalized time average, excluding executions where no states can be merged for any heuristics; viii) the normalized time average, for only the executions where no states can be merged for any heuristics; ix) the number of wins over the size of the state space (i.e. the total number of symbolic states after merging); x) the average size of the state space over all models; xi) the average size of the state space over all models, excluding the executions where no states can be merged; xii) the median size of the state space over all models; xiii) the normalized size average, compared to the Nomerge results.

The reason to give both an average time (resp. number of states) and a normalized time (resp. number of states) is because both metrics complement each other: the weight of the large models has a higher influence in the average (which can be seen as unfair, as a few models have a large influence), while all models have equal influence in the normalized average (which can also be seen as unfair, as very small models have the same influence as very large models).

In Table 2 (and in Appendix A), we notice that the best (i.e. smallest) times are obtained when the merging is performed on the queue and when the update is done after a performed merge, even though doing it with a reconstruction of the state space after each step loses time compared to the Otf heuristic. Moreover, restarting when a merge is performed does not seem to bring any gain in time. Thus, with respect to time, when the winner is OQM (i.e. merging when the candidates are taken from the Queue, when the update is done on-the-fly after each merge without any restart), which minimizes both the time when
a merge is possible, but also when considering models where no merge can be
performed. Moreover, this heuristic gives the smaller times for the executions
where no merge can be done.

Concerning the state space size, the winner is **RVMr** (i.e. merging when the
candidates are taken from the **Visited** states, updating the state space by a
reconstruction after each merge, and with a restart if a merge can be performed).
This performs more checks to identify states for merging (comparing with all the
visited, not only those in the queue), thus reducing the state space even more.

Note that the methods **Nomerge** and **M2.12** are almost always the losers (i.e. slowest and largest state space), except for the heuristic where the update of the state-space is performed after the list of candidates.

Concerning our new heuristics, we note that OQM decreases the average computation time to 69% when compared to the previous merging heuristic (M2.12 [AFS13]), and even to only 46% (i.e. a division by a factor > 2) compared with M2.12 on the subset of models for which at least one merge can be done. Compared to disabling merging (**Nomerge**), our new heuristic OQM decreases to 38% on the whole benchmark set, and even to 19% (i.e. a division by a factor > 5) on the subset of models for which at least one merge can be done. This leads us to consider the new combination of merging only in the queue and with an on-the-fly update after each merge and without restart (heuristic OQM) as the default merging heuristic in **IMITATOR**. For use cases that require a minimal state space, the new combination **RVMr** is the recommended option. Note that this version is still faster on average (83%) than the previous heuristic (M2.12), and more than twice as fast (46%) as not merging at all (**Nomerge**).

5 Conclusion

In this paper, we investigated the importance of the merging operations in reach-
ability synthesis using parametric timed automata. We investigated different
combinations of options. The chosen heuristic (OQM, when the candidates are
taken from the Queue, when the update is done on-the-fly after each merge with-
out any restart) brings a decrease to 38% of the average computation time for
our entire benchmarks library compared to the absence of merging. Compared
to the previous merging heuristic from [AFS13], the gain of our new heuris-
tic is a decrease to 69% of the average computation time—meaning that our
new heuristic decreases the computation time by 31% compared to the former
heuristic from [AFS13]. In other words, despite the cost of the mergeability test,
the overall gain is large and shows the importance of the merge operation for
parameter synthesis. We also provide a heuristic for use cases where a minimal
state space is important, for instance for a follow-up analysis. Even though this
is not the fastest heuristic, it is still faster than not merging at all, and faster
than the old merging heuristic [AFS13]. Our experiments show the high impor-
tance of carefully choosing the merging heuristics. Our heuristics preserve the
correctness of parameter synthesis for reachability properties.
*Future work.* We noted that pruning merged states away (“garbage collection”) can prevent future merges. Another option would be to keep such states in a collection of “potential mergers”. These extra states could be useful as “glue” to merge a number of other states, that otherwise could not be merged, into one superstate—but at the cost of more memory. Another option could be to merge more than two states in one go. These options remain to be investigated.

It is well-known that less heuristics can be used for *liveness* properties than for reachability properties. Investigating whether *some* merging can still be used for liveness synthesis (i.e. the synthesis of parameter valuations for which some location is infinitely often reachable) is an interesting future work.

Another, more theoretical question is to define and compute the “best possible merge”. Currently, the result of merging is not canonical, since it depends on the exploration order and the order of searching for siblings. We have not found a candidate definition that minimizes the state space and provides natural, canonical merge representatives.

Finally, investigating the recent PPLite [BZ18; BZ20] instead of PPL for polyhedra computation is on our agenda.

## Acknowledgements

We thank Benjamin Loillier for helping us testing our artifact. Experiments presented in this paper were carried out using the Grid’5000 testbed, supported by a scientific interest group hosted by Inria and including CNRS, RE-NATER and several universities as well as other organizations (see https://www.grid5000.fr).
A Results for all Heuristics on the Full Benchmark

<table><thead><tr><th>With Restarting</th><th>Nomerge</th><th>M2.12</th><th>RVMr</th><th>RVCr</th><th>RQMr</th><th>RQCr</th><th>RDMr</th><th>ROCr</th><th>OVMr</th><th>OVCr</th><th>QOMr</th><th>QDCr</th><th>QDMr</th><th>QDCr</th></tr></thead><tbody><tr><td rowspan="10">Time</td><td># wins</td><td>20</td><td>17</td><td>15</td><td>2</td><td>10</td><td>3</td><td>5</td><td>3</td><td>9</td><td>4</td><td>8</td><td>8</td><td>4</td><td>8</td></tr><tr><td>Avg (s)</td><td>10.0</td><td>5.47</td><td>4.56</td><td>46.7</td><td>3.84</td><td>43.53</td><td>4.69</td><td>49.05</td><td>5.58</td><td>5.7</td><td>3.79</td><td>3.81</td><td>5.54</td><td>5.63</td></tr><tr><td>Avg (merge) (s)</td><td>18.8</td><td>7.83</td><td>5.57</td><td>17.8</td><td>3.83</td><td>10.1</td><td>5.86</td><td>18.69</td><td>8.0</td><td>8.32</td><td>3.66</td><td>3.7</td><td>7.89</td><td>8.14</td></tr><tr><td>Avg (no merge) (s)</td><td>3.83</td><td>3.82</td><td>3.85</td><td>66.93</td><td>3.85</td><td>66.93</td><td>3.88</td><td>70.29</td><td>3.89</td><td>3.87</td><td>3.88</td><td>3.88</td><td>3.89</td><td>3.87</td></tr><tr><td>Median (s)</td><td>1.39</td><td>1.2</td><td>1.14</td><td>4.85</td><td>1.14</td><td>2.98</td><td>1.19</td><td>6.49</td><td>1.15</td><td>1.15</td><td>1.12</td><td>1.12</td><td>1.15</td><td>1.17</td></tr><tr><td>Nrm. avg</td><td>1.0</td><td>0.91</td><td>0.91</td><td>9.06</td><td><strong>0.87</strong></td><td>8.91</td><td>0.92</td><td>10.34</td><td>0.92</td><td>0.92</td><td>0.88</td><td><strong>0.87</strong></td><td>0.92</td><td>0.93</td></tr><tr><td>Nrm. avg (merge)</td><td>1.0</td><td>0.75</td><td>0.74</td><td>1.74</td><td>0.66</td><td>1.4</td><td>0.76</td><td>1.86</td><td>0.75</td><td>0.76</td><td>0.66</td><td><strong>0.65</strong></td><td>0.77</td><td>0.78</td></tr><tr><td>Nrm. avg (no-mrg)</td><td>1.0</td><td>1.02</td><td>1.03</td><td>14.27</td><td>1.02</td><td>14.25</td><td>1.03</td><td>16.38</td><td>1.03</td><td>1.03</td><td>1.04</td><td>1.03</td><td>1.03</td><td>1.04</td></tr><tr><td># wins</td><td>0</td><td>19</td><td>32</td><td>29</td><td>15</td><td>15</td><td>29</td><td>30</td><td>20</td><td>20</td><td>16</td><td>16</td><td>20</td><td>20</td></tr><tr><td>Avg (merge)</td><td>11445.61</td><td>11096.54</td><td>11064.37</td><td>11106.09</td><td>11120.34</td><td>11120.55</td><td>11066.85</td><td>11105.77</td><td>11089.5</td><td>11089.5</td><td>11118.73</td><td>11118.73</td><td>11087.77</td><td>11087.77</td></tr><tr><td>Median</td><td>1518.17</td><td>670.43</td><td>592.31</td><td>693.62</td><td>728.24</td><td>728.74</td><td>598.33</td><td>692.74</td><td>653.33</td><td>653.33</td><td>724.31</td><td>724.31</td><td>649.14</td><td>649.14</td></tr><tr><td>Nrm. avg</td><td>2389.5</td><td>703.5</td><td>604.5</td><td>607.0</td><td>905.0</td><td>905.0</td><td>604.5</td><td>607.0</td><td>701.0</td><td>701.0</td><td>905.0</td><td>905.0</td><td>701.0</td><td>701.0</td></tr><tr><td></td><td>1.0</td><td>0.86</td><td>0.84</td><td>0.85</td><td>0.88</td><td>0.88</td><td>0.84</td><td>0.85</td><td>0.86</td><td>0.86</td><td>0.88</td><td>0.88</td><td>0.85</td><td>0.85</td></tr><tr><td rowspan="10">No Restarting</td><td># wins</td><td>20</td><td>17</td><td>11</td><td>4</td><td>8</td><td>3</td><td>4</td><td>2</td><td>6</td><td>6</td><td>19</td><td>6</td><td>8</td><td>8</td></tr><tr><td>Avg (s)</td><td>10.0</td><td>5.47</td><td>4.56</td><td>46.48</td><td>3.85</td><td>43.31</td><td>4.65</td><td>48.92</td><td>5.09</td><td>5.19</td><td>3.77</td><td>3.78</td><td>5.16</td><td>5.25</td></tr><tr><td>Avg (merge) (s)</td><td>18.8</td><td>7.83</td><td>5.58</td><td>17.19</td><td>3.86</td><td>9.57</td><td>5.74</td><td>18.41</td><td>6.8</td><td>7.07</td><td>3.63</td><td>3.64</td><td>7.0</td><td>7.24</td></tr><tr><td>Avg (no merge) (s)</td><td>3.83</td><td>3.82</td><td>3.85</td><td>66.97</td><td>3.85</td><td>66.94</td><td>3.89</td><td>70.28</td><td>3.89</td><td>3.88</td><td>3.88</td><td>3.88</td><td>3.88</td><td>3.87</td></tr><tr><td>Median (s)</td><td>1.39</td><td>1.2</td><td>1.14</td><td>4.34</td><td>1.14</td><td>2.82</td><td>1.17</td><td>5.4</td><td>1.13</td><td>1.12</td><td>1.12</td><td>1.12</td><td>1.13</td><td>1.15</td></tr><tr><td>Nrm. avg</td><td>1.0</td><td>0.91</td><td>0.9</td><td>9.04</td><td>0.88</td><td>8.91</td><td>0.92</td><td>10.33</td><td>0.9</td><td>0.91</td><td><strong>0.87</strong></td><td><strong>0.87</strong></td><td>0.91</td><td>0.92</td></tr><tr><td>Nrm. avg (merge)</td><td>1.0</td><td>0.75</td><td>0.74</td><td>1.69</td><td>0.65</td><td>1.38</td><td>0.76</td><td>1.83</td><td>0.72</td><td>0.74</td><td><strong>0.64</strong></td><td>0.65</td><td>0.74</td><td>0.76</td></tr><tr><td>Nrm. avg (no-mrg)</td><td>1.0</td><td>1.02</td><td>1.02</td><td>14.28</td><td>1.04</td><td>14.27</td><td>1.03</td><td>16.38</td><td>1.03</td><td>1.03</td><td>1.03</td><td>1.03</td><td>1.03</td><td>1.04</td></tr><tr><td># wins</td><td>0</td><td>19</td><td>23</td><td>26</td><td>15</td><td>15</td><td>29</td><td>32</td><td>19</td><td>19</td><td>15</td><td>15</td><td>19</td><td>19</td></tr><tr><td>Avg (merge)</td><td>11445.61</td><td>11096.54</td><td>11073.57</td><td>11105.33</td><td>11123.2</td><td>11122.24</td><td>11068.6</td><td>11105.41</td><td>11096.89</td><td>11096.89</td><td>11120.79</td><td>11120.79</td><td>11090.01</td><td>11090.01</td></tr><tr><td>Median</td><td>1518.17</td><td>670.43</td><td>614.64</td><td>691.79</td><td>735.17</td><td>732.83</td><td>601.12</td><td>691.98</td><td>671.29</td><td>671.29</td><td>729.33</td><td>729.33</td><td>654.57</td><td>654.57</td></tr><tr><td>Nrm. avg</td><td>2389.5</td><td>703.5</td><td>636.5</td><td>583.0</td><td>905.0</td><td>905.0</td><td>604.5</td><td>577.0</td><td>706.5</td><td>706.5</td><td>905.0</td><td>905.0</td><td>701.0</td><td>701.0</td></tr><tr><td></td><td>1.0</td><td>0.86</td><td><strong>0.84</strong></td><td>0.85</td><td>0.88</td><td>0.88</td><td><strong>0.84</strong></td><td>0.85</td><td>0.86</td><td>0.86</td><td>0.88</td><td>0.88</td><td>0.86</td><td>0.86</td></tr></tbody></table>
References

[AD94] Rajeev Alur and David L. Dill. "A theory of timed automata". In: *Theoretical Computer Science* 126.2 (Apr. 1994), pp. 183-235. ISSN: 0304-3975.
DOI: 10.1016/0304-3975(94)90010-8 (cit. on pp. 1-3).

[AFS13] Étienne André, Laurent Fribourg, and Romain Soulat. "Merge and Conquer: State Merging in Parametric Timed Automata". In: *ATVA* (Oct. 15-18, 2013). Ed. by Dang-Van Hung and Mizuhito Ogawa. Vol. 8172. Lecture Notes in Computer Science. Ha Noi, Viet Nam: Springer, Oct. 2013, pp. 381-396. DOI: 10.1007/978-3-319-02444-8_27 (cit. on pp. 2, 5, 10, 11, 14).

[AHV93] Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. "Parametric real-time reasoning". In: *STOC* (May 16-18, 1993). Ed. by S. Rao Kosaraju, David S. Johnson, and Alok Aggarwal. San Diego, California, United States: ACM, 1993, pp. 592-601. DOI: 10.1145/167088.167242 (cit. on pp. 1, 3).

[ALM20] Étienne André, Didier Lime, and Nicolas Markey. "Language Preservation Problems in Parametric Timed Automata". In: *Logical Methods in Computer Science* 16.1 (Jan. 2020). DOI: 10.23638/LMCS-16(1:5)2020 (cit. on p. 2).

[ALR15] Étienne André, Didier Lime, and Olivier H. Roux. "Integer-Complete Synthesis for Bounded Parametric Timed Automata". In: *RP* (Sept. 21-23, 2015). Ed. by Mikołaj Bojańczyk, Slawomir Lasota, and Igor Potapov. Vol. 9328. Lecture Notes in Computer Science. Warsaw, Poland: Springer, Sept. 2015, pp. 7-19. DOI: 10.1007/978-3-319-24537-9_2 (cit. on p. 2).

[AMP21] Étienne André, Dylan Marinho, and Jaco van de Pol. "A Benchmarks Library for Extended Timed Automata". In: *TAP* (June 21-25, 2021). Ed. by Frédéric Louergue and Franz Wotawa. Vol. 12740. Lecture Notes in Computer Science. virtual: Springer, 2021, pp. 39-50. DOI: 10.1007/978-3-030-79379-1_3 (cit. on pp. 2, 12).

[And+09] Étienne André, Thomas Chatain, Emmanuelle Encrenaz, and Laurent Fribourg. "An Inverse Method for Parametric Timed Automata". In: *International Journal of Foundations of Computer Science* 20.5 (Oct. 2009), pp. 819-836. DOI: 10.1142/S0129054109006905 (cit. on p. 4).

[And+21] Étienne André, Jaime Arias, Laure Petrucci, and Jaco van de Pol. "Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata". In: *TACAS* (Mar. 27-Apr. 1, 2021). Ed. by Jan Friso Groote and Kim G. Larsen. Vol. 12651. Lecture Notes in Computer Science. Virtual: Springer, 2021, pp. 311-329. DOI: 10.1007/978-3-030-72016-2_17 (cit. on p. 2).

[And19] Étienne André. "What's decidable about parametric timed automata?" In: *International Journal on Software Tools for Technology Transfer* 21.2 (Apr. 2019), pp. 203-219. DOI: 10.1007/s10009-017-0467-0 (cit. on p. 1).

[And21] Étienne André. "IMITATOR 3: Synthesis of timing parameters beyond decidability". In: *CAV* (July 18-23, 2021). Ed. by Rustan Leino and Alexandra Silva. Vol. 12759. Lecture Notes in Computer Science. virtual: Springer, 2021, pp. 1-14. DOI: 10.1007/978-3-030-81685-8_26 (cit. on pp. 2, 11).
[ANP17] Étienne André, Hoang Gia Nguyen, and Laure Petrucci. "Efficient parameter synthesis using optimized state exploration strategies". In: *ICECCS* (Nov. 6–8, 2017). Ed. by Zhenjiang Hu and Guangdong Bai. Fukuoka, Japan: IEEE, 2017, pp. 1–10. DOI: 10.1109/ICECCS.2017.28 (cit. on p. 2).

[BBM06] Ramzi Ben Salah, Marius Bozga, and Oded Maler. "On Interleaving in Timed Automata". In: *CONCUR* (Aug. 27–30, 2006). Ed. by Christel Baier and Holger Hermanns. Vol. 4137. Lecture Notes in Computer Science. Bonn, Germany: Springer, 2006, pp. 465–476. ISBN: 3-540-37376-4. DOI: 10.1007/11817949_31 (cit. on p. 2).

[Beh+06] Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, and Radek Pelánek. "Lower and upper bounds in zone-based abstractions of timed automata". In: *International Journal on Software Tools for Technology Transfer* 8.3 (2006), pp. 204–215. DOI: 10.1007/s10009-005-0190-0 (cit. on p. 2).

[Bez+16] Peter Bezděk, Nikola Beneš, Jiří Barnat, and Ivana Černá. "LTL Parameter Synthesis of Parametric Timed Automata". In: *SEFM* (July 4–8, 2016). Ed. by Rocco De Nicola and Eva Kühn. Vol. 9763. Lecture Notes in Computer Science. Vienna, Austria: Springer, 2016, pp. 172–187. DOI: 10.1007/978-3-319-41591-8_12 (cit. on p. 2).

[BK08] Christel Baier and Joost-Pieter Katoen. *Principles of Model Checking*. MIT Press, 2008. ISBN: 978-0-262-02649-9 (cit. on p. 10).

[BMZ08] Roberto Bagnara, Hill Patricia M., and Enea Zaffanella. "The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems". In: *Science of Computer Programming* 72.1–2 (2008), pp. 3–21. DOI: 10.1016/j.scico.2007.08.001 (cit. on p. 11).

[Bog+20] Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. "Reachability Analysis of Linear Hybrid Systems via Block Decomposition". In: *IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems* 39.11 (2020), pp. 4018–4029. DOI: 10.1109/TCAD.2020.3012859 (cit. on p. 2).

[BZ18] Anna Becchi and Enea Zaffanella. "An Efficient Abstract Domain for Not Necessarily Closed Polyhedra". In: *SAS* (Aug. 29–31, 2018). Ed. by Andreas Podelski. Vol. 11002. Lecture Notes in Computer Science. Freiburg, Germany: Springer, 2018, pp. 146–165. DOI: 10.1007/978-3-319-99725-4_11 (cit. on p. 15).

[BZ20] Anna Becchi and Enea Zaffanella. "PPLite: Zero-overhead encoding of NNC polyhedra". In: *Information and Computation* 275 (2020), pp. 1–36. DOI: 10.1016/j.ic.2020.104620 (cit. on p. 15).

[CÁF11] Xin Chen, Erika Ábrahám, and Goran Frehse. "Efficient Bounded Reachability Computation for Rectangular Automata". In: *RP* (Sept. 28–30, 2011). Ed. by Giorgio Delzanno and Igor Potapov. Vol. 6945. Lecture Notes in Computer Science. Genoa, Italy: Springer, 2011, pp. 139–152. DOI: 10.1007/978-3-642-24288-5_13 (cit. on p. 2).

[CSÁ14] Xin Chen, Sriram Sankaranarayanan, and Erika Ábrahám. "Underapproximate flowpipes for non-linear continuous systems". In: *FMCAD* (Oct. 21–24, 2014). Lausanne, Switzerland: IEEE, 2014, pp. 59–66. DOI: 10.1109/FMCAD.2014.6987596 (cit. on p. 2).
[Dav05] Alexandre David. "Merging DBMs Efficiently". In: *NWPT* (Oct. 19-21, 2005). DIKU, University of Copenhagen, 2005, pp. 54-56 (cit. on p. 2).

[Hen96] Thomas A. Henzinger. "The Theory of Hybrid Automata". In: *LiCS*. Ed. by Moshe Y. Vardi and Edmund M. Clarke. New Brunswick, New Jersey, USA: IEEE Computer Society, 1996, pp. 278-292. DOI: 10.1109/LICS.1996.561342 (cit. on p. 2).

[Her+20] Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, and Igor Walukiewicz. "Why Liveness for Timed Automata Is Hard, and What We Can Do About It". In: *ACM Transactions on Computational Logic* 21.3 (2020), 17:1-17:28. DOI: 10.1145/3372310 (cit. on p. 2).

[HMP91] Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. "Temporal Proof Methodologies for Real-time Systems". In: *POPL* (Jan. 21-23, 1991). Ed. by David S. Wise. Orlando, Florida, USA: ACM Press, 1991, pp. 353-366. DOI: 10.1145/99583.99629 (cit. on p. 3).

[HSW12] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. "Efficient emptiness check for timed Büchi automata". In: *Formal Methods in System Design* 40.2 (2012), pp. 122-146. DOI: 10.1007/s10703-011-0133-1 (cit. on p. 2).

[HSW13] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. "Lazy Abstractions for Timed Automata". In: *CAV* (July 13-19, 2013). Ed. by Natasha Sharygina and Helmut Veith. Vol. 8044. Lecture Notes in Computer Science. Saint Petersburg, Russia: Springer, 2013, pp. 990-1005. DOI: 10.1007/978-3-642-39799-8_71 (cit. on p. 2).

[HSW16] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. "Better abstractions for timed automata". In: *Information and Computation* 251 (2016), pp. 67-90. DOI: 10.1016/j.ic.2016.07.004 (cit. on p. 2).

[HT15] Frédéric Herbreteau and Thanh-Tung Tran. "Improving Search Order for Reachability Testing in Timed Automata". In: *FORMATS* (Sept. 2-4, 2015). Ed. by Sriram Sankaranarayanan and Enrico Vicario. Vol. 9268. Lecture Notes in Computer Science. Madrid, Spain: Springer, 2015, pp. 124-139. DOI: 10.1007/978-3-319-22975-1_9 (cit. on p. 2).

[Hun+02] Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager. "Linear parametric model checking of timed automata". In: *Journal of Logic and Algebraic Programming* 52-53 (2002), pp. 183-220. DOI: 10.1016/S1567-8326(02)00037-1 (cit. on pp. 2, 4).

[JLR15] Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. "Integer Parameter Synthesis for Real-Time Systems". In: *IEEE Transactions on Software Engineering* 41.5 (2015), pp. 445-461. DOI: 10.1109/TSE.2014.2357445 (cit. on pp. 4, 6).

[Laa+13] Alfons Laarman, Mads Chr. Olesen, Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen, and Jaco van De Pol. "Multi-Core Emptiness Checking of Timed Büchi Automata using Inclusion Abstraction". In: *CAV* (July 13-19, 2013). Ed. by Natasha Sharygina and Helmut Veith. Vol. 8044. Lecture Notes in Computer Science. Saint Petersburg, Russia: Springer, July 2013, pp. 968-983. DOI: 10.1007/978-3-642-39799-8_69 (cit. on pp. 2, 11).

[NPV18] Hoang Gia Nguyen, Laure Petrucci, and Jaco Van de Pol. "Layered and Collecting NDFS with Subsumption for Parametric Timed Automata". In: *ICECCS* (Dec. 12-14, 2018). Ed. by Anthony Widjaja Lin and Jun
Sun. Melbourne, Australia: IEEE Computer Society, Dec. 2018, pp. 1–9.
DOI: 10.1109/ICECCS2018.2018.00009 (cit. on p. 10).

[SNÁ17] Stefan Schupp, Johanna Nellen, and Erika Ábrahám. "Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis". In: *QAPL@ETAPS*. Ed. by Herbert Wiklicky and Erik P. de Vink. Vol. 250. Electronic Proceedings in Theoretical Computer Science. Uppsala, Sweden, 2017, pp. 1–14. DOI: 10.4204/EPTCS.250.1 (cit. on p. 2).