pith. sign in

arxiv: 2606.11003 · v1 · pith:RR6Q3ULTnew · submitted 2026-06-09 · 💻 cs.FL · cs.IT· math.IT

Weighing Timed Regular Languages: The Final Step (long version)

Eugene Asarin , Aldric Degorre , Catalin Dima , Bernardo Jacobo Incl\'an This is my paper

Pith reviewed 2026-06-27 10:33 UTC · model grok-4.3

classification 💻 cs.FL cs.ITmath.IT
keywords timed automatatimed languagesbandwidthreward-to-cost ratioasymptotic analysisnormal classregular languages
0
0 comments X

The pith

The bandwidth of normal timed automata is computed as α log(1/ε) by reducing the problem to the maximum reward-to-cost ratio on a derived weighted finite graph.

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

The paper supplies an algorithm for the bandwidth of timed regular languages in the normal class, which had remained open. Normal automata are defined by bounded event frequency together with the presence of at least one non-punctual transition. The method constructs a weighted finite graph from the automaton and locates the highest reward-to-cost ratio on that graph; the bandwidth is then recovered as approximately that ratio times log(1/ε) when observation precision ε tends to zero. This finishes the algorithmic treatment of all three asymptotic classes of timed regular languages.

Core claim

We compute the bandwidth of any such automaton in the form ≈α log 1/ε. Our approach reduces this problem to computing the best reward-to-cost ratio in a weighted finite graph constructed from the given timed automaton.

What carries the argument

Reduction of asymptotic bandwidth computation to the maximum reward-to-cost ratio problem on a weighted finite graph obtained from the timed automaton.

If this is right

  • Bandwidth can now be computed algorithmically for every timed regular language.
  • The three classes meager, normal, and obese are fully separated by their bandwidth asymptotics.
  • Normal languages exhibit bandwidth that scales exactly as a constant times log(1/ε).
  • The same reduction applies uniformly to every automaton satisfying the normal-class conditions.

Where Pith is reading between the lines

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

  • The graph-reduction technique could be adapted to compute information measures for other continuous-time models that admit finite abstractions.
  • One could verify the method on families of normal automata whose bandwidths are already known by independent means.
  • The construction may reveal structural invariants that distinguish normal automata from the other two classes at the level of their underlying graphs.

Load-bearing premise

The weighted finite graph built from the timed automaton preserves the asymptotic bandwidth exactly for all non-punctual transitions and bounded-frequency behaviors.

What would settle it

A concrete normal timed automaton for which the reward-to-cost ratio extracted from the constructed graph differs from the bandwidth measured directly on the original automaton.

Figures

Figures reproduced from arXiv: 2606.11003 by Aldric Degorre, Bernardo Jacobo Incl\'an, Catalin Dima, Eugene Asarin.

