2-EXPTIME 3-EXPTIME EXPTIME exp Reach Obese Meager Normal 11institutetext:
Université Paris Cité, CNRS, IRIF, Paris, France 22institutetext: LACL,
Université Paris-Est Créteil, France

# Computing the Bandwidth of
Meager Timed Automata††thanks: This work was supported by the ANR project
MAVeriQ ANR-CE25-0012 and by the ANR-JST project CyPhAI.

(long version)

Eugene Asarin 11 0000-0001-7983-2202 Aldric Degorre 11 0000-0003-2712-4954
Cătălin Dima 22 0000-0001-5981-4533
Bernardo Jacobo Inclán 11 0009-0009-5323-7945

###### Abstract

The bandwidth of timed automata characterizes the quantity of information
produced/transmitted per time unit. We previously delimited 3 classes of TA
according to the nature of their asymptotic bandwidth: meager, normal, and
obese. In this paper, we propose a method, based on a finite-state simply-
timed abstraction, to compute the actual value of the bandwidth of meager
automata. The states of this abstraction correspond to barycenters of the
faces of the simplices in the region automaton. Then the bandwidth is $\log
1/|z_{0}|$ where $z_{0}$ is the smallest root (in modulus) of the
characteristic polynomial of this finite-state abstraction.

###### Keywords:

Timed automata Information Bandwidth Entropy

##  1 Introduction

We study timed automata [1] from the information-theoretic standpoint. An
important characteristic of a timed automaton is its bandwidth [14], a notion
generalizing the growth rate of formal languages [9, 8, 12, 13]. In the case
of timed automata, bandwidth describes the quantity of information that it can
produce/transmit per time unit; however, differently from the case of discrete
formal languages, information that timed automata may produce must be related
to a degree of precision of an observer of the timed words generated by the
timed automaton.

In the preceding work [5] we made a first step in this direction by
identifying three classes of TA according to the nature of their asymptotic
bandwidth: meager, normal, and obese. This analysis relies on a refinement of
orbit graphs [19, 3] associated with cycles in the timed automata, which
themselves refine the region construction for timed automata. The three types
of timed languages behave very differently. First, meager automata are almost
discrete automata, or automata in which real-time delays are very constrained,
leading to quasi-Zeno behaviors (some quantities decrease while remaining
positive, as the distance between Achilles and the Tortoise, see [2, VI:9] or
the more recent paper [6]). Their bandwidth is bounded by a constant, as is
the case for languages of finite automata, hence being independent of the
precision of an observer. Second, in normal timed languages, information can
be encoded every few time units and their bandwidth is
$O(\log(1/\varepsilon))$, where $\varepsilon$ is the degree of precision by
which an observer may distinguish timed words generated by the automaton.
Thirdly, obese timed languages allow encoding information with a very high
frequency, leading to $O(1/\varepsilon)$ bandwidth.

In this paper, we make the first step towards computing the bandwidth of a
timed automaton, by attacking the case of meager automata. Our solution is
based on another finite-state abstraction of orbit graphs and region automata,
in which each state is associated with a barycenter of one of the faces of the
regions. The bandwidth can then be computed as $\log 1/|z_{0}|$ where $z_{0}$
is the root of the smallest modulus of the characteristic polynomial of the
adjacency $\lambda$-matrix [16] associated with the finite-state abstraction.
The correctness of our construction heavily depends on investigations in [5,
full version], which rely on Simon’s factorization theorem [20] and Puri’s
reachability theory [19].

The paper is structured as follows: in Sect. 2 we recall the main notions and
results concerning the bandwidth of timed automata; in Sect. 3 we show how to
compute the bandwidth for the restricted class of simply-timed graphs; in
Sect. 4 we present our main contribution: a method for computing the bandwidth
of meager timed automata (by reduction to simply-timed ones). Most of the
proofs can be found in the Appendix.

##  2 Preliminaries

###  2.1 Timed words, languages and automata

Timed automata have been introduced in [1] for modeling and verification of
real-time systems. We will use the main definitions in the following form:

###### Definition 1

Given $\Sigma$, a finite alphabet of discrete events, a _timed word_ over
$\Sigma$ is an element from $\left(\Sigma\times_{+}\right)^{*}$ of the form
$w=(a_{1},t_{1})\dots(a_{n},t_{n})$, with $0\leq t_{1}\leq t_{2}\cdots\leq
t_{n}$. We denote $\mathop{\mathrm{dur}}(w)=t_{n}$. A _timed language_ over
$\Sigma$ is a set of timed words over the same alphabet.

For a set of variables $\Xi$, let $G_{\Xi}$ be the set of finite conjunctions
of constraints of the form $\xi\sim b$ with $\xi\in\Xi$,
$\sim\in\\{<,\leq,>,\geq\\}$ and $b\in\mathds{N}$.

###### Definition 2

A _timed automaton_ is a tuple $(Q,X,\Sigma,\Delta,S,I,F)$, where

  * •

$Q$ is the finite set of discrete locations;

  * •

$X$ is the finite set of clocks;

  * •

$\Sigma$ is a finite alphabet;

  * •

$S,I,F:Q\rightarrow G_{X}$ define respectively the starting, initial, and
final clock values for each location;

  * •

$\Delta\subseteq Q\times Q\times\Sigma\times G_{X}\times 2^{X}$ is the
transition relation, whose elements are called edges.

A timed automaton is _deterministic_ (referred to as DTA) if
$\\{(q,x)|x\models I(q)\\}$ is a singleton and for any two edges
$(q,q_{1},a,\mathfrak{g}_{1},\mathfrak{r}_{1})$ and
$(q,q_{2},a,\mathfrak{g}_{2},\mathfrak{r}_{2})$ with $q_{1}\neq q_{2}$, the
constraint $\mathfrak{g}_{1}\wedge\mathfrak{g}_{2}$ is non-satisfiable.

A small particularity of our definition is the starting clock constraint
$S(q)$ defining with which clock values the run can enter each state $q$.

$\mathcal{A}_{1}:$$q$$a,2<x<3,\\{x\\}$$\mathcal{A}_{2}:$$q$$a,b,\,x<1$$c,5<x<6,\\{x\\}$$\mathcal{A}_{3}:$$q$$a,b,\,x<5$$\mathcal{A}_{4}:$$q$$p$$a,b,\,3<x<4$$\delta_{2}:b,5<y<6,\\{x,y\\}$$\mathcal{A}_{5}:$$q$$p$$a,b,\,x=3$$b,\,y=5,\\{x,y\\}$$\mathcal{A}_{6}:$$q$$p$$a,b,x<1,\\{x\\}$$a,b,1<y<2,\\{y\\}$$\mathcal{A}_{7}:$$q$$p$$a,x<1,\\{x\\}$$b,y<1,\\{y\\}$
Figure 1: 7 running examples of timed automata, $I(q)=\\{\mathbf{0}\\}$,
$F(\cdot)=\mathbf{true}$ for marked locations. An arrow labeled with $a,b$ is
a shorthand for two transitions with the same guards and resets.

The semantics of a timed automaton is given by a _timed transition system_
whose states are tuples $(q,x)$ composed of a location $q\in Q$ and a clock
valuation (vector) $x\in[0,\infty)^{X}$. Each edge
$\delta=(q,q^{\prime},a,\mathfrak{g},\mathfrak{r})\in\Delta$ generates many
timed transitions, which are tuples
$(q,x)\xrightarrow{\delta,d}(q^{\prime},x^{\prime})$ where $x\models S(q)$,
$x+d\models\mathfrak{g}$ and $x^{\prime}_{c}=0$ whenever $c\in\mathfrak{r}$
and $x^{\prime}_{c}=x_{c}+d$ otherwise, provided that $x^{\prime}\models
S(q^{\prime})$. We also denote $x[\mathfrak{r}]$ the operation of resetting
the clocks in $\mathfrak{r}$, hence $x^{\prime}=(x+d)[\mathfrak{r}]$.

_Paths_ are sequences of edges that agree on intermediary locations. At the
semantic level, they generate _runs_ of the form

$\rho=(q_{0},x_{0})\xrightarrow{(\delta_{1},d_{1})}(q_{1},x_{1})\dots\xrightarrow{(\delta_{n},d_{n})}(q_{n},x_{n}),$

which are sequences of timed transitions that agree on intermediary
configurations. An _accepting run_ is a run in which the first state satisifes
$x_{0}\models I(q_{0})$ and the last one $x_{n}\models F(q_{n})$.

Given a run $\rho$ as above, the path associated with $\rho$ is defined as
$\mathop{path}(\rho)\triangleq\delta_{1}\dots\delta_{n}$. Furthermore, if
$\delta_{i}=(q_{i},q_{i+1},a_{i},\mathfrak{g}_{i},\mathfrak{r}_{i})$, then the
timed word associated with $\rho$ is defined as
$\mathop{word}(\rho)\triangleq(a_{1},d_{1})(a_{2},d_{1}+d_{2})\ldots(a_{n},\sum_{i\leq
n}d_{i})$. The _duration_ of $\rho$ is
$\mathop{\mathrm{dur}}(\rho)=\mathop{\mathrm{dur}}(\mathop{word}(\rho))$. The
language of a timed automaton is the set of timed words associated with some
accepting run and is denoted $L(\mathcal{A})$. We will also need _time-
restricted languages_ : for any timed language $L$ and nonnegative real
$T\in[0,\infty)$, $L_{T}=\\{w\in L\mid\mathop{\mathrm{dur}}(w)\leq T\\}$.

For a small example consider a 3-edge path $q\to p\to q$ in the timed
automaton $\mathcal{A}_{6}$ in Fig. 1. One of its runs is

$(q,0,0)\xrightarrow{(a,0.8)}(p,0,0.8)\xrightarrow{(b,0.7)}(q,0.7,0)\xrightarrow{(b,0.2)}(p,0,0.2)$

and the corresponding timed word is $(a,0.8)(b,1.5)(b,1.7)$.

