A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata

B. Srivathsan; Kyveli Doveri; Pierre Ganty

arxiv: 2601.15104 · v2 · submitted 2026-01-21 · 💻 cs.FL · cs.LO

A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata

Kyveli Doveri , Pierre Ganty , B. Srivathsan This is my paper

Pith reviewed 2026-05-16 11:53 UTC · model grok-4.3

classification 💻 cs.FL cs.LO

keywords Myhill-Nerode characterizationone-clock timed automataactive learningdeterministic timed automataL* algorithmhalf-integral wordsreset information

0 comments

The pith

A Myhill-Nerode characterization for one-clock deterministic timed automata accounts for varying clock resets along the same word.

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

The paper develops a Myhill-Nerode style equivalence relation that captures exactly the languages accepted by one-clock deterministic timed automata. The relation works by viewing accepted words as half-integral sequences together with the specific reset points the automaton records on them. This perspective produces a finite-index congruence even though different automata can choose different reset locations on identical input words. The resulting equivalence classes directly define the states of a canonical minimal 1-DTA. The same relation is then used to adapt Angluin's L* procedure so that the canonical automaton can be learned from membership and equivalence queries on timed words.

Core claim

We present a Myhill-Nerode style characterization for languages recognized by one-clock deterministic timed automata (1-DTA). Although there is only one clock, distinct automata may reset it differently along the same word. This adds a significant challenge in the search for a canonical automaton. Our characterization is based on a new perspective of 1-DTAs in terms of 'half-integral' words that they accept, along with the reset information encoded by them. We apply our results to develop L* style algorithms that learn the canonical 1-DTA.

What carries the argument

The Myhill-Nerode equivalence on half-integral words augmented with reset information, which induces a finite-index congruence whose classes are the states of the canonical 1-DTA.

If this is right

The equivalence classes of the new relation are exactly the states of the unique minimal 1-DTA for any given language.
An L* learner can be instantiated directly on the half-integral-word congruence to recover the canonical automaton from membership and equivalence queries.
Any language whose minimal 1-DTA exists must have finite index under this reset-augmented relation.
The learning algorithm terminates and returns the smallest deterministic one-clock automaton consistent with the observed timed words.

Where Pith is reading between the lines

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

The half-integral perspective may simplify the design of verification algorithms that must track only one clock and its resets.
Active-learning techniques developed here could be lifted to infer timing models of embedded controllers whose specifications are given by one-clock constraints.
If a similar finite encoding of multiple reset sequences can be found, the same approach might extend the Myhill-Nerode result to deterministic timed automata with two clocks.

Load-bearing premise

Reset information along words can be encoded into a finite equivalence relation that yields a canonical deterministic one-clock automaton despite the possibility of different reset points on the same word.

What would settle it

A language accepted by some 1-DTA for which the proposed equivalence relation on half-integral words with resets produces infinitely many classes would falsify the characterization.

Figures

Figures reproduced from arXiv: 2601.15104 by B. Srivathsan, Kyveli Doveri, Pierre Ganty.

**Figure 1.** Figure 1: Top: minimal acceptor for L = {(1·a)(t1 ·b)(t2 ·c) | t1 ∈ (0, 1) and t1+t2 = 1} ∪ {(t1 · d)(t2 · c) | t1 ∈ (1, 2) and t1 + t2 = 2}. Bottom: A(RL,≈L) . This example shows that A(RL,≈L) is not necessarily minimal among all acceptors. For readability, sink states are omitted from the figure, though they are always assumed to be present in our reasoning. Proof. We start by showing AT is deterministic. Consider… view at source ↗

**Figure 2.** Figure 2: Two minimal non isomorphic acceptors with different reset functions ac [PITH_FULL_IMAGE:figures/full_fig_p033_2.png] view at source ↗

**Figure 3.** Figure 3: Conjectures for Example 37. AT ′′ ϵ 0 ( 1 2 · a) ( 1 2 · a)(1 + 1 2 · a) a, x /∈ (0, 1), 0 a, 0 < x < 1, 0 a, x ≤ 1, 0 a, 1 < x, 0 a, 0 ≤ x, 0 AT ′′′ ϵ 0 ( 1 2 · a) ( 1 2 · a)(1 + 1 2 · a) ( 1 2 · a)(2 · a) a, x /∈ (0, 1), 0 a, 0 < x < 1, 0 a, x /∈ (1, 2), 0 a, 1 < x < 2, 0 a, 0 ≤ x, 0 a, 0 ≤ x, 0 [PITH_FULL_IMAGE:figures/full_fig_p039_3.png] view at source ↗

**Figure 4.** Figure 4: Conjectures for Example 39 [PITH_FULL_IMAGE:figures/full_fig_p039_4.png] view at source ↗

read the original abstract

We present a Myhill-Nerode style characterization for languages recognized by one-clock deterministic timed automata (1-DTA). Although there is only one clock, distinct automata may reset it differently along the same word. This adds a significant challenge in the search for a canonical automaton. Our characterization is based on a new perspective of 1-DTAs in terms of "half-integral" words that they accept, along with the reset information encoded by them. We apply our results to develop L* style algorithms that learn the canonical 1-DTA.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note private letter to a colleague