Figure 1
Figure 1. Figure 1: Timed automata and their approximate bandwidths [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Pseudo-distance between two timed words (dotted arrows represent →→ [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Three normal automata 4 Bandwidth computation for normal automata 4.1 Informal discussion & three examples Intuitively, the coefficient α in the bandwidth of a normal automaton corresponds to the number of “degrees of freedom” per time unit. A degree of freedom cor￾responds to a transition for which the duration can be freely chosen in some interval. A natural idea would be to assign the reward 1 to each “… view at source ↗
Figure 4
Figure 4. Figure 4: Computing the bandwidth of A1, A2, A3 from [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗
read the original abstract

The bandwidth of a timed language characterizes the quantity of information per time unit (with a finite observation precision $\varepsilon$). The asymptotic behavior of the bandwidth as $\varepsilon \to 0$ classifies timed regular languages in three classes: meager, normal, and obese. Normal timed automata have a bounded frequency of events and some non-punctual transitions, and, up to now, were the only class of timed automata for which no algorithm was available for computing their bandwidth. In this article, we compute the bandwidth of any such automaton in the form $\approx\alpha\log{1/\varepsilon}$. Our approach reduces this problem to computing the best reward-to-cost ratio in a weighted finite graph constructed from the given timed automaton.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

1 major / 0 minor

Summary. The paper claims to complete the algorithmic computation of bandwidth for timed regular languages by handling the remaining 'normal' class of timed automata (those with bounded event frequency and non-punctual transitions). It asserts that the bandwidth takes the asymptotic form α log(1/ε) and reduces the problem to computing the maximum reward-to-cost ratio on a weighted finite graph constructed from the input timed automaton.

Significance. If the asserted reduction holds exactly, the result would finish the classification of all timed automata into meager, normal, and obese classes with effective algorithms for each, using a uniform reduction to a standard graph-theoretic optimization problem. This would be a notable contribution to the theory of timed languages and quantitative verification.

major comments (1)
  1. [Abstract] Abstract: the central claim is a reduction of the bandwidth computation to a best reward-to-cost ratio on a constructed weighted finite graph, but no construction, region encoding, or proof sketch is supplied in the provided text, so it is impossible to check whether the graph preserves the exact asymptotic coefficient α including for non-punctual transitions and bounded-frequency behaviors.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review and for highlighting the need for greater accessibility of the central construction. The full long-version manuscript contains the graph construction, region encoding, and proof; the comment appears directed at the abstract alone. We address this below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim is a reduction of the bandwidth computation to a best reward-to-cost ratio on a constructed weighted finite graph, but no construction, region encoding, or proof sketch is supplied in the provided text, so it is impossible to check whether the graph preserves the exact asymptotic coefficient α including for non-punctual transitions and bounded-frequency behaviors.

    Authors: The referee comment is labeled as applying to the Abstract. The long-version manuscript supplies the explicit construction of the weighted finite graph (via a region-based encoding of the timed automaton that tracks both clock constraints and event frequencies), together with the proof that the maximum reward-to-cost ratio on this graph equals the coefficient α for normal automata. Because the abstract is only a high-level summary, it omits these details; we will insert a short paragraph outlining the region encoding and the reduction in the revised abstract so that the central claim can be verified from the abstract alone. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper asserts a direct algorithmic reduction of bandwidth computation for normal timed automata to the standard maximum reward-to-cost ratio problem on a finite weighted graph constructed from the automaton. The abstract and provided context contain no equations, self-citations, fitted parameters, or ansatzes that reduce the claimed result back to its inputs by construction. The reduction is presented as preserving the asymptotic quantity exactly via an explicit construction, with no load-bearing reliance on prior author work or renaming of known results. This is a standard self-contained algorithmic claim.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no explicit free parameters, axioms, or invented entities. The reduction itself may rest on unstated domain assumptions about clock regions or region graphs that are standard in timed automata but cannot be audited here.

pith-pipeline@v0.9.1-grok · 5656 in / 1117 out tokens · 24029 ms · 2026-06-27T10:33:28.539169+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

31 extracted references · 19 canonical work pages

  1. [1]

    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci.126, 183– 235 (1994).https://doi.org/10.1016/0304-3975(94)90010-8

    work page doi:10.1016/0304-3975(94)90010-8 1994

  2. [2]

    In: Proc

    Asarin, E., Basset, N., B´ eal, M.P., Degorre, A., Perrin, D.: Toward a timed theory of channel coding. In: Proc. FORMATS. LNCS, vol. 7595, pp. 27–42. Springer (2012).https://doi.org/10.1007/978-3-642-33365-1_4

    work page doi:10.1007/978-3-642-33365-1_4 2012

  3. [3]

    Asarin, E., Basset, N., Degorre, A.: Entropy of regular timed languages. Inf. Com- put.241, 142–176 (2015).https://doi.org/10.1016/j.ic.2015.03.003

    work page doi:10.1016/j.ic.2015.03.003 2015

  4. [4]

    In: Proc

    Asarin, E., Basset, N., Degorre, A.: Distance on timed words and applications. In: Proc. FORMATS. LNCS, vol. 11022, pp. 199–214. Springer (2018).https: //doi.org/10.1007/978-3-030-00151-3_12

    work page doi:10.1007/978-3-030-00151-3_12 2018

  5. [5]

    In: Proc

    Asarin, E., Basset, N., Degorre, A., Perrin, D.: Generating functions of timed languages. In: Proc. MFCS. LNCS, vol. 7464, pp. 124–135. Springer (2012).https: //doi.org/10.1007/978-3-642-32589-2_14

    work page doi:10.1007/978-3-642-32589-2_14 2012

  6. [6]

    In: Proc

    Asarin, E., Degorre, A., Dima, C., Jacobo Incl´ an, B.: Bandwidth of timed au- tomata: 3 classes. In: Proc. FSTTCS. LIPIcs, vol. 284, pp. 10:1–10:17 (2023). https://doi.org/10.4230/LIPICS.FSTTCS.2023.10, full versionhttps://arxiv. org/abs/2310.01941

    work page doi:10.4230/lipics.fsttcs.2023.10 2023

  7. [7]

    In: Proc

    Asarin, E., Degorre, A., Dima, C., Jacobo Incl´ an, B.: Computing the bandwidth of meager timed automata. In: Proc. CIAA. LNCS, vol. 15015, pp. 19–34. Springer (2024).https://doi.org/10.1007/978-3-031-71112-1_2, full versionhttps:// arxiv.org/abs/2406.12694

    work page doi:10.1007/978-3-031-71112-1_2 2024

  8. [8]

    In: Reachability Problems

    Asarin, E., Degorre, A., Dima, C., Jacobo Incl´ an, B.: Weighing obese timed lan- guages. In: Reachability Problems. LNCS, vol. 16230, pp. 112–125. Springer (2026). https://doi.org/10.1007/978-3-032-09524-4_8, full versionhttps://arxiv. org/abs/2508.18133

    work page doi:10.1007/978-3-032-09524-4_8 2026

  9. [9]

    Cambridge University Press (2009).https://doi.org/10.1017/CBO9781139195768

    Berstel, J., Perrin, D., Reutenauer, C.: Codes and Automata. Cambridge University Press (2009).https://doi.org/10.1017/CBO9781139195768

    work page doi:10.1017/cbo9781139195768 2009

  10. [10]

    In: Proc

    Boja´ nczyk, M.: Factorization forests. In: Proc. DLT. LNCS, vol. 5583, pp. 1–17. Springer (2009).https://doi.org/10.1007/978-3-642-02737-6_1

    work page doi:10.1007/978-3-642-02737-6_1 2009

  11. [11]

    Formal Methods Syst

    Bouyer, P., Brinksma, E., Larsen, K.G.: Optimal infinite scheduling for multi- priced timed automata. Formal Methods Syst. Des.32(1), 3–23 (2008).https: //doi.org/10.1007/S10703-007-0043-4

    work page doi:10.1007/s10703-007-0043-4 2008

  12. [12]

    Information and Control1(2), 91 – 112 (1958).https://doi.org/10.1016/S0019-9958(58)90082-2

    Chomsky, N., Miller, G.A.: Finite state languages. Information and Control1(2), 91 – 112 (1958).https://doi.org/10.1016/S0019-9958(58)90082-2

    work page doi:10.1016/s0019-9958(58)90082-2 1958

  13. [13]

    In: Proc

    Dasdan, A., Irani, S.S., Gupta, R.K.: Efficient algorithms for optimum cycle mean and optimum cost to time ratio problems. In: Proc. DAC. pp. 37–42. ACM (1999). https://doi.org/10.1145/309847.309862

    work page doi:10.1145/309847.309862 1999

  14. [14]

    In: Proc

    Jacobo Incl´ an, B., Degorre, A., Asarin, E.: Bounded delay timed channel coding. In: Proc. FORMATS. LNCS, vol. 13465, pp. 65–79. Springer (2022).https://doi. org/10.1007/978-3-031-15839-1_4

    work page doi:10.1007/978-3-031-15839-1_4 2022

  15. [15]

    Uspekhi Matematicheskikh Nauk14(2), 3–86 (1959).https://doi.org/ 10.1090/trans2/017,http://mi.mathnet.ru/eng/umn7289

    Kolmogorov, A.N., Tikhomirov, V.M.:ε-entropy andε-capacity of sets in function spaces. Uspekhi Matematicheskikh Nauk14(2), 3–86 (1959).https://doi.org/ 10.1090/trans2/017,http://mi.mathnet.ru/eng/umn7289

    work page doi:10.1090/trans2/017 1959

  16. [16]

    Cam- bridge University Press (1995).https://doi.org/10.1017/CBO9780511626302

    Lind, D., Marcus, B.: An Introduction to Symbolic Dynamics and Coding. Cam- bridge University Press (1995).https://doi.org/10.1017/CBO9780511626302

    work page doi:10.1017/cbo9780511626302 1995

  17. [17]

    M¨ obius, A.F.: Der barycentrische Calcul. J.A. Barth., Leipzig (1827),http:// sites.mathdoc.fr/cgi-bin/oeitem?id=OE_MOBIUS__1_1_0 17

  18. [18]

    Discrete Event Dynamic Sys- tems10(1–2), 87–113 (2000).https://doi.org/10.1023/A:1008387132377

    Puri, A.: Dynamical properties of timed automata. Discrete Event Dynamic Sys- tems10(1–2), 87–113 (2000).https://doi.org/10.1023/A:1008387132377

    work page doi:10.1023/a:1008387132377 2000

  19. [19]

    The Bell System Tech- nical Journal27(3), 379–423 (1948).https://doi.org/10.1002/j.1538-7305

    Shannon, C.E.: A mathematical theory of communication. The Bell System Tech- nical Journal27(3), 379–423 (1948).https://doi.org/10.1002/j.1538-7305. 1948.tb01338.x

    work page doi:10.1002/j.1538-7305 1948

  20. [20]

    Simon, I.: Factorization forests of finite height. Theor. Comput. Sci.72(1), 65–94 (1990).https://doi.org/10.1016/0304-3975(90)90047-L 18 A Preliminaries A.1 On geometry of points, runs and words A busy reader can skip this section except its first paragraph, Def. 14 and Lem. 16 that will be used in the proof of the lower bound. A motivated reader is invi...

    work page doi:10.1016/0304-3975(90)90047-l 1990

  21. [21]

    resetting

    and thus|t 1 1−t2 1| ≤ − →d(w 1, w2)< µ/2, and the basis of induction is established. Suppose now, by inductive hypothesis, that (8) holds for somei; we want to prove it fori+ 1. There are two cases, by definition of the gap: –in polytopeP, for all pointst i+1 =t i. In this case,|t 1 i+1 −t 2 i+1|=|t 1 i −t 2 i |< µ/2, as required. –in polytopeP, for all ...

  22. [22]

    ift i −t 0 >1anda i =b(the heartbeat), mthent i =t pbi + 1; 2.t i ∈[τ+ cb i −1, τ+ cb i + 2]

  23. [23]

    ift i −t 0 > M, thenx k i =t i −t rk i

  24. [24]

    Herepb i is the index 12 of the last hearbeat event withina 1,

    wheneverr(δ ′) = 0, the duration of this transitiond i =g i(xi−1). Herepb i is the index 12 of the last hearbeat event withina 1, . . . , ai−1; alsocb i stands for the number 13 of heartbeat eventsbwithina 1, . . . , ai, andr k i for the maximalj≤isuch thatδ j resetsx k (it exists since all clocks are bounded byM). Finally,g i are polynomial functions (de...

  25. [25]

    for each non-zeroa∈O 0 (image of a route from(p 1, ℓ1)→(p 2, ℓ2)with cost and reward 0), its graph corresponds to a surjective functionℓ 1 i →ℓ 2 i for everyi

  26. [26]

    for image of a cycle from(p, ℓ)→(p, ℓ)(with cost and reward 0), its 0-orbit graph corresponds to a permutationℓ i →ℓ i for everyi

  27. [27]

    ifab=a̸= 0fora, b∈O 0, thenb= 1 ℓ for a certainℓ. Proof.1. Any vertex of active faceℓ 1 i has a successor vertex inℓ 2 i by Con- str. 2; this successor is unique (otherwise the reward would be>0). As for surjectivity, every vertex inℓ 2 i has a predecessor also by Constr. 2

  28. [28]

    A surjective function from a finite set to itself is always a permutation

  29. [29]

    Letvbe a vertex inℓ 2, vertexv ′ its predecessor viaainℓ 1, andv ′′ its successor viabinℓ 2

    Orbit graphsaandbcorrespond to some routes from (p 1, ℓ1) to (p 2, ℓ2) and from (p 2, ℓ2) to (p 2, ℓ2), respectively. Letvbe a vertex inℓ 2, vertexv ′ its predecessor viaainℓ 1, andv ′′ its successor viabinℓ 2. Sinceab=a, we have thatv ′′ =v. The only permutation graph satisfying this property for allvis 1 ℓ2. We conclude thatb= 1 ℓ2.⊓ ⊔ Definition 16.A0-...

  30. [30]

    ifs i −τ >2anda i =b, thent i ∈s pbi + [1−ε,1 +ε]; 2.s i ∈[τ+ cb i −1−ε, τ+ cb i + 2 +ε]

  31. [31]

    Note that the above constraints are relaxations of the properties in Lemma Lem

    ifs i−1 −τ > Mandr(δ ′) = 0, thens i ∈s i−1 +g i(xi−1) + [−νε−ε, νε+ε], wherex k i =s i −s rk i . Note that the above constraints are relaxations of the properties in Lemma Lem. 24. Lemma 9.The setNet fol ε (π, π′, τ)defined in Constr. 3 is anε-net for all words traces of runs following the routeπ, π ′ (starting within[τ, τ+ 1)). Proof.A wordw= (a 1, t1)....