Learning Event-recording Automata Passively

Anirban Majumdar; Jean-Fran\c{c}ois Raskin; Sayan Mukherjee

REVIEW 3 major objections 4 minor 32 references

Learning Event-recording Automata Passively

T0 review · 3 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper claims that a state-merging algorithm, LEAP, can passively learn every ERA-definable timed language from positive and negative symbolic timed words, checking each merge by SMT despite the NP-complete consistency problem.

desk verdict A genuinely new passive learner for ERA from symbolic timed words, with a plausible NP-completeness result, but the completeness theorem leans on an unproved imported lemma that may not survive the paper's own empty-word convention. read the letter →

arxiv 2508.03627 v1 pith:D3UCRPEQ submitted 2025-08-05 cs.FL

Anirban Majumdar , Sayan Mukherjee , Jean-François Raskin This is my paper · ORCID

classification cs.FL MSC 68Q4568Q3268Q17

keywords event-recordingautomatapassivelearningstate-mergingsymbolictimedwordslanguagescharacteristicsetsNP-completenessSMTsolving

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper establishes that a useful class of timed languages, those definable by Event-Recording Automata (ERA), can be learned passively from examples. LEAP, the proposed algorithm, takes positive and negative symbolic timed words—event sequences whose positions carry timing constraints—and returns an ERA that is consistent with the sample. The main theoretical claim is completeness: for every ERA-recognizable language there exist finite characteristic sample sets for which LEAP returns an ERA accepting exactly that language. Because ERA are determinizable and complementable, this opens a route to deriving timed requirement specifications from high-level scenarios rather than from raw timed execution logs.

What carries the argument

The load-bearing machinery is the state-merging loop of LEAP, adapting RPNI to the timed setting: a prefix tree over symbolic timed words, a total order that fixes which frontier node is processed next, and a fold operation that recursively merges successors after a successful merge. Each candidate merge is filtered through an SMT encoding of the intersection non-emptiness problem for an ERA and a symbolic word. For completeness, the key objects are tail languages TL(u), the set of region-word suffixes w such that u.w lies in the target language, together with a structural property of simple deterministic ERA taken from the literature: region words reaching the same state must agree, for every suffix, on whether the concatenation is satisfiable. Lemma 16 uses that property to show the set of distinct tails is finite, and the characteristic-set construction uses shortest prefixes and a kernel of one-step extensions to force LEAP to reproduce the target tails.

What would settle it

Exhibit a K-ERA-recognizable language and two region words u and v that lead to the same state of its minimal simple DERA, together with a suffix w such that exactly one of Ju.wK and Jv.wK is empty; this directly contradicts the property from [13] on which Lemma 16 and Theorem 13 depend, and a small search over ERA benchmarks could look for it.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that passive identification from symbolic timed words is complete for the class of ERA languages. LEAP starts from a prefix tree of the positive samples, then repeatedly merges a blue frontier node into a red state whenever the resulting ERA still rejects all negative words; because symbolic guards can overlap, deciding whether a merge is safe is NP-complete, and the paper encodes that decision as an SMT instance. Theorem 4 guarantees that LEAP terminates and returns an ERA consistent with the sample, while Theorem 13 guarantees that for every K-ERA-recognizable language L there is a characteristic sample set S of region words such that LEAP outputs a deterministic ERA with L(A)=L. The proof is language-theoretic: tails TL(u) of region words are shown to be finite and to determine when state merging is safe, which lets the characteristic set enforce that every merge in LEAP preserves the target language.

Load-bearing premise

The completeness proof depends on a cited structural property of event-recording automata: any two region words that lead to the same state must agree, for every possible continuation, on whether the continuation can be realised by an actual timed word; if that property fails for some ERA language, the finiteness of tails and the whole characteristic-set construction collapse.

Editorial extensions

If this is right