The paper gives a Myhill-Nerode characterization for one-clock DTAs by folding reset choices into equivalence classes over half-integral words, then builds an L* learner on top of it.

read the letter

The core advance is a Myhill-Nerode relation for one-clock deterministic timed automata that stays finite even though the same word can trigger resets at different times in different automata. They do this by re-expressing accepted words as half-integral sequences and recording the reset information those sequences carry. From there they extract a canonical automaton and an L* procedure that learns it. That combination is new; earlier timed learning work either stayed with untimed automata or did not produce a canonical one-clock form. The approach is grounded in the concrete structure of one-clock models rather than a generic trick, which is useful because one-clock automata already appear in real-time verification tools. The learning algorithm follows directly once the equivalence is shown to be finite and right-congruent, so the practical payoff is clear if the proofs hold. The obvious soft spot is exactly the finiteness claim. Distinct reset points on the same word could in principle generate infinitely many classes unless the half-integral encoding bounds them uniformly. The paper asserts that the perspective collapses those distinctions, but the argument needs to be checked for any language where reset locations can drift arbitrarily while preserving the timed language. If that step is tight, the rest is fine; if it relies on an implicit bound that does not always apply, both the characterization and the learner would need repair. No other gaps stand out from the presentation. This is for people working on automata learning or on timed-system verification who already know the one-clock restriction. A reader who needs a concrete learning procedure for this subclass will find the result directly usable. It is specific enough and formally motivated enough to merit a serious referee, even if the proofs require tightening on the finiteness side. I would send it to review.

Referee Report

2 major / 2 minor

Summary. The paper presents a Myhill-Nerode style characterization for languages recognized by one-clock deterministic timed automata (1-DTA). It introduces a perspective based on 'half-integral' words together with encoded reset information to handle the fact that distinct 1-DTAs may reset their single clock at different points along the same word. The characterization is then used to construct L*-style active learning algorithms that identify the canonical 1-DTA for a given language.

Significance. If the finiteness and canonicity arguments hold, the result supplies a missing theoretical foundation for active learning of one-clock timed automata, a model class widely used in real-time verification. The explicit handling of variable reset points via half-integral words is a technical contribution that could enable practical inference tools for timed systems.

major comments (2)

[§3] §3, Definition 3.4 and Theorem 3.7: the equivalence relation on half-integral words is claimed to be finite and to yield a canonical deterministic one-clock automaton, yet the argument that reset information can always be collapsed into finitely many classes (independent of the particular automaton) is only sketched; a concrete bound on the number of classes in terms of the number of states or the maximal constant appearing in the guards is missing.
[§5.2] §5.2, Algorithm 1 (L* learner): the termination and correctness proof relies on the Myhill-Nerode relation being of finite index, but no explicit argument shows that the observation table construction respects the half-integral word partitioning when the target automaton uses non-integral reset points; this step is load-bearing for the claim that the learned automaton is canonical.

minor comments (2)

[§3] Notation for half-integral words (e.g., the distinction between integral and half-integral suffixes) is introduced without a running example; adding a small concrete 1-DTA and its accepted half-integral words would improve readability.
[Introduction] The abstract and introduction both state that the characterization is 'parameter-free,' but the definition of the equivalence classes implicitly depends on the finite set of constants appearing in the target automaton; this should be clarified.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review. The comments identify places where the proofs can be made more explicit. We address each point below and will revise the manuscript to strengthen the arguments while preserving the original technical development.

read point-by-point responses

Referee: [§3] §3, Definition 3.4 and Theorem 3.7: the equivalence relation on half-integral words is claimed to be finite and to yield a canonical deterministic one-clock automaton, yet the argument that reset information can always be collapsed into finitely many classes (independent of the particular automaton) is only sketched; a concrete bound on the number of classes in terms of the number of states or the maximal constant appearing in the guards is missing.

Authors: We agree that the finiteness argument in the proof of Theorem 3.7 would benefit from an explicit bound. The equivalence classes correspond exactly to the states of the canonical 1-DTA; because any 1-DTA language has a finite minimal automaton, the index is finite independently of any particular automaton. To make this concrete we will add a supporting lemma stating that, for a language recognized by a 1-DTA whose guards use constants at most C, the number of equivalence classes is bounded by O(n·(2C+1)), where n is the number of states of the minimal automaton. The revised proof of Theorem 3.7 will include this bound together with a detailed argument showing how reset information is collapsed into these classes. revision: yes
Referee: [§5.2] §5.2, Algorithm 1 (L* learner): the termination and correctness proof relies on the Myhill-Nerode relation being of finite index, but no explicit argument shows that the observation table construction respects the half-integral word partitioning when the target automaton uses non-integral reset points; this step is load-bearing for the claim that the learned automaton is canonical.

Authors: The observation-table construction in Algorithm 1 is designed to query precisely the half-integral words that appear in the Myhill-Nerode relation of Section 3, thereby inheriting its finite index. Nevertheless, we acknowledge that the interaction between non-integral reset points and table consistency is not spelled out. We will insert a new lemma (Lemma 5.3) proving that any two half-integral words placed in the same row of the table produce identical future observations, even when the underlying automaton resets at non-integral times. The termination and canonicity arguments in Section 5.2 will then cite this lemma directly. revision: yes