#### Region-split form.

Many algorithms related to timed automata utilize the finitary abstraction of
the timed transition system called the _region construction_ [1] that we
briefly recall here. Let us denote by $M$ the maximal constant appearing in
the constraints used in the automaton. Also, for $\xi\in$, we denote
$\lfloor\xi\rfloor$ its integral part, $\\{\xi\\}$ its fractional part and,
for a clock vector $x\in[0,\infty)^{X}$, $x_{\text{int}}\triangleq\\{c\in
X|x_{c}\in[0,M]\cap\mathds{N}\\}$, and $x_{\text{frac}}\triangleq\\{c\in
X|x_{c}\in[0,M]\setminus\mathds{N}\\}$. Then regions are defined as
equivalence classes of the region equivalence described hereafter. Two clock
vectors $x$ and $y$ are region-equivalent iff :

  * •

$x_{\text{int}}=y_{\text{int}}$ and $x_{\text{frac}}=y_{\text{frac}}$;

  * •

and for any clock $c\in x_{\text{int}}\cup x_{\text{frac}},\lfloor
x_{c}\rfloor=\lfloor y_{c}\rfloor$;

  * •

and for any two clocks $c_{1},c_{2}\in x_{\text{int}}\cup x_{\text{frac}}$,
$\\{x_{c_{1}}\\}\leq\\{x_{c_{2}}\\}$ iff $\\{y_{c_{1}}\\}\leq\\{y_{c_{2}}\\}$.

Note that a region $R$ is a simplex of some dimension $d\leq\\#X$.

As in [3, 5] we utilize here timed automata in which the guards defining
starting clock values for each location actually define regions:

###### Definition 3

A _region-split TA_ (or RsTA for short) is a deterministic timed automaton
$(Q,X,\Sigma,\Delta,S,I,F)$, such that, for any location $q\in Q$:

  * •

$S(q)$ defines a non-empty bounded region, called the _starting region_ of
$q$;

  * •

all states in $\\{q\\}\times S(q)$ are reachable from the initial state and
co-reachable to a final state;

  * •

either $I(q)=S(q)$ is a singleton111by definition of DTA this is possible for
a unique location $q$ or $I(q)=\emptyset$;

  * •

for any edge $(q,q^{\prime},a,\mathfrak{g},\mathfrak{r})\in\Delta$,
$\left(\\{S(q)+d\mid
d\in_{+}\\}\cap\mathfrak{g}\right)[\mathfrak{r}]=S(q^{\prime})$, where we
utilized the $(\cdot)[\mathfrak{r}]$ operator lifted to sets of clock
valuations.

A folklore result says that any DTA can be brought into a region-split form
which may contain an exponentially larger set of locations. Note that this
construction is similar to that of the region automaton introduced in [1],
except that the outcome is slightly coarser and is typed as a timed automaton.
As an example, we present on Fig. 4 the region-split form
$\mathcal{A}_{6}^{\prime}$ of the automaton $\mathcal{A}_{6}$ (from Fig. 1)
with explicit starting regions $S(\cdot)$ for each state. In particular, state
$q$ of $\mathcal{A}_{6}$ is split into two states: the initial $s$ and $q$
corresponding to zero and non-zero clock vectors, respectively.

We also introduce the notation $\bar{\mathcal{A}}$ for the closed version of
any RsTA $\mathcal{A}$: i.e. the same automaton where all strict inequalities
are changed to non-strict ones. Thanks to region-splitting, the closure
retains the same set of symbolic behaviors as the original RsTA, this allows
us to safely reason on runs that visit vertices and faces of regions.

###  2.2 Pseudo-distance on timed words

We are using the proximity measure on timed words introduced in [4].

###### Definition 4

The _pseudo-distance_ $d$ between timed words

$w=(a_{1},t_{1})\dots(a_{n},t_{n})\text{ and
}v=(b_{1},s_{1})\dots(b_{m},s_{m})$

is defined as follows (with the convention $\min\emptyset=\infty$):

$\overrightarrow{d}(w,v)\triangleq\max_{i\in\\{1..n\\}}\min_{j\in\\{1..m\\}}\\{|t_{i}-s_{j}|:a_{i}=b_{j}\\};\hfill
d(w,v)\triangleq\max(\overrightarrow{d}(w,v),\overrightarrow{d}(v,w)).$

This pseudo-distance allows a meaningful comparison of timed words with a
different number of events. It is illustrated on Fig. 2. Intuitively, two
words are close to each other when they cannot be distinguished by an observer
that reads the discrete letters of the word exactly (they can determine
whether or not a letter has occurred) but with some imprecision w.r.t. time.
So the observer cannot determine when two letters are very close to one
another, which one came before the other, and not even how many times a letter
was repeated within a short interval.

$\bullet$$\circ$$\bullet$$\circ$$\bullet$$u=(a,.7),(b,1.8),(a,3),(b,4),(a,4.1)$$\bullet$$\bullet$$\circ$$\bullet$$\bullet$$\circ$$v=(a,.6),(a,1),(b,1.7),(a,3),(a,4.1),(b,4.2)$
Figure 2: Pseudo-distance between two timed words (dotted lines with arrows
represent directed matches between letters). $\overrightarrow{d}(u,v)=0.2;\
\overrightarrow{d}(v,u)=0.3$, thus $d(u,v)=0.3$.

It is possible that $d$ fails to distinguish timed words, that is
$d(w_{1},w_{2})=0$ but $w_{1}\neq w_{2}$; this could happen when $w_{1}$ and
$w_{2}$ only differ by order and quantity of simultaneous letters, e.g. for
$w=(a,1)(b,1)$ and $v=(b,1)(b,1)(a,1)$, that is why $d$ is only a pseudo-
distance.

We will sometimes use the following trick to “transform” $d$ into a distance.
We call a timed word $w=(a_{1},t_{1})\dots(a_{n},t_{n})$ _0-free_ whenever
$0<t_{1}<t_{2}<\cdots<t_{n}$. Note that $d$ satisfies the axiom
$w_{1}=w_{2}\Leftrightarrow d(w_{1},w_{2})=0$ whenever $w_{1},w_{2}$ are
0-free, hence $d$ becomes a distance on 0-free words.

######  Definition 5 (0-elimination, words)

Given a timed word $w$ over an alphabet $\Sigma$, we define its _$0$
-elimination_ as the 0-free timed word $W=\mathop{\nu}(w)$ over the alphabet
$2^{\Sigma}\setminus\\{\emptyset\\}$ as follows:

  * •

let $0<t_{1}<t_{2}<\cdots<t_{n}$ be all the distinct non-zero event times in
$w$;

  * •

let $A_{i}\in 2^{\Sigma}$ be the set of all the events in $w$ occurring at
time $t_{i}$;

  * •

finally let $W=(A_{1},t_{1}),(A_{2},t_{2}),\dots,(A_{n},t_{n})$.

For example
$\mathop{\nu}((c,0)(a,5)(b,5)(a,5)(c,7))=(\\{a,b\\},5)(\\{c\\},7)$, the events
at time $0$ are ignored. We summarize the properties of the operation
$\mathop{\nu}$:

###### Proposition 1

Operation $\mathop{\nu}$ maps timed words on $\Sigma$ to $0$-free ones on
$2^{\Sigma}\setminus\\{\emptyset\\}$.
$\mathop{\nu}(w_{1})=\mathop{\nu}(w_{2})$ if and only if the words
$w_{i},i=1,2$ admit decompositions $w_{i}=u_{i}v_{i}$ with
$\mathop{\mathrm{dur}}(u_{i})=0$ and $d(v_{1},v_{2})=0$.

In words, 0-eliminations of two timed words coincide if and only if the words
are at distance $0$ except for the initial time instant $0$.

###  2.3 Bandwidth of timed languages

The definition of bandwidth is based on Kolmogorov&Tikhomirov’s work [15]
formalizing the quantity of information in an element of a compact metric
space observed with a given precision. We recall the adaptation of their
definitions from [4] to the context of timed languages.

###### Definition 6

Let $L$ be a timed language, then:

  * •

${\mathcal{M}}\subseteq L$ is an $\varepsilon$_-separated subset_ of $L$ if
$\forall x\neq y\in{\mathcal{M}},d(x,y)>\varepsilon$;

  * •

${\mathcal{N}}$ is an $\varepsilon$_-net_ of $L$ if $\forall y\in L,\exists
s\in{\mathcal{N}}\text{ s.t. }d(y,s)\leq\varepsilon$;

  * •

$\varepsilon$_-capacity_ of $L$ is defined222all logarithms in this article
are base 2 as

$\mathcal{C}_{\varepsilon}(L)\triangleq\log\max\\{\\#\\!\mathcal{M}\mid{\mathcal{M}}\text{
$\varepsilon$-separated set of }L\\};$

  * •

$\varepsilon$_-entropy_ of $L$ is defined as

$\mathcal{H}_{\varepsilon}(L)\triangleq\log\min\\{\\#\\!\mathcal{N}\mid{\mathcal{N}}\text{
$\varepsilon$-net of $L$}\\}.$

As shown in [4], every time-bounded timed language is compact with respect to
our distance $d$ and thus has finite $\varepsilon$-capacity and
$\varepsilon$-entropy. [14] introduced the notion of bandwidth of a timed
language as the entropy or capacity per time unit and related this notion to
bounded delay codes.

######  Definition 7 (bandwidth, [14])

The $\varepsilon$_-entropic_ and $\varepsilon$_-capacitive bandwidths_ of a
timed language $L$ are

$\mathcal{BH}_{\varepsilon}(L)\triangleq\limsup_{T\rightarrow\infty}\frac{\mathcal{H}_{\varepsilon}(L_{T})}{T};\qquad\mathcal{BC}_{\varepsilon}(L)\triangleq\limsup_{T\rightarrow\infty}\frac{\mathcal{C}_{\varepsilon}(L_{T})}{T}.$