For every ERA-definable language, some finite sample of positive and negative region words makes LEAP return a deterministic ERA for exactly that language, so passive learning of ERA is complete in the limit from symbolic data.
Because LEAP may keep nondeterminism, it can represent some languages with exponentially fewer states than any deterministic learner; the paper demonstrates this with the L_n family, where n+2 states suffice.
The merge-consistency test is NP-complete for general symbolic words but polynomial when the samples are region words and the current automaton is deterministic, so the computational cost of LEAP depends sharply on the input representation.
No polynomial-size characteristic set built from region words can exist for all ERA languages, since the class is not polynomially learnable; the guaranteed sample sets may need to be exponential.
Working directly with symbolic zone words keeps the sample size small and insensitive to the maximal constant K, which the experiments show lets LEAP scale to benchmarks where the region-word version times out.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The tail-based completeness argument does not rely on a unique minimal automaton, so a natural extension is to adapt it to other timed model classes with a region-like canonical form, such as deterministic timed automata with resets.
A concrete test of the paper's load-bearing premise is to search ERA benchmarks for a language whose minimal simple DERA violates the same-state/same-satisfiability-tail property; if one exists, the completeness theorem fails even though the algorithm's consistency guarantee survives.
The paper's interactive use case suggests a practical measure: how few natural-language scenarios, possibly generated by a language model and vetted by an engineer, are enough for LEAP to converge to the intended ERA compared with active-learning query counts.
Scaling LEAP to large samples will hinge on the SMT encoding of merge checks; a specialised difference-constraints solver for the region-word case could avoid the exponential blowup observed when zone words are split into region words.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

This is a serious paper. The state-merging algorithm LEAP is genuinely new, the NP-completeness of intersection non-emptiness for DERA/ERA is a real contribution, and the authors back it with an SMT-based implementation and a completeness argument via characteristic sets. They also ship code and an artifact, which is more than many theory papers do. The L_n example showing succinct nondeterministic ERA over determinized versions is a nice empirical touch. If I worked on timed automata learning, I would want to know about this work.

The soft spots are real but not fatal, except one. First, Theorem 4 states the wrong direction for negative samples: it says L(A) ∩ JwK ≠ ∅ for all w ∈ S−, but the surrounding text and the merge check clearly intend empty intersection. That is an obvious typo, but it is in a theorem statement and should be fixed before publication. Second, the empirical section compares only against active learners; there is no passive baseline, and the query-count comparison is not apples-to-apples. That is defensible given that no other passive symbolic-word ERA learner exists, but the authors should acknowledge the mismatch more explicitly.

The load-bearing concern is the completeness proof. Lemma 16, which makes the characteristic-set construction finite, is proved entirely by importing Lemma 19 of [13] to assert the existence of a simple DERA where same-state regions have identical non-emptiness tails. The paper neither states nor proves that lemma, and it is fragile under the paper's convention that every empty region word (JwK = ∅) belongs to every timed language. Under that convention, two prefixes can reach the same control state with different current clock regions, yet have different tails simply because one continuation is empty (hence in the language) and the other is non-empty and rejected. I checked the concrete DERA from the stress-test note: it is small, has satisfiable accepting paths, and does exactly this. If the cited property from [13] does not hold for the ERA class as defined here, then Lemma 16, Corollary 19, and Theorem 13 all collapse. At minimum, the authors need to state and prove the imported lemma in their own setting, or modify the empty-word convention so the same-state/tail property is not vacuous.

The reduction for NP-hardness looks plausible, and the SMT encoding is standard. The citation pattern is clean: self-citations are only baselines, and the main results are not derived from the authors' own prior work.

This paper deserves a serious referee. The central algorithm and complexity result stand on their own, and the completeness proof is a genuine attempt that might be repairable. I would send it to peer review, but the reviewer report must push hard on Lemma 16 and the empty-word convention.

Referee Report

3 major / 4 minor

Summary. The paper introduces LEAP, a state-merging algorithm for passively learning event-recording automata (ERA) from positive and negative symbolic timed words. LEAP builds a prefix tree from the positive sample, then repeatedly attempts to merge frontier states with red states, allowing the merge only if the resulting automaton remains consistent with the negative sample; the consistency check is reduced to an SMT problem. The paper proves that the underlying intersection non-emptiness problem for an ERA and a symbolic word is NP-complete even for deterministic ERA, gives a polynomial case for region words, and proves a completeness result: for every ERA-recognizable language there exists a finite characteristic sample set of region words on which LEAP returns a DERA for exactly that language. An implementation is evaluated against active learning tools on several benchmarks, and an artifact is provided.