Circularity Check

0 steps flagged

Myhill-Nerode characterization for 1-DTAs is derived independently from structural properties

full rationale

The paper defines a Myhill-Nerode equivalence on half-integral words augmented with reset information directly from the acceptance behavior of 1-DTAs. This construction yields a finite index relation that produces the canonical automaton without reducing any central claim to a fitted parameter, a self-citation chain, or a redefinition of the target language. The L* learner follows from the same equivalence classes, remaining self-contained against external benchmarks for timed regular languages.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The claim rests on the existence of a finite equivalence relation induced by half-integral words and resets; this relation is treated as a new primitive rather than derived from earlier results.

axioms (1)

domain assumption Deterministic one-clock timed automata are defined in the standard way with a single clock that can be reset on transitions.
The paper builds directly on the existing model of 1-DTA.

invented entities (1)

half-integral words no independent evidence
purpose: To represent accepted words together with the clock-reset decisions made by the automaton.
Introduced as the central new perspective for the characterization.

pith-pipeline@v0.9.0 · 5391 in / 1261 out tokens · 51806 ms · 2026-05-16T11:53:58.070593+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat recovery and embed_strictMono unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Our characterization is based on a new perspective of 1-DTAs in terms of 'half-integral' words ... along with the reset information encoded by them (Theorem 7, syntactic reset function R_L).
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

A profile (R,≈) is monotonic, L-preserving and has finite index (Def. 9, Prop. 10).

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

41 extracted references · 41 canonical work pages

[1]

A Theory of Timed Automata

Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 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]

Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: A determinizable class of timed automata. Theor. Comput. Sci.211(1-2), 253–273 (1999).https://doi. org/10.1016/S0304-3975(97)00173-4

work page doi:10.1016/s0304-3975(97)00173-4 1999
[3]

An, J., Chen, M., Zhan, B., Zhan, N., Zhang, M.: Learning one-clock timed au- tomata. In: Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. ...

work page doi:10.1007/978-3-030-45190-5_25 2020
[4]

An, J., Wang, L., Zhan, B., Zhan, N., Zhang, M.: Learning real-time automata. Sci. China Inf. Sci.64(9) (2021).https://doi.org/10.1007/S11432-019-2767-4

work page doi:10.1007/s11432-019-2767-4 2021
[5]

ACM Transactions on Embedded Computing Systems20(5s), 1–26 (2021)

An, J., Zhan, B., Zhan, N., Zhang, M.: Learning Nondeterministic Real-Time Au- tomata. ACM Transactions on Embedded Computing Systems20(5s), 1–26 (2021). https://doi.org/10.1145/3477030

work page doi:10.1145/3477030 2021
[6]

Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987).https://doi.org/10.1016/0890-5401(87)90052-6

work page doi:10.1016/0890-5401(87)90052-6 1987
[7]

Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Formal Methods for the Design of Real-Time Systems, International School on For- mal Methods for the Design of Computer, Communication and Software Sys- tems, SFM-RT 2004, Revised Lectures. Lecture Notes in Computer Science, vol. 3185, pp. 200–236. Springer, Bertinoro, Italy (2004).https://d...

work page 2004
[8]

In: RP’17: Proc

Bhave, D., Guha, S.: Adding Dense-Timed Stack to Integer Reset Timed Au- tomata. In: RP’17: Proc. 11th International Conference on Reachability Prob- lems. LNCS, vol. 10506, pp. 9–25. Springer, London, United Kingdom (2017). https://doi.org/10.1007/978-3-319-67089-8_2

work page doi:10.1007/978-3-319-67089-8_2 2017
[9]

CoRRabs/2403.02019(2024).https: //doi.org/10.48550/ARXIV.2403.02019 1-DTA: Myhill-Nerode characterization and active learning 19