$\bullet$$\circ$$\bullet$$\circ$$\bullet$$\circ$$\bullet$$\circ$$\bullet$$\circ$$\bullet$$\circ$$\bullet$
Figure 3: A run of $\mathcal{A}_{6}$ on
$(a,.9)(b,1.2)(a,1.8)(b,2.4)(a,2.7)(b,3.5)(a,3.6)(b,4.52)\\\
(a,4.59)(b,5.53)(a,5.58)(b,6.535)(a,6.575)$.
$\mathcal{A}_{6}^{\prime}:$$\displaystyle\frac{s}{x=y=0}$$\displaystyle\frac{q}{0=y<x<1}$$\displaystyle\frac{p}{0=x<y<1}$$a,b,x<1,\\{x\\}$$a,b,x<1,\\{x\\}$$a,b,1<y<2,\\{y\\}$
Figure 4: The region-split form of $\mathcal{A}_{6}$, constraints within
states correspond to start conditions $S(\cdot)$.

######  Definition 8 (3 classes, [5])

A timed language $L$ is

  * •

_meager_ whenever $\mathcal{BH}_{\varepsilon}(L)=O(1)$;

  * •

_normal_ whenever
$\mathcal{BH}_{\varepsilon}(L)=\Theta(\log\frac{1}{\varepsilon})$;

  * •

_obese_ whenever
$\mathcal{BH}_{\varepsilon}(L)=\Theta(\frac{1}{\varepsilon})$, as
$\varepsilon\to 0$.

As the main result of [5] we proved that every timed regular language belongs
to one of these classes, and provided a classification algorithm for timed
automata.

Fig. 1 gives a few examples of automata in the three classes:
$\mathcal{A}_{3}$, $\mathcal{A}_{5}$ and $\mathcal{A}_{6}$ are meager,
$\mathcal{A}_{1}$ and $\mathcal{A}_{4}$ are normal and $\mathcal{A}_{2}$ and
$\mathcal{A}_{7}$ are obese. From now on, we concentrate on meager timed
automata and compute their bandwidth. $\mathcal{A}_{5}$ has only discrete
choices since its transitions happen at discrete dates only. $\mathcal{A}_{3}$
can produce a huge amount of information ($2/\varepsilon$ bits every second),
but only during the first five seconds of its life. Its bandwidth is
$\lim_{T\to\infty}2/\varepsilon T=0$. The automaton $\mathcal{A}_{6}$ (serving
as running example below) is much less evident. It involves two flows of
events, with events of the former being $<1$ second apart and of the latter on
the contrary $>1$ second apart, as shown on Fig. 3. Such interleaving is
possible for any duration $T$, but real-valued delays between symbols become
more and more constrained.

##  3 Simply-timed graphs and their bandwidth

Following [10, 18], we define a class of graphs that will serve as the main
abstraction for computing the bandwidth of meager timed automata.

######  Definition 9 (Simply-timed graphs)

A _simply-timed graph_ (STG) is a tuple $\mathcal{G}=(Q,\Sigma,\Delta)$ with
$Q$ a finite set of states, $\Sigma$ a finite alphabet, and $\Delta\subset
Q\times\mathds{Q}_{+}\times\Sigma\times Q$ a finite transition relation. For a
transition $(p,d,a,q)\in\Delta$, the state $p$ is referred to as origin, $q$
destination, $a$ label and $d$ delay.

An STG is _$0$ -free_ if all its delays are strictly positive. It is
_deterministic_ if for any two transitions $(p,d,a,q)$ and
$(p,d,a,q^{\prime})$ necessarily $q=q^{\prime}$.

The timed language of such a graph is defined in a natural way.

######  Definition 10 (Semantics of STG)

A _run_ of an STG $(Q,\Sigma,\Delta)$ on a timed word
$w=(a_{1},t_{1})\dots(a_{n},t_{n})$ is a sequence
$q^{0}\xrightarrow{d_{0},a_{1}}q^{1}\xrightarrow{d_{1},a_{2}}\cdots q^{n},$
such that $t_{i}-t_{i-1}=d_{i}$, and $(q^{i-1},d_{i},a_{i},q^{i})\in\Delta$.
The _language_ $L(\mathcal{G})$ of an STG $\mathcal{G}$ is the set of all
timed words having a run.

$q$$p$$3\,a$$0\,b$$5\,b,5\,c$$2\,c$$q$$p$$3\,a$$2\,\\{b,c\\}$$5\,b,5\,c,3\,\\{a,b\\}$$2\,c$

$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$x$$y$$1$$2$$1$$2$

Figure 5:  A simply-timed graph (left), and its 0-free form (middle). Right: a
2-dimensional region, its 7 faces, and their barycenters.

The notions of $\varepsilon$-bandwidth are simpler for STG.

###### Definition 11

For a set $S$ of timed words, we call its _size_ and denote by $\Upsilon(S)$
the cardinality of the largest $0$-separated set in $S$.

Equivalently, this is the cardinality of the smallest 0-net, and the number of
equivalence classes for the binary relation $d(u,v)=0$ over $S$. We remark
that whenever $S$ is 0-free, $\Upsilon(S)=\\#S$.

###### Definition 12

The _growth rate_ of an STG $\mathcal{G}$ is defined as

$\beta(\mathcal{G})=\lim_{T\to\infty}\frac{\log\Upsilon(L_{T}(\mathcal{G}))}{T},$

whenever this limit exists and is finite.

###### Proposition 2

Given an STG $\mathcal{G}$ with non-empty language, the growth rate
$\beta(\mathcal{G})$ always exists. Moreover, taking $N$ the common
denominator of all delays, for $\varepsilon<1/2N$ the growth rate coincides
with both bandwidths:

$\mathcal{BC}_{\varepsilon}(L(\mathcal{G}))=\mathcal{BH}_{\varepsilon}(L(\mathcal{G}))=\beta(\mathcal{G}).$

We present the method for computing $\beta(\mathcal{G})$, which consists of
several transformations. First, we relate the notions of size and growth rate
to 0-elimination.

###### Proposition 3

0-elimination preserves the growth rate: $\beta(L)=\beta(\mathop{\nu}(L))$.

Thanks to this proposition, instead of counting equivalence classes in $L_{T}$
we will count timed words in $\mathop{\nu}(L)_{T}$. To that aim, we will
transform the STG for $L$ to that for $\mathop{\nu}(L)$.

######  Construction 1 (0-elimination in STG)

Given an STG $\mathcal{G}=(Q,\Sigma,\Delta)$, we define
$\mathop{\nu}(\mathcal{G})=(Q,2^{\Sigma}\setminus\\{\emptyset\\},\Delta^{\prime})$
combining every timed transition with each subsequent instant transition:
$(p,d,A,q)\in\Delta^{\prime}$ whenever $d>0$ and there exist
$(p,d,a_{0},q_{0}),(q_{0},0,a_{1},q_{1}),\dots,(q_{k-1},0,a_{k},q_{k})\in\Delta$
with $q_{k}=q$, $A=\\{a_{0},\dots,a_{k}\\}$.

We remark that $\mathop{\nu}(\mathcal{G})$ can be easily computed by
saturation.

###### Proposition 4

Whenever an STG $\mathcal{G}$ recognizes $L$, the 0-eliminated graph
$\mathop{\nu}(\mathcal{G})$ recognizes the language $\mathop{\nu}(L)$.

Given an STG $\mathcal{G}$, we compute its determinization by the usual subset
construction, see e.g. [17, Thm 3.3.2]. Determinization preserves the timed
language and thus the growth rate.

Given a deterministic $0$-free STG $\mathcal{G}$, we can compute its growth
rate using the technique of generating functions.

###### Construction 2

Given an STG $\mathcal{G}=(Q,\Sigma,\Delta)$ with $Q=\\{q_{1},\dots,q_{n}\\}$,
we define its $n\times n$ _adjacency matrix_ as

$M_{\mathcal{G}}(z)=(m_{ij}(z))\mathrm{\ with\
}m_{ij}(z)=\sum_{(q_{i},d,a,q_{j})\in\Delta}z^{d},$

and its _characteristic quasi-polynomial_ as
$\psi_{\mathcal{G}}(z)=\det(I-M_{\mathcal{G}}(z))$.

###### Proposition 5

Let $\mathcal{G}$ be a deterministic $0$-free STG, and let $z_{0}$ be the
smallest root (in modulus) of its _characteristic equation_
$\psi_{\mathcal{G}}(z)\\!=\\!0$. Then
$\beta(\mathcal{G})\\!=\\!-\\!\log|z_{0}|$.

###### Theorem 3.1

Given an STG $\mathcal{G}$, for $\varepsilon$ small enough,
$\mathcal{BC}_{\varepsilon}(\mathcal{G})=\mathcal{BH}_{\varepsilon}(\mathcal{G})=\beta(\mathcal{G})$.
The growth rate $\beta(\mathcal{G})$ is a logarithm of an algebraic number
computable as a function of $\mathcal{G}$.

###### Proof

The algorithm for computing $\beta(\mathcal{G})$ is as follows: eliminate 0,
determinize, write the adjacency matrix, and solve the characteristic
equation. Its correctness follows from the above propositions. ∎

As an example consider the STG on Fig. 5 (left). Its 0-free form is
represented in the middle, it is deterministic. The characteristic matrix and
equation are

$M(z)=\begin{pmatrix}z^{3}+2z^{5}&z^{3}\\\ z^{2}&z^{2}\end{pmatrix};\
\det(I-M(z))=2z^{7}-2z^{5}-z^{3}-z^{2}+1=0,$

with the smallest root $z_{0}\approx 0.698776$, the growth rate is
$-\log_{2}z_{0}\approx 0.517098$.

##  4 Computing the bandwidth of a meager RsTA