Significance. If the completeness proof is made fully rigorous, this is a solid contribution to timed automata learning. The paper provides the first passive learner for ERA from symbolic timed words, with an identification-in-the-limit guarantee for the whole ERA class, together with a clean NP-completeness result that justifies the SMT-based merge check. The authors explicitly exploit nondeterminism and symbolic (zone-like) words to obtain compact automata, and they provide an open-source implementation and an artifact. The experiments give useful evidence that handling symbolic words directly can outperform region-based splitting on practical benchmarks. The main novelty — a language-theoretic characteristic-set construction for a class without unique minimal automata — is interesting and potentially extendable.

major comments (3)

[Section 3.2, Theorem 4] Theorem 4 states the wrong side of the consistency condition for negative samples: it claims that for every w∈S−, JwK∩L(A)≠∅, whereas consistency with a negative sample requires JwK∩L(A)=∅. The proof sketch and the merge-check description on page 8 use the correct (empty) direction, so this is likely a typo, but it appears in a central statement and must be corrected.
[Section 5, Lemma 16] Lemma 16 is load-bearing for the completeness theorem: it is used to infer that the set of tails {TL(u) | u∈RW(Σ,K)} is finite, which is what makes the characteristic sets of Corollary 19 and Theorem 13 finite. The proof is not self-contained: it invokes 'Lemma 19 of [13]' without stating that lemma or proving that it applies to the definitions used here. In particular, the paper's convention that empty region words belong to every language interacts with the tail definition, and the claimed property that two region words reaching the same state have identical non-emptiness tails for all suffixes is not a formal consequence of the definitions given in the paper. A concrete DERA with K=2 illustrates the risk: let q0 go to q1 on (a, xa=0∧xb=0), let q1 go to q2 on (a, xa∈(0,1)∧xb∈(0,1)) and also on (a, xa>2∧xb>2), and let q2 go to a rejecting state on (b, xa=0∧xb∈(0,1)) and to an accepting state on (b, xa=0∧xb>2). The region words u=(a,xa=0∧xb=0)(a,xa∈(0,1)∧xb∈(0,1)) and v=(a,xa=0∧xb=0)(a,xa>2∧xb>2) both reach q2, yet for w=(b,xa=0∧xb∈(0,1)) the word u.w is non-empty and rejected while v.w is empty and hence, by the paper's convention, in L. Thus TL(u)≠TL(v) even though the two prefixes reach the same state. The authors must either state and prove the imported property for their exact SDERA notion, or give a direct proof of Lemma 16; without this, Theorem 13 is not established.
[Section 5, proof of Theorem 13] In the final paragraph of the proof of Theorem 13, the reverse inclusion L⊆L(A_n) uses the sentence 'from Lemma 26(5) we know that δn(qin,w′)=δn(qin,t′)' to conclude that two tails-equal prefixes reach the same state. Lemma 26(5), however, is stated for a pair consisting of one red and one non-red state in an intermediate automaton A_i. In the final automaton A_n all states are red, so the lemma does not apply. The needed statement is the converse direction — equal tails imply the same state for red states — which the paper neither states nor proves. Since this step is essential for the contradiction that shows w∈L(A_n), the proof of Theorem 13 is incomplete as written.

minor comments (4)

[Section 5, Lemma 11 and Corollary 12] The paper asserts that the proof of [28] for DTA 'also holds for the class of ERA, by relabeling' but gives no relabeling argument, and the step from non-polynomial learnability to the nonexistence of polynomial-size characteristic sets for LEAP is asserted without proof. This is a secondary claim, but it should be substantiated or softened.
[Section 5, Definition 15 and Remark 22] The convention that every empty region word belongs to every timed language is unusual and is central to the tail argument; it should be introduced as a formal definition, and its effect on tail languages and on the consistency of samples should be discussed explicitly.
[Section 4, Lemma 9] The proof says that checking JwK≠∅ suffices; this is correct only because the word is a region word and the automaton is complete over regions, so the path is syntactically determined. This assumption should be stated explicitly in the proof.
[Section 6, Table 1] The table compares the number of samples for passive LEAP with the number of queries for active learners. The text acknowledges the different settings, but the table would benefit from a note making explicit that the columns are not directly comparable measures of data efficiency.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the main derivation chain is self-contained, with external citations and one non-load-bearing self-citation as a baseline.

full rationale