Bruy` ere, V., Garhewal, B., P´ erez, G.A., Staquet, G., Vaandrager, F.W.: Active learning of mealy machines with timers. CoRRabs/2403.02019(2024).https: //doi.org/10.48550/ARXIV.2403.02019 1-DTA: Myhill-Nerode characterization and active learning 19

work page doi:10.48550/arxiv.2403.02019 2024
[10]

In 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Doveri, K., Ganty, P., Srivathsan, B.: A myhill-nerode style characterization for timed automata with integer resets. In: 44th IARCS Annual Conference on Founda- tions of Software Technology and Theoretical Computer Science, FSTTCS 2024. LIPIcs, vol. 323, pp. 21:1–21:18. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Infor- matik, Gandhinagar, Gujarat, India (2...

work page doi:10.4230/lipics 2024
[11]

Theoretical Computer Science411(47), 4029–4054 (2010).https://doi.org/10

Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theoretical Computer Science411(47), 4029–4054 (2010).https://doi.org/10. 1016/j.tcs.2010.07.008

work page 2010
[12]

In: FoSSaCS’04: Proc

Maler, O., Pnueli, A.: On Recognizable Timed Languages. In: FoSSaCS’04: Proc. of the Int. Conf. on Foundations of Software Science and Computation Structures. LNCS, vol. 2987, pp. 348–362. Springer, Barcelona, Spain (2004).https://doi. org/10.1007/978-3-540-24727-2_25

work page doi:10.1007/978-3-540-24727-2_25 2004
[13]

In: LICS’04: Proc

Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: Closing a decidability gap. In: LICS’04: Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science. pp. 54–63. IEEE, Turku, Finland (2004).https: //doi.org/10.1109/LICS.2004.1319600

work page doi:10.1109/lics.2004.1319600 2004
[14]

In: FORMATS’08: Proc

Suman, P.V., Pandya, P.K., Krishna, S.N., Manasa, L.: Timed Automata with In- teger Resets: Language Inclusion and Expressiveness. In: FORMATS’08: Proc. of the Int. Conf. on Formal Modeling and Analysis of Timed Systems. vol. 5215, pp. 78–92. Springer, Saint-Malo, France (2008).https://doi.org/10.1007/ 978-3-540-85778-5_7

work page 2008
[15]

Vaandrager, F.W., Ebrahimi, M., Bloem, R.: Learning mealy machines with one timer. Inf. Comput.295(Part A), 105013 (2023).https://doi.org/10.1016/J. IC.2023.105013

work page doi:10.1016/j 2023
[16]

In: CAV’23: Proc

Waga, M.: Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization. In: CAV’23: Proc. of the 35th Int. Conf. on Computer Aided Verification. LNCS, vol. 13964, pp. 3–26. Springer, Paris, France (2023). https://doi.org/10.1007/978-3-031-37706-8_1

work page doi:10.1007/978-3-031-37706-8_1 2023
[17]

In: Bouajjani, A., Hol´ ık, L., Wu, Z

Xu, R., An, J., Zhan, B.: Active learning of one-clock timed automata using con- straint solving. In: Bouajjani, A., Hol´ ık, L., Wu, Z. (eds.) Automated Technol- ogy for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13505, pp. 249–265. Springer...

work page doi:10.1007/978-3-031-19992-9_16 2022
[18]

ifr= 0, then add (p i, q0, a, ϕ, r) for all copiesp i,

work page
[19]

⊓ ⊔ Proposition (10).For an acceptorA, the profile(R A,≈ A)is monotonic, L(A)-preserving and has finite index

else, from all copiesp i ofp, add an outgoing transition (p i, qJϕK, a, ϕ, r). ⊓ ⊔ Proposition (10).For an acceptorA, the profile(R A,≈ A)is monotonic, L(A)-preserving and has finite index. Proof.Finite-index of≈ A comes from finiteness of the set of states. ForKthe maximum constant ofAC(K) holds, thusK (RA,≈A) ≤Kis finite. Therefore, (RA,≈ A) has finite ...

work page
[20]

Replace every large stateqby a new state q

work page
[21]

Replace every transition (p, q, a, K < x,1)∈Twherepis small andqis large, by a transition (p, q, a, K < x,0)

work page
[22]

Replace every transition (s, s ′, a, K < x,1)∈Twheresands ′ are large by a transition ( s, s′, a,0≤x,0)

work page
[23]

x < K” are enabled. Moreover, such transitions allow all time delays. 1-DTA: Myhill-Nerode characterization and active learning 23 Thus, such a “large

Replace every resetting transition (q, p, a, K < x,0)∈Twhereqis large by a transition ( q, p, a,0≤x,0). We define the initial state ofBto beq I and its accepting states to be all the statespand psuch thatp∈F. This modification removes all transitions of the form (p, q, a, K < x,1) and only adds resetting transitions with target states of region{0}. Thus,B...

work page
[24]

Replace every critical stateqby a new state qand remove all the transitions associated toq

work page
[25]

For every stateps.t.region(p) = (i, i+ 1) form≤iadd a copy p

work page
[26]

For every transition (p, q, a, x=m,1)∈Twherepis good andqis critical add a transition (p, q, a, x=m,0)

work page
[27]

For every transition (s, s ′, a, x=m,1)∈Twheresands ′ are critical add a transition (s, s′, a, x= 0,0)

work page
[28]

For every transition (s, s ′, a, ϕ,1)∈Ts.t.region(s)∈ {[m] ≡K } ∪ {[(i, i+ 1)]≡K |m≤i}andJϕK= (c, c+ 1) for somem≤cadd a transition (s, s′, a, c−m < x < c−m+ 1,1)

work page
[29]

critical portion

For every transition (s, s ′, a, ϕ,0)∈Ts.t.region(s)∈ {[m] ≡K } ∪ {[(i, i+ 1)]≡K |m≤i}add a transition ( s, s′, a,modify(ϕ),0) where, modify(ϕ) =    c−m < x < c−m+ 1 ifϕisc < x < c+ 1 K−c < xifϕisK < x x=c−melse (ϕisx=c). Finally, we define the initial state ofBto beq I and its accepting states to be all the statespand psuch thatp∈F. We introduced no...

work page
[30]

Fort 2, we consider two numbers 1− {x+t 1}and 1− {t 1}and compare the relation of{t 2}with these numbers

Consider the order between{t 1}and 1− {x}: if{t 1}= 1− {x}, then set{t ′ 1}= 1− {x ′}; if{t 1}<1− {x}, choose 1-DTA: Myhill-Nerode characterization and active learning 25 a value for{t ′ 1}between 0 and 1− {x ′}; else choose a value in the interval (1− {x ′},1). Fort 2, we consider two numbers 1− {x+t 1}and 1− {t 1}and compare the relation of{t 2}with the...

work page
[31]

In particular, sinceA (RL,≈L) is a strict acceptor (henceR L(1·a) = 0) it has at least six states

Thus,u andvcannot be sent to the same state. In particular, sinceA (RL,≈L) is a strict acceptor (henceR L(1·a) = 0) it has at least six states. The top automaton in Fig. 1 acceptsLwith five states (including the sink). Therefore,A (RL,≈L) is not minimal. Fig. 2 shows two minimal acceptors for the same language with different reset functions. Even when the...

work page
[32]

Similarly, there is (t 2 ·a)∈Σ K such that:row(s 2(t2 ·a)) =row(s ′ 2),g=ϕ K(r(s 2) +t 2) andd 2 = 0 ifr(s ′

= 0 and,d 1 = 1 otherwise. Similarly, there is (t 2 ·a)∈Σ K such that:row(s 2(t2 ·a)) =row(s ′ 2),g=ϕ K(r(s 2) +t 2) andd 2 = 0 ifr(s ′

work page
[33]

Sinceϕ K(r(s 1)+t1) =ϕ K(r(s 2)+t2) we haves1+t1 ≡K s2+t2

= 0 and, d2 = 1 otherwise. Sinceϕ K(r(s 1)+t1) =ϕ K(r(s 2)+t2) we haves1+t1 ≡K s2+t2. Ifs 1 +t 1 ≤Kthenr(s 1) +t 1 ≡K r(s 2) +t 2 impliesr(s 1) +t 1 =r(s 2) +t 2 since each boundedK-region contains exactly one half-integral value. Since r(s 1) =r(s 2) we thus deducet 1 =t 2. Then by consistency (a) we deduce row(s1(t1 ·a)) =row(s 2(t2 ·a)), thusrow(s ′

work page
[34]

Ifs 1 +t 1 > Kthen by consistency (b)row(s 1(t1 ·a)) =row(s 1(K+ 1 2 ·a)) and similarlyrow(s 2(t2 ·a)) = row(s2(K+ 1 2 ·a))

=row(s ′ 2). Ifs 1 +t 1 > Kthen by consistency (b)row(s 1(t1 ·a)) =row(s 1(K+ 1 2 ·a)) and similarlyrow(s 2(t2 ·a)) = row(s2(K+ 1 2 ·a)). By consistency (a)row(s 1(K+ 1 2 ·a)) =row(s 2(K+ 1 2 ·a)). Hence,row(s 1(t1 ·a)) =row(s 2(t2 ·a)), thusrow(s ′

work page
[35]

Since the re- set informationd 1 only depends on [r(s ′ 1)]≡K and similarlyd 2 only depends on [r(s′ 2)]≡K,row(s ′

=row(s ′ 2). Since the re- set informationd 1 only depends on [r(s ′ 1)]≡K and similarlyd 2 only depends on [r(s′ 2)]≡K,row(s ′

work page
[36]

Since for every staterow(s) we haveregion(row(s)) = [r(s)] ≡K,A T is easily seen to be an acceptor

impliesd 1 =d 2. Since for every staterow(s) we haveregion(row(s)) = [r(s)] ≡K,A T is easily seen to be an acceptor. Finally, sinceTis valid,R AT :R ≥0 →[0, K]\N >0. The last part of the proposition is proven by an easy induction on the length of words inS. G Smart Teacher Algorithm – Additional Material Lemma 36.The next closed, consistent, valid OT obta...

work page
[37]

(0,0) ( 1 2 ·a)(1 + 1 2 ·a) (1,0) (0,0) (0·a) (0,0) (0,0) (0·a)( 1 2 ·a) (0,0) (0,0) (0·a)( 1 2 ·a)(1 + 1 2 ·a) (0,0) (0,0) ⋆ (0,0) (0,0) Algorithm 2:Learning a strict acceptor with a Smart Teacher Output:A strictK L-acceptorA T such thatL(A T ) =L 1(K, S, E)←(0,{ϵ},{ϵ}); 2whiletruedo 3T ←(K, S, E, T);// buildTfromS,EandK 4ifTis not closed or not consiste...

work page
[38]

Therefore, we add|Σ K||E|new cells and for each one them we need to chose whether we reset or not

After an application of action 1 we add|Σ K|new extensions and each one of them is a|E|-dimensional vector. Therefore, we add|Σ K||E|new cells and for each one them we need to chose whether we reset or not. Thus, the width of the branching is at most 2 |ΣK ||E|

work page
[39]

For every s∈S∪SΣ K we need to assign a value toT(s,(t·a)e)(2)

After an application of action 2 we add a new column (t·a)e. For every s∈S∪SΣ K we need to assign a value toT(s,(t·a)e)(2). Since for every s∈S, we should haveT(s,(t·a)e) =T(s(t·a), e), choice only happens for s∈SΣ K. Hence, the width of the branching is at most 2 |S||ΣK |

work page
[40]

Thus, the width of the branching is at most 2 2|S||E|

After increasing the constant (action 3 or 4) we add 2|S|new extensions. Thus, the width of the branching is at most 2 2|S||E|

work page
[41]

never-resetting

After processing a counterexample we add at mostm2 m(1 +|Σ K|) toS∪ SΣK. Hence, the width of the branching is at most 2 m2m(1+|ΣK |)|E|. Hence, the branching degree of the tree isO(2H 2m2m|Σ|). Finally, we find that the total number of membership queries in an execution isO(2 H 3m2m|Σ|H 3m2m|Σ|) and the number of processed OTs isO(2 H 3m2m|Σ|H).⊓ ⊔ 1-DTA:...

work page

[1] [1]

A Theory of Timed Automata

Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 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]

Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: A determinizable class of timed automata. Theor. Comput. Sci.211(1-2), 253–273 (1999).https://doi. org/10.1016/S0304-3975(97)00173-4

work page doi:10.1016/s0304-3975(97)00173-4 1999

[3] [3]

An, J., Chen, M., Zhan, B., Zhan, N., Zhang, M.: Learning one-clock timed au- tomata. In: Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. ...

work page doi:10.1007/978-3-030-45190-5_25 2020

[4] [4]

An, J., Wang, L., Zhan, B., Zhan, N., Zhang, M.: Learning real-time automata. Sci. China Inf. Sci.64(9) (2021).https://doi.org/10.1007/S11432-019-2767-4

work page doi:10.1007/s11432-019-2767-4 2021

[5] [5]

ACM Transactions on Embedded Computing Systems20(5s), 1–26 (2021)

An, J., Zhan, B., Zhan, N., Zhang, M.: Learning Nondeterministic Real-Time Au- tomata. ACM Transactions on Embedded Computing Systems20(5s), 1–26 (2021). https://doi.org/10.1145/3477030

work page doi:10.1145/3477030 2021

[6] [6]

Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987).https://doi.org/10.1016/0890-5401(87)90052-6

work page doi:10.1016/0890-5401(87)90052-6 1987

[7] [7]

Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Formal Methods for the Design of Real-Time Systems, International School on For- mal Methods for the Design of Computer, Communication and Software Sys- tems, SFM-RT 2004, Revised Lectures. Lecture Notes in Computer Science, vol. 3185, pp. 200–236. Springer, Bertinoro, Italy (2004).https://d...

work page 2004

[8] [8]

In: RP’17: Proc

Bhave, D., Guha, S.: Adding Dense-Timed Stack to Integer Reset Timed Au- tomata. In: RP’17: Proc. 11th International Conference on Reachability Prob- lems. LNCS, vol. 10506, pp. 9–25. Springer, London, United Kingdom (2017). https://doi.org/10.1007/978-3-319-67089-8_2

work page doi:10.1007/978-3-319-67089-8_2 2017

[9] [9]

CoRRabs/2403.02019(2024).https: //doi.org/10.48550/ARXIV.2403.02019 1-DTA: Myhill-Nerode characterization and active learning 19

Bruy` ere, V., Garhewal, B., P´ erez, G.A., Staquet, G., Vaandrager, F.W.: Active learning of mealy machines with timers. CoRRabs/2403.02019(2024).https: //doi.org/10.48550/ARXIV.2403.02019 1-DTA: Myhill-Nerode characterization and active learning 19