Consider a closure of a $(c-1)$-dimensional clock region $\bar{r}$ in the
clock space of $\mathcal{A}$. It is a simplex with $c$ vertices. The convex
hull of any subset of $k>0$ vertices of a region will be referred to as a
$(k-1)$-dimensional _face_. Note that each vertex and the whole closed region
are considered as faces. To each such face $f$ with vertices
$v_{1},\dots,v_{k}$ we associate its _barycenter_
$b=\frac{1}{k}\sum_{i=1}^{k}v_{k}$, as illustrated on Fig. 5, right. We denote
the set of all such face barycenters $\alpha(r)$.

Given a clock vector $x\in\bar{r}$, we consider the smallest face
$\mathfrak{f}(x)$ containing $x$ and denote $\alpha(x)$ the barycenter of
$\mathfrak{f}(x)$. Abusively, we also say that $x$ and $\alpha(x)$ have the
dimension $k-1$.

#### Barycentric abstraction.

Our method for the computation of the bandwidth of an RsTA involves
abstracting the RsTA by an STG whose states correspond to barycenters of the
faces of each start region in the RsTA. The transitions of the STG are exactly
the timed transitions of the original RsTA that allow a unique time delay and
do not change face dimension. Formally:

###### Construction 3

Given an RsTA $\mathcal{A}=(Q,X,\Sigma,\Delta,S,I,F)$, its _barycentric
abstraction_ is an STG
$\mathcal{G}=\alpha(\mathcal{A})=(Q^{\prime},\Sigma,\Delta^{\prime})$ obtained
as follows:

  * •

the state space is constituted by face barycenters of all the starting
regions:

$Q^{\prime}=\bigcup_{q\in Q}\\{q\\}\times\alpha(\overline{S(q)});$

  * •

for each edge $\delta=(p,p^{\prime},a,\mathfrak{g},\mathfrak{r})\in\Delta$,
and for each couple of barycenters $x\in\alpha(S(p))$ and
$x^{\prime}\in\alpha(S(p^{\prime}))$ of the same dimension,
if $L_{\bar{\delta}}((p,x),(p^{\prime},x^{\prime}))=\\{ta\\}$ for some unique
$t\in\mathds{Q}$, then $\Delta^{\prime}$ contains a transition
$((p,x),t,a,(p^{\prime},x^{\prime}))$. $\Delta^{\prime}$ contains no other
transitions.

Note that the abstraction leaves some edges of the RsTA without a counterpart
in the built STG. In fact, these removed edges can only appear a bounded
number of times within a run of a meager automaton, and thus are actually not
needed to produce the full amount of bandwidth.

For our running example, the region-split automaton $\mathcal{A}_{6}^{\prime}$
on Fig. 4 the starting region is 0-dimensional for $s$, just $(0,0)$. The two
other starting regions are 1-dimensional: $(0,1)\times\\{0\\}$ for $q$ and
$\\{0\\}\times(0,1)$ for $p$, in each of those there are two vertices and one
1-dimensional barycenter in the middle. The barycentric abstraction is
presented on Fig. 6, top; it splits into two connected components: one on
vertices (left subfigure) and one on region centers $(1/2,0)$ for $q$ and
$(0,1/2)$ for $p$ (right).

The theorem below states that the bandwidth of the apparently smaller language
$L(\mathcal{G})$ is indeed the same as that of $L(\bar{\mathcal{A}})$,
implying that the barycentric abstraction is sufficient for computing the
bandwidth of meager automata.

###### Theorem 4.1

For any meager RsTA $\mathcal{A}$ and its barycentric abstraction
$\mathcal{G}=\alpha(\mathcal{A})$, and for $\varepsilon$ small enough it holds
that

$\mathcal{BC}_{\varepsilon}(\mathcal{A})=\mathcal{BH}_{\varepsilon}(\mathcal{A})=\beta(L(\mathcal{G})).$

Let us sketch the main ideas of the proof.

The lower bound is not difficult. By the pigeonhole principle, there exists a
node $n=(p,x)$ of $\mathcal{G}$, such $L_{\mathcal{G}}(n,n)$ has growth rate
$\beta(L(\mathcal{G}))$. Let now $u$ a timed word leading in
$\bar{\mathcal{A}}$ from $I$ to $(p,x)$ and $v$ leading from $(p,x)$ to $F$.
Then it is easy to see (directly from Constr. 3) that $u\cdot
L_{\mathcal{G}}(n,n)\cdot v\subset L(\bar{\mathcal{A}})$ and hence
$\beta(L(\mathcal{G}))=\mathcal{BH}_{0}(u\cdot L_{\mathcal{G}}(n,n)\cdot
v)\leq\mathcal{BH}_{0}(u\cdot L_{\mathcal{G}}(n,n)\cdot
v)\leq\mathcal{BH}_{0}(L(\bar{\mathcal{A}}))=\mathcal{BH}_{0}(L(\mathcal{A}))$.333The
latter equality is a consequence of [5], full version, Lem. 35.

For the upper bound, as established in [5], the totality of the bandwidth of
meager automata is produced by cycles running from a unique state $(q,x)$ (in
the closure of the automaton) to itself. Moreover, each path from $(q,x)$ to
itself admits a unique timing. We prove that this bunch of cycles can be
approximated by a similar bunch on the barycenter $(q,\alpha(x))$. We count
elements of the latter using the STG $\mathcal{G}$.

As a comment, while our reasoning could possibly still be valid for other
choices of face representatives than barycenters (any interior point of a face
can represent it), our choice is not arbitrary because it allows for a terser
abstraction, based on a single, canonical, representative per face. Indeed,
when an edge in a cycle of a RsTA sends a face onto another face, the
barycenter of the destination face is always a successor of the barycenter of
the origin face.

Our main result is immediate from Thms. 4.1 and 3.1.

###### Theorem 4.2

The bandwidth of a meager DTA $\mathcal{A}$, for $\varepsilon$ small enough,
satisfies
$\mathcal{BC}_{\varepsilon}(\mathcal{A})=\mathcal{BH}_{\varepsilon}(\mathcal{A})=\beta$
with $\beta$ a logarithm of an algebraic number computable as a function of
$\mathcal{A}$.

We remark that the overall complexity of our algorithm is doubly exponential:
one exponent is due to region-splitting and taking barycenters of all faces,
the other to determinizing the STG. This is to compare to -completeness of
recognizing meager DTA[5].

$s$$q$$p$$0,a,b$$1,a,b$$0,a,b$$1,a,b$$0,a,b$$1,a,b$$1,a,b$$0,a,b$$q$$p$$1/2,a,b$$1/2,a,b$

$1,a,b,ab$$1,a,b$$1,a,b,ab$$1,a,b,ab$$1,a,b$$1,a,b,ab$$1,a,b$$1,a,b,ab$$1,a,b$$1,a,b,ab$$1/2,a,b$$1/2,a,b$

Figure 6: Top: barycentric abstraction
$\mathcal{G}=\alpha(\mathcal{A}_{6}^{\prime})$ split in components of
dimension 0 and 1. Bottom: the same graph after 0-elimination. Multiple labels
on an edge mean that there is an edge for each label, all with the same
timing.

For the running example $\mathcal{A}_{6}$, we proceed with 0-elimination for
the STG on Fig. 6 (top), the result is given on Fig. 6 (bottom). The graph
obtained is deterministic. The adjacency matrix of the 0-free STG obtained
splits into two diagonal blocks (corresponding to connected components of
barycenters of dimensions 0 and 1):

$\begin{pmatrix}0&3z&0&3z&2z\\\ 0&3z&0&3z&2z\\\ 0&0&0&0&0\\\ 0&0&2z&3z&0\\\
0&0&2z&3z&0\end{pmatrix};\quad\begin{pmatrix}0&2z^{1/2}\\\
2z^{1/2}&0\end{pmatrix}.$

The characteristic equation also splits:

$(1-3z)^{2}(1-4z)=0.$

The smallest root (corresponding to dimension 1 barycenters) is $1/4$, the
bandwidth is $-\log 1/4=2$.

##  5 Conclusions

We have solved the problem of computing the bandwidth for simply-timed graphs
and based on that, for all meager automata. Our main tool is the barycentric
abstraction, a new construction that can be seen as a refinement of the corner
point automaton from [7] (which, in turn, refines the region automaton [1]).

The next step is to build appropriate abstractions for computing the bandwidth
of normal and obese automata, using the tools from [5]. Synthesis of timed
codes and their applications would be the outcome of this research program.