I walked the paper's claimed derivation chain and found no step in which a prediction or first-principles result reduces by definition or by construction to its own inputs. The correctness of LEAP (Theorem 4) is established by construction: every merge is admitted only after an SMT-based check that the merged automaton remains consistent with the negative sample, and the algorithm terminates because red states are never reprocessed. The NP-completeness of the intersection non-emptiness problem is proved by an explicit reduction from 3-SAT for the lower bound and by a polynomial-time certificate check for the upper bound. The completeness argument in Section 5 is a genuine constructive argument: characteristic sets are defined from the tail languages TL(u) and the kernel N(L), and the invariants in Lemma 26 are proved by induction on the iterations of LEAP rather than by assuming the target conclusion. The one load-bearing external import is Lemma 19 of [13], used in Lemma 16 to establish finiteness of the set of tails. That is a substantive external correctness assumption, and if the property fails for the paper's definitions the completeness theorem would be at risk; however, it is not circularity, because [13] is not authored by the present authors and the property is not assumed in the statement being proved. The only self-citation is [19], which appears as a baseline tool in the experiments and as one of several citations for the standard assumption that K is known; that citation is not load-bearing for the central correctness or completeness proofs. The paper's explicit convention that empty region words belong to every timed language (Remark 22) is a definitional convenience that the paper discloses, and it does not smuggle the completeness conclusion into the premises. Accordingly, no specific circular step can be quoted, and the appropriate score is 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No numeric constants are fitted to data. The bound K and alphabet Σ are inputs assumed known, which is standard in this literature; they are listed as axioms rather than fitted parameters. The central claims rest on several external lemmas, two of which are imported with little justification.

assumptions (5)

standard math Every ERA can be transformed into an equivalent DERA (Lemma 2, after [4]).
Used to justify working with deterministic ERAs in the completeness argument and the P-time region-word result.
domain assumption For every ERA-recognizable language there exists a simple DERA where any two region words leading to the same state have identical tails (Lemma 19 of [13]).
Imported from prior work by Grinchtein, Jonsson, and Leucker; foundational for Lemma 16, which bounds the number of tails. The paper does not reprove this property.
ad hoc to paper The class of ERA is not polynomially learnable, and the proof for DTA in [28] transfers to ERA by relabeling (Lemma 11).
The transfer is asserted without a construction; Corollary 12 (no polynomial region-word characteristic sets) depends on it.
domain assumption The alphabet Σ and the maximal constant K are known inputs to LEAP and to the completeness theorem.
Stated in Section 5 as a reasonable assumption used in related active learning work [13,31,19]; without it the characteristic-set construction is not well defined.
domain assumption The input sample is consistent: no word in S+ has non-empty intersection with a word in S-.
Required for any language to separate positive and negative samples; the paper assumes this from Section 3 onward.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Learning Event-recording Automata Passively." pith.science (2026). https://pith.science/paper/D3UCRPEQ

@misc{pith2026250803627,
  author       = {Pith},
  title        = {Pith review of: Learning Event-recording Automata Passively},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/D3UCRPEQ}},
  note         = {Machine review of arXiv:2508.03627}
}

read the original abstract

This paper presents a state-merging algorithm for learning timed languages definable by Event-Recording Automata (ERA) using positive and negative samples in the form of symbolic timed words. Our algorithm, LEAP (Learning Event-recording Automata Passively), constructs a possibly nondeterministic ERA from such samples based on merging techniques. We prove that determining whether two ERA states can be merged while preserving sample consistency is an NP-complete problem, and address this with a practical SMT-based solution. Our implementation demonstrates the algorithm's effectiveness through examples. We also show that every ERA-definable language can be inferred using our algorithm with a suitable sample.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

32 extracted references · 29 canonical work pages

[13]

Learning of event-recording automata

Olga Grinchtein, Bengt Jonsson, and Martin Leucker. Learning of event-recording automata. Theor. Comput. Sci. , 411(47):4029--4054, 2010

work page 2010
[1]

Rajeev Alur, Rastislav Bod \' k, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar - Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013 , pages 1--8. IEEE , 2013

work page 2013
[2]

Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci. , 126(2):183--235, 1994

1994
[3]

Henzinger

Rajeev Alur, Tom \' a s Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. J. ACM , 43(1):116--146, 1996

work page 1996
[4]

Henzinger

Rajeev Alur, Limor Fix, and Thomas A. Henzinger. Event-clock automata: A determinizable class of timed automata. Theor. Comput. Sci. , 211(1-2):253--273, 1999