work page doi:10.48550/arxiv.2403.02019 2024

[10] [10]

In 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Doveri, K., Ganty, P., Srivathsan, B.: A myhill-nerode style characterization for timed automata with integer resets. In: 44th IARCS Annual Conference on Founda- tions of Software Technology and Theoretical Computer Science, FSTTCS 2024. LIPIcs, vol. 323, pp. 21:1–21:18. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Infor- matik, Gandhinagar, Gujarat, India (2...

work page doi:10.4230/lipics 2024

[11] [11]

Theoretical Computer Science411(47), 4029–4054 (2010).https://doi.org/10

Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theoretical Computer Science411(47), 4029–4054 (2010).https://doi.org/10. 1016/j.tcs.2010.07.008

work page 2010

[12] [12]

In: FoSSaCS’04: Proc

Maler, O., Pnueli, A.: On Recognizable Timed Languages. In: FoSSaCS’04: Proc. of the Int. Conf. on Foundations of Software Science and Computation Structures. LNCS, vol. 2987, pp. 348–362. Springer, Barcelona, Spain (2004).https://doi. org/10.1007/978-3-540-24727-2_25

work page doi:10.1007/978-3-540-24727-2_25 2004

[13] [13]

In: LICS’04: Proc

Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: Closing a decidability gap. In: LICS’04: Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science. pp. 54–63. IEEE, Turku, Finland (2004).https: //doi.org/10.1109/LICS.2004.1319600

work page doi:10.1109/lics.2004.1319600 2004

[14] [14]

In: FORMATS’08: Proc

Suman, P.V., Pandya, P.K., Krishna, S.N., Manasa, L.: Timed Automata with In- teger Resets: Language Inclusion and Expressiveness. In: FORMATS’08: Proc. of the Int. Conf. on Formal Modeling and Analysis of Timed Systems. vol. 5215, pp. 78–92. Springer, Saint-Malo, France (2008).https://doi.org/10.1007/ 978-3-540-85778-5_7

work page 2008

[15] [15]

Vaandrager, F.W., Ebrahimi, M., Bloem, R.: Learning mealy machines with one timer. Inf. Comput.295(Part A), 105013 (2023).https://doi.org/10.1016/J. IC.2023.105013

work page doi:10.1016/j 2023

[16] [16]

In: CAV’23: Proc

Waga, M.: Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization. In: CAV’23: Proc. of the 35th Int. Conf. on Computer Aided Verification. LNCS, vol. 13964, pp. 3–26. Springer, Paris, France (2023). https://doi.org/10.1007/978-3-031-37706-8_1

work page doi:10.1007/978-3-031-37706-8_1 2023

[17] [17]

In: Bouajjani, A., Hol´ ık, L., Wu, Z

Xu, R., An, J., Zhan, B.: Active learning of one-clock timed automata using con- straint solving. In: Bouajjani, A., Hol´ ık, L., Wu, Z. (eds.) Automated Technol- ogy for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13505, pp. 249–265. Springer...

work page doi:10.1007/978-3-031-19992-9_16 2022

[18] [18]

ifr= 0, then add (p i, q0, a, ϕ, r) for all copiesp i,

work page

[19] [19]

⊓ ⊔ Proposition (10).For an acceptorA, the profile(R A,≈ A)is monotonic, L(A)-preserving and has finite index

else, from all copiesp i ofp, add an outgoing transition (p i, qJϕK, a, ϕ, r). ⊓ ⊔ Proposition (10).For an acceptorA, the profile(R A,≈ A)is monotonic, L(A)-preserving and has finite index. Proof.Finite-index of≈ A comes from finiteness of the set of states. ForKthe maximum constant ofAC(K) holds, thusK (RA,≈A) ≤Kis finite. Therefore, (RA,≈ A) has finite ...

work page

[20] [20]

Replace every large stateqby a new state q

work page

[21] [21]

Replace every transition (p, q, a, K < x,1)∈Twherepis small andqis large, by a transition (p, q, a, K < x,0)

work page

[22] [22]

Replace every transition (s, s ′, a, K < x,1)∈Twheresands ′ are large by a transition ( s, s′, a,0≤x,0)

work page

[23] [23]

x < K” are enabled. Moreover, such transitions allow all time delays. 1-DTA: Myhill-Nerode characterization and active learning 23 Thus, such a “large

Replace every resetting transition (q, p, a, K < x,0)∈Twhereqis large by a transition ( q, p, a,0≤x,0). We define the initial state ofBto beq I and its accepting states to be all the statespand psuch thatp∈F. This modification removes all transitions of the form (p, q, a, K < x,1) and only adds resetting transitions with target states of region{0}. Thus,B...

work page

[24] [24]

Replace every critical stateqby a new state qand remove all the transitions associated toq

work page

[25] [25]

For every stateps.t.region(p) = (i, i+ 1) form≤iadd a copy p

work page

[26] [26]

For every transition (p, q, a, x=m,1)∈Twherepis good andqis critical add a transition (p, q, a, x=m,0)

work page

[27] [27]

For every transition (s, s ′, a, x=m,1)∈Twheresands ′ are critical add a transition (s, s′, a, x= 0,0)

work page

[28] [28]

For every transition (s, s ′, a, ϕ,1)∈Ts.t.region(s)∈ {[m] ≡K } ∪ {[(i, i+ 1)]≡K |m≤i}andJϕK= (c, c+ 1) for somem≤cadd a transition (s, s′, a, c−m < x < c−m+ 1,1)

work page

[29] [29]

critical portion

For every transition (s, s ′, a, ϕ,0)∈Ts.t.region(s)∈ {[m] ≡K } ∪ {[(i, i+ 1)]≡K |m≤i}add a transition ( s, s′, a,modify(ϕ),0) where, modify(ϕ) =    c−m < x < c−m+ 1 ifϕisc < x < c+ 1 K−c < xifϕisK < x x=c−melse (ϕisx=c). Finally, we define the initial state ofBto beq I and its accepting states to be all the statespand psuch thatp∈F. We introduced no...

work page

[30] [30]

Fort 2, we consider two numbers 1− {x+t 1}and 1− {t 1}and compare the relation of{t 2}with these numbers

Consider the order between{t 1}and 1− {x}: if{t 1}= 1− {x}, then set{t ′ 1}= 1− {x ′}; if{t 1}<1− {x}, choose 1-DTA: Myhill-Nerode characterization and active learning 25 a value for{t ′ 1}between 0 and 1− {x ′}; else choose a value in the interval (1− {x ′},1). Fort 2, we consider two numbers 1− {x+t 1}and 1− {t 1}and compare the relation of{t 2}with the...

work page

[31] [31]

In particular, sinceA (RL,≈L) is a strict acceptor (henceR L(1·a) = 0) it has at least six states

Thus,u andvcannot be sent to the same state. In particular, sinceA (RL,≈L) is a strict acceptor (henceR L(1·a) = 0) it has at least six states. The top automaton in Fig. 1 acceptsLwith five states (including the sink). Therefore,A (RL,≈L) is not minimal. Fig. 2 shows two minimal acceptors for the same language with different reset functions. Even when the...

work page

[32] [32]

Similarly, there is (t 2 ·a)∈Σ K such that:row(s 2(t2 ·a)) =row(s ′ 2),g=ϕ K(r(s 2) +t 2) andd 2 = 0 ifr(s ′

= 0 and,d 1 = 1 otherwise. Similarly, there is (t 2 ·a)∈Σ K such that:row(s 2(t2 ·a)) =row(s ′ 2),g=ϕ K(r(s 2) +t 2) andd 2 = 0 ifr(s ′

work page

[33] [33]

Sinceϕ K(r(s 1)+t1) =ϕ K(r(s 2)+t2) we haves1+t1 ≡K s2+t2

= 0 and, d2 = 1 otherwise. Sinceϕ K(r(s 1)+t1) =ϕ K(r(s 2)+t2) we haves1+t1 ≡K s2+t2. Ifs 1 +t 1 ≤Kthenr(s 1) +t 1 ≡K r(s 2) +t 2 impliesr(s 1) +t 1 =r(s 2) +t 2 since each boundedK-region contains exactly one half-integral value. Since r(s 1) =r(s 2) we thus deducet 1 =t 2. Then by consistency (a) we deduce row(s1(t1 ·a)) =row(s 2(t2 ·a)), thusrow(s ′

work page

[34] [34]

Ifs 1 +t 1 > Kthen by consistency (b)row(s 1(t1 ·a)) =row(s 1(K+ 1 2 ·a)) and similarlyrow(s 2(t2 ·a)) = row(s2(K+ 1 2 ·a))

=row(s ′ 2). Ifs 1 +t 1 > Kthen by consistency (b)row(s 1(t1 ·a)) =row(s 1(K+ 1 2 ·a)) and similarlyrow(s 2(t2 ·a)) = row(s2(K+ 1 2 ·a)). By consistency (a)row(s 1(K+ 1 2 ·a)) =row(s 2(K+ 1 2 ·a)). Hence,row(s 1(t1 ·a)) =row(s 2(t2 ·a)), thusrow(s ′

work page

[35] [35]

Since the re- set informationd 1 only depends on [r(s ′ 1)]≡K and similarlyd 2 only depends on [r(s′ 2)]≡K,row(s ′

=row(s ′ 2). Since the re- set informationd 1 only depends on [r(s ′ 1)]≡K and similarlyd 2 only depends on [r(s′ 2)]≡K,row(s ′

work page

[36] [36]

Since for every staterow(s) we haveregion(row(s)) = [r(s)] ≡K,A T is easily seen to be an acceptor

impliesd 1 =d 2. Since for every staterow(s) we haveregion(row(s)) = [r(s)] ≡K,A T is easily seen to be an acceptor. Finally, sinceTis valid,R AT :R ≥0 →[0, K]\N >0. The last part of the proposition is proven by an easy induction on the length of words inS. G Smart Teacher Algorithm – Additional Material Lemma 36.The next closed, consistent, valid OT obta...

work page

[37] [37]

(0,0) ( 1 2 ·a)(1 + 1 2 ·a) (1,0) (0,0) (0·a) (0,0) (0,0) (0·a)( 1 2 ·a) (0,0) (0,0) (0·a)( 1 2 ·a)(1 + 1 2 ·a) (0,0) (0,0) ⋆ (0,0) (0,0) Algorithm 2:Learning a strict acceptor with a Smart Teacher Output:A strictK L-acceptorA T such thatL(A T ) =L 1(K, S, E)←(0,{ϵ},{ϵ}); 2whiletruedo 3T ←(K, S, E, T);// buildTfromS,EandK 4ifTis not closed or not consiste...

work page

[38] [38]

Therefore, we add|Σ K||E|new cells and for each one them we need to chose whether we reset or not

After an application of action 1 we add|Σ K|new extensions and each one of them is a|E|-dimensional vector. Therefore, we add|Σ K||E|new cells and for each one them we need to chose whether we reset or not. Thus, the width of the branching is at most 2 |ΣK ||E|

work page

[39] [39]

For every s∈S∪SΣ K we need to assign a value toT(s,(t·a)e)(2)

After an application of action 2 we add a new column (t·a)e. For every s∈S∪SΣ K we need to assign a value toT(s,(t·a)e)(2). Since for every s∈S, we should haveT(s,(t·a)e) =T(s(t·a), e), choice only happens for s∈SΣ K. Hence, the width of the branching is at most 2 |S||ΣK |

work page

[40] [40]

Thus, the width of the branching is at most 2 2|S||E|

After increasing the constant (action 3 or 4) we add 2|S|new extensions. Thus, the width of the branching is at most 2 2|S||E|

work page

[41] [41]

never-resetting

After processing a counterexample we add at mostm2 m(1 +|Σ K|) toS∪ SΣK. Hence, the width of the branching is at most 2 m2m(1+|ΣK |)|E|. Hence, the branching degree of the tree isO(2H 2m2m|Σ|). Finally, we find that the total number of membership queries in an execution isO(2 H 3m2m|Σ|H 3m2m|Σ|) and the number of processed OTs isO(2 H 3m2m|Σ|H).⊓ ⊔ 1-DTA:...

work page