## References

  * [1] Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8
  * [2] Aristotle: Physics (350 BCE), https://classics.mit.edu/Aristotle/physics.html
  * [3] Asarin, E., Basset, N., Degorre, A.: Entropy of regular timed languages. Information and Computation 241, 142–176 (2015). https://doi.org/10.1016/j.ic.2015.03.003
  * [4] Asarin, E., Basset, N., Degorre, A.: Distance on timed words and applications. In: Proc. FORMATS. LNCS, vol. 11022, pp. 199–214 (2018). https://doi.org/10.1007/978-3-030-00151-3_12
  * [5] Asarin, E., Degorre, A., Dima, C., Jacobo Inclán, B.: Bandwidth of timed automata: 3 classes. In: Proc. FSTTCS. LIPIcs, vol. 284, pp. 10:1–10:17 (2023). https://doi.org/10.4230/LIPICS.FSTTCS.2023.10, full version https://doi.org/10.48550/arXiv.2310.01941
  * [6] Bérard, B., Petit, A., Diekert, V., Gastin, P.: Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae 36(2-3), 145–182 (1998). https://doi.org/10.3233/FI-1998-36233
  * [7] Bouyer, P., Brinksma, E., Larsen, K.G.: Staying alive as cheaply as possible. In: Proc. HSCC. LNCS, vol. 2993, pp. 203–218 (2004). https://doi.org/10.1007/978-3-540-24743-2_14
  * [8] Bridson, M.R., Gilman, R.H.: Context-free languages of sub-exponential growth. Journal of Computer and System Sciences 64(2), 308–310 (2002). https://doi.org/10.1006/jcss.2001.1804
  * [9] Chomsky, N., Miller, G.A.: Finite state languages. Information and Control 1(2), 91 – 112 (1958). https://doi.org/10.1016/S0019-9958(58)90082-2
  * [10] Dima, C.: Real-time automata. Journal of Automata, Languages and Combinatorics 6(1), 3–23 (2001). https://doi.org/10.25596/JALC-2001-003
  * [11] Fekete, M.: Über die Verteilung der Wurzeln bei gewissen algebraischen Gleichungen mit ganzzahligen Koeffizienten. Mathematische Zeitschrift 17, 228–249 (1923). https://doi.org/10.1007/BF01504345
  * [12] Gawrychowski, P., Krieger, D., Rampersad, N., Shallit, J.: Finding the growth rate of a regular or context-free language in polynomial time. In: Proc. DLT. LNCS, vol. 5257, pp. 339–358 (2008). https://doi.org/10.1007/978-3-540-85780-8_27
  * [13] Grigorchuk, R., Machí, A.: An example of an indexed language of intermediate growth. Theoretical Computer Science 215(1), 325–327 (1999). https://doi.org/10.1016/S0304-3975(98)00161-3
  * [14] Jacobo Inclán, B., Degorre, A., Asarin, E.: Bounded delay timed channel coding. In: Proc. FORMATS. LNCS, vol. 13465, pp. 65–79 (2022). https://doi.org/10.1007/978-3-031-15839-1_4
  * [15] Kolmogorov, A., Tikhomirov, V.: $\varepsilon$-entropy and $\varepsilon$-capacity of sets in function spaces. Uspekhi Matematicheskikh Nauk 14(2), 3–86 (1959). https://doi.org/10.1007/978-94-017-2973-4_7
  * [16] Lancaster, P.: Lambda-matrices and Vibrating Systems. Pergamon Press (1966)
  * [17] Lind, D., Marcus, B.: An Introduction to Symbolic Dynamics and Coding. Cambridge University Press (1995)
  * [18] Markey, N., Schnoebelen, P.: Symbolic model checking for simply-timed systems. In: Proc. FORMATS/FTRTFT. LNCS, vol. 3253, pp. 102–117 (2004). https://doi.org/10.1007/978-3-540-30206-3_9
  * [19] Puri, A.: Dynamical properties of timed automata. Discrete Event Dynamic Systems 10(1-2), 87–113 (2000). https://doi.org/10.1023/A:1008387132377
  * [20] Simon, I.: Factorization forests of finite height. Theoretical Computer Science 72(1), 65–94 (1990). https://doi.org/10.1016/0304-3975(90)90047-L

##  Appendix 0.A Proof details concerning STG

###  0.A.1 Proof of Prop. 2

###### Proof

Let $L$ be the language of an STG and assume that all delays labeling
transitions of the STG are multiple of $1/N$ for some $N\in\mathds{N}$. Let
also $K\in\mathds{N}$ be an upper bound for all transition’s delays.

We have that

$L_{T_{1}+T_{2}+K}\subset L_{T_{1}+K}\cdot L_{T_{2}+K}$

(each long run can be split into two shorter ones), thus

$\Upsilon(L_{T_{1}+T_{2}+K})\leq\Upsilon(L_{T_{1}+K})\cdot\Upsilon(L_{T_{2}+K}),$

and the function $f(T)=\log\Upsilon(L_{T+K})$ is subadditive. Fekete’s lemma
[11] states that whenever $f$ is subadditive, $\lim_{T\to\infty}f(T)/T$
exists. In our case, this is the required limit (the growth rate of $L$).

To relate the bandwidth with the growth rate, we remark that for words
$w_{1},w_{2}\in L$ the distance $d(w_{1},w_{2})$ is always multiple of $1/N$,
hence $d(w_{1},w_{2})\neq 0\Leftrightarrow d(w_{1},w_{2})\geq 1/N$.
Consequently, the notions of $0$-separated and $\varepsilon$-separated sets
coincide for $\varepsilon<1/N$. This implies that
$\mathcal{C}_{\varepsilon}(L_{T})=\log\Upsilon(L_{T})$.

As for $\varepsilon$-entropy, we can use the inequality
$\mathcal{C}_{2\varepsilon}(L_{T})\leq\mathcal{H}_{\varepsilon}(L_{T})\leq\mathcal{C}_{\varepsilon}(L_{T})$
from [15] to conclude that everything coincides for $\varepsilon<1/2N$:

$\mathcal{H}_{\varepsilon}(L_{T})=\mathcal{C}_{\varepsilon}(L_{T})=\log\Upsilon(L_{T});$

dividing by $T$ and taking the limit we obtain the required equality of
bandwidths. ∎

###  0.A.2 Proof of Prop. 3

###### Proof

For any finite set $S$ of timed words over alphabet $\Sigma$, we will prove
that

$\\#\mathop{\nu}(S)\leq\Upsilon(S)\leq\\#\mathop{\nu}(S)(2^{\\#\Sigma}-1).$
(1)

The inequality $\\#\mathop{\nu}(S)\leq\Upsilon(S)$ comes from the fact that
for each word $w\in\nu(S)$ one can select one word $\tilde{\nu}(w)\in
S\cap\nu^{-1}(w)$; hence we obtain the set $\tilde{\nu}(\nu(S))$ which is a
$0$-separated subset of $S$ with the cardinality of $\nu(S)$.