work page 1999
[5]

Learning real-time automata

Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. Learning real-time automata. Sci. China Inf. Sci. , 64(9), 2021

work page 2021
[6]

LTL reactive synthesis with a few hints

Mrudula Balachander, Emmanuel Filiot, and Jean - Fran c ois Raskin. LTL reactive synthesis with a few hints. In TACAS (2) , volume 13994 of Lecture Notes in Computer Science , pages 309--328. Springer, 2023

work page 2023
[7]

P \' e rez, Ga \" e tan Staquet, and Frits W

V \' e ronique Bruy \` e re, Bharat Garhewal, Guillermo A. P \' e rez, Ga \" e tan Staquet, and Frits W. Vaandrager. Active learning of mealy machines with timers. CoRR , abs/2403.02019, 2024

arXiv 2024

Show all 32 references

[8]

Stephen A. Cook. The complexity of theorem-proving procedures. In STOC , pages 151--158. ACM , 1971

1971
[9]

g Cornanguer, Christine Largou \

L \' e na \" g Cornanguer, Christine Largou \" e t, Laurence Roz \' e , and Alexandre Termier. TAG: learning timed automata from logs. In AAAI , pages 3949--3958. AAAI Press, 2022

2022
[10]

Incremental regular inference

Pierre Dupont. Incremental regular inference. In ICGI , volume 1147 of Lecture Notes in Computer Science , pages 222--237. Springer, 1996

1996
[11]

Mark Gold

E. Mark Gold. Language identification in the limit. Inf. Control. , 10(5):447--474, 1967

1967
[12]

Mark Gold

E. Mark Gold. Complexity of automaton identification from given data. Inf. Control. , 37(3):302--320, 1978

1978
[14]

Inference of event-recording automata using timed decision trees

Olga Grinchtein, Bengt Jonsson, and Paul Pettersson. Inference of event-recording automata using timed decision trees. In CONCUR , volume 4137 of Lecture Notes in Computer Science , pages 435--449. Springer, 2006

2006
[15]

Active learning of timed automata with unobservable resets

L \' e o Henry, Thierry J \' e ron, and Nicolas Markey. Active learning of timed automata with unobservable resets. In FORMATS , volume 12288 of Lecture Notes in Computer Science , pages 144--160. Springer, 2020

2020
[16]

A scenario-based methodology for conducting requirements elicitation

H Holbrook III. A scenario-based methodology for conducting requirements elicitation. ACM SIGSOFT Software Engineering Notes , 15(1):95--104, 1990

1990
[17]

UPPAAL in a nutshell

Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. , 1(1-2):134--152, 1997

1997
[18]

An efficient algorithm for learning event-recording automata

Shang - Wei Lin, \' E tienne Andr \' e , Jin Song Dong, Jun Sun, and Yang Liu. An efficient algorithm for learning event-recording automata. In ATVA , volume 6996 of Lecture Notes in Computer Science , pages 463--472. Springer, 2011

2011
[19]

Greybox learning of languages recognizable by event-recording automata

Anirban Majumdar, Sayan Mukherjee, and Jean - Fran c ois Raskin. Greybox learning of languages recognizable by event-recording automata. In ATVA , volume 15054 of Lecture Notes in Computer Science , pages 235--256. Springer, 2024

2024
[20]

Inferring regular languages in polynomial updated time

Jos \'e Oncina and Pedro Garcia. Inferring regular languages in polynomial updated time. In Pattern recognition and image analysis: selected papers from the IVth Spanish Symposium , pages 49--61. World Scientific, 1992

1992
[21]

Timed k-tail: Automatic inference of timed automata

Fabrizio Pastore, Daniela Micucci, and Leonardo Mariani. Timed k-tail: Automatic inference of timed automata. In ICST , pages 401--411. IEEE Computer Society, 2017

2017
[22]

Aichernig, Kim Guldstrand Larsen, and Florian Lorber

Martin Tappler, Bernhard K. Aichernig, Kim Guldstrand Larsen, and Florian Lorber. Time to learn - learning timed automata from tests. In FORMATS , volume 11750 of Lecture Notes in Computer Science , pages 216--235. Springer, 2019

2019
[23]

Aichernig, and Florian Lorber

Martin Tappler, Bernhard K. Aichernig, and Florian Lorber. Timed automata learning via SMT solving. In NFM , volume 13260 of Lecture Notes in Computer Science , pages 489--507. Springer, 2022

2022
[24]

Learning deterministic multi-clock timed automata

Yu Teng, Miaomiao Zhang, and Jie An. Learning deterministic multi-clock timed automata. In HSCC , pages 6:1--6:11. ACM , 2024

2024
[25]

Vaandrager

Frits W. Vaandrager. Model learning. Commun. ACM , 60(2):86--95, 2017

2017
[26]

Vaandrager, Masoud Ebrahimi, and Roderick Bloem

Frits W. Vaandrager, Masoud Ebrahimi, and Roderick Bloem. Learning mealy machines with one timer. Inf. Comput. , 295(Part B ):105013, 2023

2023
[27]

Vaandrager, Bharat Garhewal, Jurriaan Rot, and Thorsten Wi mann

Frits W. Vaandrager, Bharat Garhewal, Jurriaan Rot, and Thorsten Wi mann. A new approach for active automata learning based on apartness. In TACAS (1) , volume 13243 of Lecture Notes in Computer Science , pages 223--243. Springer, 2022

2022
[28]

Polynomial distinguishability of timed automata

Sicco Verwer, Mathijs de Weerdt, and Cees Witteveen. Polynomial distinguishability of timed automata. In ICGI , volume 5278 of Lecture Notes in Computer Science , pages 238--251. Springer, 2008

2008
[29]

One-clock deterministic timed automata are efficiently identifiable in the limit

Sicco Verwer, Mathijs de Weerdt, and Cees Witteveen. One-clock deterministic timed automata are efficiently identifiable in the limit. In LATA , volume 5457 of Lecture Notes in Computer Science , pages 740--751. Springer, 2009

2009
[30]

A likelihood-ratio test for identifying probabilistic deterministic real-time automata from positive data

Sicco Verwer, Mathijs de Weerdt, and Cees Witteveen. A likelihood-ratio test for identifying probabilistic deterministic real-time automata from positive data. In ICGI , volume 6339 of Lecture Notes in Computer Science , pages 203--216. Springer, 2010

2010
[31]

Active learning of deterministic timed automata with myhill-nerode style characterization

Masaki Waga. Active learning of deterministic timed automata with myhill-nerode style characterization. In CAV (1) , volume 13964 of Lecture Notes in Computer Science , pages 3--26. Springer, 2023

2023
[32]

Active learning of one-clock timed automata using constraint solving

Runqing Xu, Jie An, and Bohua Zhan. Active learning of one-clock timed automata using constraint solving. In ATVA , volume 13505 of Lecture Notes in Computer Science , pages 249--265. Springer, 2022

2022

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.

[1] [13]

Learning of event-recording automata

Olga Grinchtein, Bengt Jonsson, and Martin Leucker. Learning of event-recording automata. Theor. Comput. Sci. , 411(47):4029--4054, 2010

work page 2010

[2] [1]

Rajeev Alur, Rastislav Bod \' k, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar - Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013 , pages 1--8. IEEE , 2013

work page 2013

[3] [2]

Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci. , 126(2):183--235, 1994

1994

[4] [3]

Henzinger

Rajeev Alur, Tom \' a s Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. J. ACM , 43(1):116--146, 1996

work page 1996

[5] [4]

Henzinger

Rajeev Alur, Limor Fix, and Thomas A. Henzinger. Event-clock automata: A determinizable class of timed automata. Theor. Comput. Sci. , 211(1-2):253--273, 1999

work page 1999

[6] [5]

Learning real-time automata

Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. Learning real-time automata. Sci. China Inf. Sci. , 64(9), 2021

work page 2021

[7] [6]

LTL reactive synthesis with a few hints

Mrudula Balachander, Emmanuel Filiot, and Jean - Fran c ois Raskin. LTL reactive synthesis with a few hints. In TACAS (2) , volume 13994 of Lecture Notes in Computer Science , pages 309--328. Springer, 2023

work page 2023

[8] [7]

P \' e rez, Ga \" e tan Staquet, and Frits W

V \' e ronique Bruy \` e re, Bharat Garhewal, Guillermo A. P \' e rez, Ga \" e tan Staquet, and Frits W. Vaandrager. Active learning of mealy machines with timers. CoRR , abs/2403.02019, 2024

arXiv 2024