For $\Upsilon(S)\leq\\#\mathop{\nu}(S)(2^{\\#\Sigma}-1)$: consider any
$0$-separated subset $E$ of $S$. Consider the application $s$ that deletes all
the letters at time $0$ from a timed word. Then
$\mathop{\nu}(s(E))=\mathop{\nu}(E)$. Just remark that, because $E$ is
$0$-separated, every word in $\mathop{\nu}(s(E))$ only has a single pre-image
by $\mathop{\nu}$ in $s(E)$ and words from $s(E)$ at most $2^{\\#\Sigma}-1$
pre-images in $E$ by $s$. Hence
$\\#E\leq\\#\mathop{\nu}(E)(2^{\\#\Sigma}-1)\leq\\#\mathop{\nu}(S)(2^{\\#\Sigma}-1)$.
Since this is true for any $0$-separated subset $E$ of $S$, we conclude
$\Upsilon(S)\leq\\#\mathop{\nu}(S)(2^{\\#\Sigma}-1)$.

The proposition statement is immediate: applying Eq. 1 to $L_{T}$, we get
$\\#\Upsilon(\mathop{\nu}(L_{T}))\leq\Upsilon(L_{T})\leq\Upsilon(\\#\mathop{\nu}(L_{T}))(2^{\\#\Sigma}-1)$.
Taking the limit of the logarithms divided by $T$, we obtain the desired
result.

###  0.A.3 Proof of Prop. 5

###### Proof

First, let us define $L_{d}=\\{w\in
L(\mathcal{G}),\mathop{\mathrm{dur}}(w)=d\\}$ and remark that
$\beta(L(\mathcal{G}))=\lim_{T\to\infty}\frac{\log\sum_{d<T}\\#L_{d}}{T}=\lim_{d\to\infty}\frac{\log\\#L_{d}}{d}$;
let us call that number just $\beta$.

Then notice that all the delays in $\mathcal{G}$ are rational numbers with
denominators in a finite set of positive natural numbers $D$. Hence, if $m$ is
the lcm of $D$, $M_{\mathcal{G}}(\zeta^{m})$ is a matrix of polynomials in
$\zeta$.

Consider the formal matrix series
$R(\zeta)=(I-M_{\mathcal{G}}(\zeta^{m}))^{-1}=\sum_{k=0}^{\infty}M_{\mathcal{G}}^{k}(\zeta^{m})$.
Its elements are $R_{ij}(\zeta)=\sum_{n\in\mathds{N}}c_{ijn}\zeta^{n}$, where
$c_{ijn}$ is the number of runs from $q_{i}$ to $q_{j}$ with duration
$d=\frac{n}{m}$. Remark that
$\max_{i,j}c_{ijn}\leq\\#L_{d}\leq\sum_{i,j}c_{ijn}$.

Take some positive $a<|z_{0}|$, then $\det(I-M_{\mathcal{G}}(a))\neq 0$, the
matrix $(I-M_{\mathcal{G}}(a))^{-1}$ is well-defined, and thus, for
$\alpha=a^{-m}$, $\sum_{n}c_{ijn}\alpha^{n}$ converges and so does $\\#L_{d}$,
hence, for $n$ large enough, $\\#L_{d}\alpha^{n}<1$. This implies
$\\#L_{d}<\alpha^{-md}$ and thus $\beta$, the growth rate wrt $d$, verifies
$\beta\leq-m\log\alpha=-\log a$. Since $a$ can be arbitrary close to $z_{0}$
we conclude that $\beta\leq-\log|z_{0}|$.

On the other hand, suppose for contradiction that $\beta<-\log|z_{0}|-b$ for
some positive $b$. Since $\det(I-M_{\mathcal{G}}(z_{0}))=0$, there exists a
non-zero vector $u$ such that $M_{\mathcal{G}}(z_{0})u=u$, thus the series
$\sum_{k}M^{k}_{\mathcal{G}}(z_{0})u=\sum_{k}u$ diverges, hence some of its
matrix elements $R_{ij}(z_{0})$ diverge. But $c_{ijn}\leq\\#L_{d}\leq
K2^{\beta d}<z_{0}^{-d}2^{-bd}$ (for some positive constant $K$ and $d$ large
enough) and thus the general term of $R_{ij}(z_{0})$ is smaller than $2^{-bd}$
implying that $R_{ij}(z_{0})$ must also converge, which is contradictory.∎

##  Appendix 0.B Preparatory results

###  0.B.1 Puri’s reachability method

We recall here some basics on reachability in timed automata, mostly due to
[19] and slightly reformulated in [3, 5]. We will use a specific coordinate
system on clock regions.

######  Construction 4 (Canonical barycentric coordinates)

Given a $k-1$-dimensional region $r$ we compare its vertices as follows:
$v<v^{\prime}$ whenever $v\cdot\mathbf{1}<v^{\prime}\cdot\mathbf{1}$ (it is
easy to see that this is a total order). We enumerate all the vertices in the
ascending order: $v_{1}<v_{2}<\cdots<v_{k}$. For any clock vector
$x\in\bar{r}$ we define its _barycentric coordinates_
$\boldsymbol{\lambda}(x)=(\lambda_{1},\dots,\lambda_{k})$ by conditions

$\sum_{i=1}^{k}\lambda_{i}v_{i}=x;\quad\sum_{i=1}^{k}\lambda_{i}=1;\quad
0\leq\lambda_{i}\leq 1.$

Given a path $q\xrightarrow{\pi}q^{\prime}$, and faces $r$ and $r^{\prime}$ in
$S(q)$ and $S(q^{\prime})$ respectively, we aim to characterize when $x\in r$
can go to $x^{\prime}\in r^{\prime}$ through $\bar{\pi}$ (the closure of the
path). That is, there exists a run $\rho$ associated with $\bar{\pi}$. The
main tool of Puri’s method is the _orbit graph_ summarizing reachability
between vertices regions.

###### Definition 13

The _orbit graph_ $\gamma(\pi)$ is a bipartite graph from vertices of $r$ to
those of $r^{\prime}$. It has an edge $v\to v^{\prime}$ whenever $v$ can go to
$v^{\prime}$ through $\bar{\pi}$. The _orbit matrix_ $M(\pi)$ is the adjacency
matrix of $\gamma(\pi)$.

######  Theorem 0.B.1 ([19])

Given a path $q\xrightarrow{\pi}q^{\prime}$, a state $(q^{\prime},x^{\prime})$
(with $x^{\prime}$ in an $n^{\prime}$-dimensional region face) is reachable
from a state $(q,x)$ (with $x$ in an $n$-dimensional region face) through
$\bar{\pi}$ iff there exists an $n\times n^{\prime}$ stochastic matrix444That
is, $P\cdot\mathbf{1}_{n}=\mathbf{1}_{n^{\prime}}$. $P$ satisfying
$\boldsymbol{\lambda}(x)P=\boldsymbol{\lambda}(x^{\prime})$ and $P\leq
M(\pi)$.

We call such a $P$ a reachability matrix from $x$ to $x^{\prime}$ along
$\bar{\pi}$. We will enrich $P$ with duration information as follows. If for
all $i$ and $j$, such that $P_{ij}>0$, there is at most a single possible run
$\rho_{ij}$ from $v_{i}$ to $v^{\prime}_{j}$ through $\bar{\pi}$, then we
define the timing matrix $D^{P}$, such that

$D^{P}_{ij}=\begin{cases}\mathop{\mathrm{dur}}(\rho_{ij})&\text{if
}P_{ij}>0;\\\ 0&\text{otherwise}.\end{cases}$

###### Proposition 6

Let $P$ be a reachability matrix from $x$ to $x^{\prime}$ along $\bar{\pi}$,
with a well-defined timing matrix $D^{P}$. Then $x$ can go to $x^{\prime}$ in
time $d=\sum_{i,j}{\lambda_{i}(x)P_{ij}D^{P}_{ij}}$.

######  Proof (sketch)

First, remark that, for each $i$, there is a run $\rho_{i}$ along $\pi$ from
$v_{i}$ to $\sum_{j}P_{ij}v^{\prime}_{j}$ that lasts
$\sum_{j}P_{ij}D_{ij}^{P}$ (by convex combination of runs from $v_{i}$ to
$v^{\prime}_{j}$). Then, we make a convex combination of the $\rho_{i}$
according to weights in $\boldsymbol{\lambda}(x)$. Since
$x=\sum_{i}\lambda_{i}(x)v_{i}$, we obtain a run from $x$ to
$\sum_{i}\sum_{j}P_{ij}v^{\prime}_{j}=\sum_{j}(\sum_{i}P_{ij})v_{j}=x^{\prime}$
that lasts $\sum_{ij}\lambda_{i}(x)P_{ij}D_{ij}^{P}$. ∎

###  0.B.2 On cycles in meager timed automata

Through the next two sections, we consider a cyclic run (along some path
$\pi$)

$(q,x)=(q_{0},x_{0})\to(q_{1},x_{1})\to\cdots\to(q_{k},x_{k})=(q,x)$

in a meager RsTA. Let $r_{i}=\mathfrak{f}(x_{i})$ be the smallest face
containing $x_{i}$ and $P_{i}$ the reachability matrix from $x_{i-1}$ to
${x_{i}}$. By definition of $\mathfrak{f}(x_{i})$, all components of
$\boldsymbol{\lambda}(x_{i})$ are positive and
$\boldsymbol{\lambda}(x_{i-1})P_{i}=\boldsymbol{\lambda}(x_{i})$. Through a
series of lemmas, we will characterize matrices $P_{i}$ and also the
transition delays.

###### Lemma 1

Let $\pi$ be the path of the cyclic run, and take $\pi^{j}$ its power with
idempotent $\gamma(\pi^{j})$. Then the orbit graph $\gamma(\pi^{j})$ has self-
loops on all vertices of the face $r$ of $x$.

###### Proof

Suppose this is not the case for some vertex $u$. Take $U$ the set of vertices
$v$ such that there is a path from $v$ to $u$ in $\gamma(\pi)$ (and
necessarily in $\gamma(\pi^{j})$). Let $\lambda_{U}=\sum_{v\in
U}{\lambda_{v}}$. Then through $\pi$, $\lambda_{U}(x)$ diminishes which means
at least one of the $\lambda_{v}(x)$ does as well. But then it is impossible
to get the same coordinates after the cycle, which means it is impossible to
return to $x$. ∎

###### Lemma 2

All faces $r_{i}$ have the same dimension. Hence all $P_{i}$ are square
matrices.

###### Proof

Suppose this is not the case, and the run contains two points $x$ and
$x^{\prime}$ in faces $r$ and $r^{\prime}$ of dimensions $n$ and $n^{\prime}$,
with $n<n^{\prime}$ (this is w.l.o.g. as the cyclic run can be taken from
$x^{\prime}$). We denote the part of the cycle from $x$ to $x^{\prime}$ by
$\pi^{1}$ and from $x^{\prime}$ to $x$ by $\pi^{2}$, and $\pi^{1}\pi^{2}$ by
$\pi$. Denote $P^{1},P^{2},P$ the corresponding reachability matrices and
$g^{1},g^{2},g$ the orbit graphs without edges whose coefficient is null in
$P^{1},P^{2},P$.

Because $n<n^{\prime}$, there has to be at least one vertex $u$ of $r$ having
(at least) two outgoing arrows in $g^{1}$ to vertices $u^{\prime}_{1}\neq
u^{\prime}_{2}$ of $r^{\prime}$, which have themselves edges to $v_{1}$ and
$v_{2}$ (in $r$) along $g^{2}$ (they might be the same vertex). In the region
$r$, we consider $U$ the set of vertices $w$ such that there is a path of
edges in $g$ going from $w$ to $u$. Then both $v_{1}$ and $v_{2}$ belong to
$U$ because otherwise, from the previous lemma, $u\in U$ and $\lambda_{U}(x)$
would decrease (either along $(u,v_{1})$ or $(u,v_{2})$). However, if both
$v_{1}$ and $v_{2}$ are in $U$, let $l$ and $L$ be the shortest paths from
each of them to $u$, then the orbit graph of the path $\pi^{(l+1)(L+1)}$ has
two ways of going from $u$ to itself, which contradicts $\mathcal{A}$ being
meager. ∎

Let $k$ be the dimension of all the faces $r_{i}$. As a consequence of this
lemma the following holds.

###### Lemma 3

Reachability matrices $P_{i}$ can be written containing only 0 and 1, written
in this way they define bijections on $k$ vertices.

###### Proof

Take $\pi^{j}$ as in Lem. 1, then in $\gamma(\pi^{j})$ all vertices have self-
loops. By following the only path of each vertex to itself, we get a run that
goes back to $x$. This is a cyclic run, which means all interior $x_{i}$ are
of the same dimension, so necessarily no vertex-to-vertex paths coincide on
any point. This is in particular true for the first occurrence of $\pi$ which
gives the expected result. ∎

The next result shows that the delays between vertices are close to each
other.

###### Lemma 4

Let $\xi$ ($u=u_{0}\xrightarrow{d_{1}}\dots\xrightarrow{d_{k}}u_{k}=u$) and
$\xi^{\prime}$
($v=v_{0}\xrightarrow{d^{\prime}_{1}}\dots\xrightarrow{d^{\prime}_{k}}v_{k}=v)$
be cyclic runs of vertices corresponding to the same path $\bar{\pi}$ of
transitions $\delta_{i}$ in $\bar{\mathcal{A}}$ ($u_{i}$ and $v_{i}$ are
vertices of $r_{i}$). Then the following holds.

  1. 1.

For every $i$, assuming w.l.o.g. that $u_{i-1}\leq v_{i-1}$, either
$d_{i}=d^{\prime}_{i}$ and then $u_{i}\leq v_{i}$ or $d_{i}=d^{\prime}_{i}+1$
and then $u_{i}\geq v_{i}$.

  2. 2.

Both paths have the same duration: $\sum{d_{i}}=\sum{d^{\prime}_{i}}$.

###### Proof

Note that $\mathcal{A}$ being meager, these paths are the only ones cycling
from $u$ to itself and from $v$ to itself. Hence, if $u=v$ there is nothing to
prove.

We consider the case where $u\neq v$. For every $i$, $u_{i}\neq v_{i}$,
otherwise two different paths are going from $u_{i}$ to itself through the
same shifted version of $\pi$ (one passing through $u$, the other through $v$)
which is in contradiction with the fact that $\mathcal{A}$ is meager.

Moreover, one cannot have at the same time $v_{i}$ reachable from $u_{i-1}$
and $u_{i}$ reachable from $v_{i-1}$ through $\delta_{i}$. If this were the
case, through the same shifted version of $\pi$ we can go from $u_{i}$ and
$v_{i}$ to themselves and each other. By repeating this cycle twice, we get
two ways of going from $u_{i}$ (and $v_{i}$) to itself, which is again
impossible in a meager automaton.

We now fix $i$, and we will look at the difference between $d_{i}$ and
$d^{\prime}_{i}$. We can consider w.l.o.g. $u_{i-1}<v_{i-1}$. These being two
vertices of the same region $r_{i-1}$, we can partition the set of all clocks
as $X=X_{eq}\cup X_{neq}$ such that for all $c\in X_{eq}$,
${(u_{i-1})}_{c}={(v_{i-1})}_{c}$ (with $u_{c}$ being the value of clock $c$
in the vertex $u$) and for all $c\in X_{neq}$,
${(u_{i-1}})_{c}+1={(v_{i-1})}_{c}$.

Consider the case where $d_{i}<d^{\prime}_{i}$. Since these timings are
integers, this means $d_{i}+1\leq d^{\prime}_{i}$. Given $c\in X_{neq}$, we
have ${(u_{i-1})}_{c}+d_{i}+2\leq{(v_{i-1})}_{c}+d^{\prime}_{i}$, hence
${(u_{i-1})}+d_{i}$ and ${(v_{i-1})}+d^{\prime}_{i}$ are not be in the same
closed region. But $u_{i}$ and $v_{i}$ must be in the same closed region, so
necessarily $c\in\mathfrak{r}_{\delta_{i}}$. We also have that
$u_{i-1}+d_{i}\models g(\delta_{i})$ and $v_{i-1}+d^{\prime}_{i}\models
g(\delta_{i})$. Since $u_{i-1}+d_{i}<v_{i-1}+d_{i}\leq
u_{i-1}+d^{\prime}_{i}<v_{i-1}+d^{\prime}_{i}$, by convexity (on each
coordinate), all these 4 clock vectors satisfy the guard of $\delta_{i}$.
Because clocks that are different in $u_{i-1}$ and $v_{i-1}$ are reset,
$(u_{i-1}+d_{i})[\mathfrak{r}_{\delta_{i}}]=(v_{i-1}+d_{i})[\mathfrak{r}_{\delta_{i}}]=u_{i}$
and
$(u_{i-1}+d^{\prime}_{i})[\mathfrak{r}_{\delta_{i}}]=(v_{i-1}+d^{\prime}_{i})[\mathfrak{r}_{\delta_{i}}]=v_{i}$;
this means that $v_{i}$ is reachable from $u_{i-1}$ and $u_{i}$ from $v_{i-1}$
through $\delta_{i}$, which is a contradiction.

So necessarily $d_{i}\geq d^{\prime}_{i}$.

Consider the case where $d_{i}\geq d^{\prime}_{i}+2$. By similar reasoning as
before, we get that for $c\in X_{eq}$, $c\in\mathfrak{r}_{\delta_{i}}$. We
also get $v_{i-1}+d^{\prime}_{i}\leq u_{i-1}+d^{\prime}_{i}+1\leq
v_{i-1}+d_{i}-1\leq u_{i-1}+d_{i}$ with all these clock vectors satisfying the
guards of $\delta_{i}$. By taking timings $d^{\prime}_{i}+1$ for $u_{i-1}$ and
$d_{i}-1$ for $v_{i-1}$ we reach $v_{i}$ and $u_{i}$ respectively, which leads
to the same contradiction as before.

So the only possible options are $d_{i}=d^{\prime}_{i}$ or
$d_{i}=d^{\prime}_{i}+1$.

It is easy to notice that whenever $d_{i}=d^{\prime}_{i}$ then $u_{i}<v_{i}$
and whenever $d_{i}=d^{\prime}_{i}+1$ then $u_{i}>v_{i}$ (equality of delays
preserves ordering, while inequality swaps it).

Now consider the whole cycle again. Observe that on odd-numbered swaps, we
have $d=d^{\prime}+1$ and, on even-numbered ones, $d+1=d^{\prime}$. Hence in
any factor with an even number of swaps, the duration of both considered STG
paths is the same, but this is necessarily the case for the whole cycle (since
$u$ and $v$ cycle back to themselves through the two considered cycles of the
STG). So both cycles have the same duration. ∎

###### Corollary 1

All matrices $P_{i}$ have one of the forms

$P^{kl}=\left(\begin{array}[]{c|c}0_{l\times(k-l)}&I_{l}\\\ \hline\cr
I_{k-l}&0_{(k-l)\times l}\end{array}\right).$

The form $P^{kl}$ of the transition matrix corresponds to the timing matrix
$D^{P}$ of the form

$D^{kld}=\left(\begin{array}[]{c|c}0_{l\times(k-l)}&(d+1)\cdot I_{l}\\\
\hline\cr d\cdot I_{k-l}&0_{l\times(k-l)}\end{array}\right).$

###### Proof

Consider a transition, on $k$-dimensioned faces, where $l$ “slow” vertices
make it in $d+1$ time units, while the others (“fast ”) make it in $d$ time
units. It follows from Lem. 4, that the slow vertices are $v_{1}\dots v_{l}$
and they go to $v^{\prime}_{k-l+1}\dots v^{\prime}_{k}$ (in the same order),
while the fast ones are $v_{l+1}\dots v_{k}$ that go to $v^{\prime}_{1}\dots
v^{\prime}_{k-l}$. In matrix form, this corresponds to the statement to prove.
∎

###### Corollary 2

Let $\rho$ and $\rho^{\prime}$ be two cyclic runs on $x$ and $x^{\prime}$ such
that $path(\rho)=path(\rho^{\prime})=\pi$, let $w=word(\rho)$ and
$w^{\prime}=word(\rho^{\prime})$. Then $w$ and $w^{\prime}$ have the same
duration.

###### Proof

Consider $\pi^{j}$ a power of the path such that its orbit graph is
idempotent. In this orbit graph, all vertices have self-loops, from Lem. 4,
going from each of these vertices to itself via $\pi^{j}$ is done in the same
amount of time, which means that a cycle through $\pi^{j}$ is done in the same
amount of time $t$ in any point of the face. Along the orbit graph of $\pi$,
the same vertices either have self-loops, or they are in a permutation with
other vertices having the same weight in $x$ and $x^{\prime}$. In any case,
the duration of a cyclic run is necessarily $t/j$. ∎

###  0.B.3 Relating cycles with barycenters

###### Lemma 5

Let $\rho$ be a cyclic run of path $\pi$ on $x$ (of dimension $k-1$), then
there is a cyclic run of the same path on barycenters $\alpha(x)$. Moreover,
the reachability matrices are the same on both runs.

###### Proof

Consider the $P_{i}$ from the previous section for the run on $x$. Applying
the same matrices we get a run of the same path starting on $\alpha(x)$.
Moreover, as
$\boldsymbol{\lambda}(\alpha(x_{0}))=(\frac{1}{k},\dots,\frac{1}{k})$ and each
$P_{i}$ is a bijection on vertices, all the
$\boldsymbol{\lambda}(\alpha(x_{i}))$ will have exactly the same form, and
thus be barycenters of regions $r_{i}$. The run of barycenters will lead back
to $\alpha(x)$ which concludes the proof. ∎

Consider now delays in the barycentric cycle.

###### Lemma 6

In a barycentric cycle, whenever the duration matrix for transition $i$ has
the form $D^{kld}$ from Cor. 1, the transition
$\alpha(x_{i-1})\to\alpha(x_{i})$ takes $d+l/k$ time.

###### Proof

We notice, that due to meagerness, all delays in a barycentric cycle are
uniquely determined. Next, we apply Prop. 6 to the matrix $D^{kld}$ and the
barycenter with barycentric coordinates $(\frac{1}{k},\dots,\frac{1}{k})$. ∎

We will use the previous lemma in the reverse direction: knowing that the
barycenter takes a transition in $d+l/k$ time, we will deduce $l,k,d$, then
matrices $P^{kl}$ and $D^{kld}$, and finally the successors and timings in the
concrete run of $x_{i}$

###### Lemma 7

For any transition $x\xrightarrow{\bar{\delta},t}x^{\prime}$ on a cyclic run,
let

  * •

$f$ and $f^{\prime}$ be the region faces containing $x$ and $x^{\prime}$,
$k-1$ their dimension, $v_{1},\dots,v_{k}$ and
$v^{\prime}_{1},\dots,v^{\prime}_{k}$ their (ordered as in Constr. 4)
vertices;

  * •

$\boldsymbol{\lambda}$ and $\boldsymbol{\lambda}^{\prime}$ the barycentric
coordinates of $x$ and $x^{\prime}$ with respect to vertices;

  * •

$\alpha(x)\xrightarrow{\bar{\delta},t_{0}}\alpha(x^{\prime})$ the
corresponding transition between barycenters of faces $f$ and $f^{\prime}$.

Then $t=\tau_{k}(\boldsymbol{\lambda},t_{0})$ and
$\boldsymbol{\lambda}^{\prime}=\sigma_{k}(\boldsymbol{\lambda},t_{0})$, where
functions $\tau$ and $\sigma$ are always the same (for all states and all
automata). Moreover, $\tau_{k}(\boldsymbol{\lambda},t_{0})=0\Leftrightarrow
t_{0}=0$ and $\sigma_{k}(\boldsymbol{\lambda},0)=\boldsymbol{\lambda}$.

###### Proof

We first write $t_{0}$ as $d+l/k$ (with $0\leq l<k$), and conclude by Lem. 6
that reachability and delay matrices are $P^{kl}$ and $D^{kld}$. Hence
$x=\sum_{i=1}^{k}\lambda_{i}v_{i}$ would make the transition in
$d+\sum_{i=1}^{j}\lambda_{i}$ time units and arrive to

$x^{\prime}=\sum_{i=j+1}^{k}\lambda_{i}v^{\prime}_{i-j}+\sum_{i=1}^{j}\lambda_{i}v^{\prime}_{k-j+i}.$

Thus the transition time and the barycentric coordinates of the target are
uniquely determined. To be formal,

$t=\tau_{k}(\boldsymbol{\lambda},d+j/k)\triangleq
d+\sum_{i=1}^{j}\lambda_{i},\quad\boldsymbol{\lambda}^{\prime}=\sigma_{k}(\boldsymbol{\lambda},d+j/k)\triangleq\lambda_{j+1}\dots\lambda_{k}\lambda_{1}\dots\lambda_{j}.$

The statements concerning $t_{0}=0$ are now immediate. ∎

###  0.B.4 Corollary from [5, full version]

###### Definition 14

A number $b\in$ is called a _cycle growth bound_ of an RsTA $\mathcal{A}$
whenever there exists a constant $C$ such that for any $q\in
Q,x\in\bar{S}(q),T>0$, the language $L_{T}^{\bar{\mathcal{A}}}((q,x),(q,x))$
admits a $0$-net of cardinality $C2^{bT}$.

###### Proposition 7

If $b\in$ is a _cycle growth bound_ of a meager RsTA $\mathcal{A}$, then (for
any $\varepsilon>0$)

$\mathcal{BH}_{\varepsilon}(\mathcal{A})\leq\mathcal{BC}_{\varepsilon}(\mathcal{A})\leq
b.$

The quite technical (and based on Simon factorization) proof of this
proposition follows verbatim that of Lemmas 68–77 and Prop. 18 from [5, full
version].

###  0.B.5 Relating open and closed semantics

###### Lemma 8

For any $\varepsilon>0$ and any word $w\in L(\bar{\mathcal{A}})$, there exists
$w^{\prime}\in L(\mathcal{A})$ such that $d(w,w^{\prime})<\varepsilon$.

######  Proof (sketch)

It was proved in [5] that for any path $\pi$ we can define a homothety
$h_{\lambda}$ with a factor $\lambda\in(0,1)$ (its center is fixed
independently of $\lambda$ as any interior point of the polyhedron of correct
timings) such that, if we fix any run $\rho$ along $\pi$, having a timing
vector $\vec{t}$ satisfying the closed version of the constraints of $\pi$,
then $h_{\lambda}(\vec{t})$ satisfies the open version of the constraints of
$\pi$ (hence, changing the timing of $\rho$ from $\vec{t}$ to
$h_{\lambda}(\vec{t})$, with $\lambda$ close enough to $1$, we obtain a run
$\rho^{\prime}$ through $\pi$ in $\mathcal{A}$, such that
$d(\mathop{word}(\rho),\mathop{word}(\rho^{\prime}))<\varepsilon$). To lift
the previous result to the whole automaton, it remains to remark that the
paths of $\mathcal{A}$ and $\bar{\mathcal{A}}$ are the same since the two
automata have the same underlying graph. ∎

Remark that this result only holds thanks to region-splitting: indeed, the
result relies on Puri’s characterization of reachability between regions. In
particular, it is well known that general TA may have non-realizable paths
that become realizable after closing guards (in this case, no homothety can
make their languages similar).

##  Appendix 0.C Proof of main Thm. 4.1

We have proved on Thm. 4.1 that

$\mathcal{BC}_{\varepsilon}(\mathcal{A})\geq\beta(\alpha(\mathcal{A}));\quad\mathcal{BH}_{\varepsilon}(\mathcal{A})\geq\beta(\alpha(\mathcal{A})).$
(2)

The proof (below) of the opposite inequality is based on Prop. 7.

###  0.C.1 Bounding the cycle growth

It remains to prove that the growth rate of $\mathcal{G}=\alpha(\mathcal{A})$
is a cycle growth bound for $\mathcal{A}$. To that aim, we concentrate on
cycles in $\mathcal{A}$.

###### Construction 5

Given a timed word $w$ accepted by a (unique) cyclic run $\rho$ from $(q,x)$
to $(q,x)$, let us consider its abstraction $\alpha(\rho)$. In turn, it
accepts some $w^{\prime}\in L^{\mathcal{G}}((q,\alpha(x)),(q,\alpha(x))$. We
denote $w^{\prime}=\alpha_{qx}(w)$.

Let us summarize some of its properties, immediate from the preceding lemmas.

###### Lemma 9

Whenever $w^{\prime}=\alpha_{qx}(w)$, for $w=(a_{1},t_{1})\dots(a_{n},t_{n})$,

  * •

$w^{\prime}$ has the form
$w^{\prime}=(a_{1},t^{\prime}_{1})\dots(a_{n},t^{\prime}_{n})$;

  * •

its duration is the same as that of $w$, i.e. $t^{\prime}_{n}=t_{n}$;

  * •

admitting that the cycle for $w$ passes through the states with barycentric
coordinates
$\boldsymbol{\lambda}^{0},\boldsymbol{\lambda}^{1},\dots,\boldsymbol{\lambda}^{n}=\boldsymbol{\lambda}^{0}$,
we have that

$t_{i}-t_{i-1}=\tau(\boldsymbol{\lambda}^{i-1},t^{\prime}_{i}-t^{\prime}_{i-1}),\quad\boldsymbol{\lambda}^{i}=\sigma(\boldsymbol{\lambda}^{i-1},t^{\prime}_{i}-t^{\prime}_{i-1}).$

###### Lemma 10

Let $w^{1},w^{2}\in L_{T}^{\bar{\mathcal{A}}}((q,x),(q,x))$ be two timed words
such that
$d(w^{1},w^{2})>0$ (necessarily they are recognized along different cyclic
paths), and ${w^{i}}^{\prime}=\alpha_{qx}(w^{i}),i=1,2$. Then
$d({w^{1}}^{\prime},{w^{2}}^{\prime})>0$.

###### Proof

For contradiction, suppose that $d({w^{1}}^{\prime},{w^{2}}^{\prime})=0$. Then
by Prop. 1, $\mathop{\nu}({w^{1}}^{\prime})=\mathop{\nu}({w^{2}}^{\prime})$,
let it be:

$\mathop{\nu}({w^{1}}^{\prime})=\mathop{\nu}({w^{2}}^{\prime})=(A_{1},t^{\prime}_{1}),(A_{2},t^{\prime}_{2}),\dots,(A_{n},t^{\prime}_{n})$

with $A_{j}\in 2^{\Sigma}$. Let $A_{0}$ be the set of events happening in
${w^{1}}^{\prime}$ and ${w^{2}}^{\prime}$ at time $0$ (necessary it is the
same set, eventually empty). By construction of ${w^{i}}^{\prime}$, the words
$w^{i}$ have the same form, with eventually different timing (in particular,
the last statement of Lem. 7 guarantees that $w^{i}$ and ${w^{i}}^{\prime}$
have 0-time transitions at the same positions), thus

$\mathop{\nu}({w^{i}})=(A_{1},t^{i}_{1}),(A_{2},t^{i}_{2}),\dots,(A_{n},t^{i}_{n}),\text{
with }i=1,2,$

and $w^{i}$ also have the set of events $A_{0}$ at the beginning.

Let $\boldsymbol{\lambda}_{0}$ be the barycentric coordinates of $x$. The run
of $\mathcal{A}$ from $(q,x)$ over $w^{i}$ visits the points with barycentric
coordinates:

  * •

$\boldsymbol{\lambda}_{0}$ in the beginning;

  * •

$\sigma(\boldsymbol{\lambda}_{0},0)=\boldsymbol{\lambda}_{0}$ again after
reading every letter of $A_{0}$, by Lem. 7;

  * •

$\boldsymbol{\lambda}_{1}=\sigma(\boldsymbol{\lambda}_{0},t^{\prime}_{1})$
after the next transition;

  * •

and again $\boldsymbol{\lambda}_{1}$ after reading each letter of $A_{1}$;

  * •

$\boldsymbol{\lambda}_{2}=\sigma(\boldsymbol{\lambda}_{1},t^{\prime}_{2}-t^{\prime}_{1})$
etc.

We see that runs on both words $w^{1}$ and $w^{2}$ follow the same sequence of
barycentric coordinates. Applying again Lem. 7 we conclude that they also have
the same timing since the transition from $\boldsymbol{\lambda}_{j}$ to
$\boldsymbol{\lambda}_{j+1}$ always takes
$\tau(\boldsymbol{\lambda}_{j},t^{\prime}_{j+1}-t^{\prime}_{j})$ time. From
that we deduce that $\mathop{\nu}({w^{1}})=\mathop{\nu}({w^{2}})$, and both
$w^{1}$ and $w^{2}$ have the same set $A_{0}$ of events at time $0$, thus
$d(w^{1},w^{2})=0$, a contradiction. ∎

###### Lemma 11

$\beta(\mathcal{G})$ is a cycle growth bound for $\mathcal{A}$.

###### Proof

Let $\mathcal{N}$ be a maximal $0$-separated set in
$L_{T}^{\bar{\mathcal{A}}}((q,x),(q,x))$ (it is also a minimal $0$-net). Its
image $\mathcal{N}^{\prime}=\alpha_{qx}(\mathcal{N})$ by virtue of Lem. 10 is
$0$-separated and of the same cardinality. By construction
$\mathcal{N}^{\prime}\subset
L_{T}^{\mathcal{G}}((q,\alpha(x)),(q,\alpha(x)))$. Hence
$\\#\mathcal{N}=\\#\mathcal{N^{\prime}}\leq C2^{\beta T}$, thus
$\beta(\mathcal{G})$ is a cycle growth bound for $\mathcal{A}$. ∎

Thm. 4.1 follows immediately from Props. 7 and 11.