Learning One-Clock Timed Automata
Jie An1() , Mingshuai Chen2,3,4 , Bohua Zhan3,4 ,Naijun Zhan3,4() , and Miaomiao Zhang1()TACAS

Artifact

Evaluation
2020
Accepted1

School of Software Engineering, Tongji University, Shanghai, China{1510796,miaomiao}@tongji.edu.cn
2
Lehrstuhl für Informatik 2, RWTH Aachen University, Aachen, Germany
chenms@cs.rwth-aachen.de3
State Key Lab. of Computer Science, Institute of Software, CAS, Beijing, China{bzhan,znj}@ios.ac.cn
4University of Chinese Academy of Sciences, Beijing, China

Abstract. We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework of Angluin’sL∗ algorithm and inspired by existing work on the active learning of symbolic
automata. Due to the need of guessing for each transition whether it resets theclock, the algorithm is of exponential complexity in the size of the learned automata. Before presenting this algorithm, we propose a simpler version where theteacher is assumed to be smart in the sense of being able to provide the reset
information. We show that this simpler setting yields a polynomial complexity of
the learning process. Both of the algorithms are implemented and evaluated ona collection of randomly generated examples. We furthermore demonstrate thesimpler algorithm on the functional speciﬁcation of the TCP protocol.
Keywords: Automaton learning · Active learning · One-clock timed automata ·Timed language · Reset-logical-timed language.

1

Introduction

In her seminal work [10], Angluin introduced the L∗ algorithm for learning a regular language from queries and counterexamples within a query-answering framework.
The Angluin-style learning therefore is also termed active learning or query learning,which is distinguished from passive learning, i.e., generating a model from a given data
set. Following this line of research, an increasing number of efﬁcient active learning
methods (cf. [38]) have been proposed to learn, e.g., Mealy machines [34,30], I/O automata [2], register automata [25,1,15], nondeterministic ﬁnite automata [12], Büchi
automata [19,28], symbolic automata [29,18,11] and Markov decision processes [36],to name just a few. Full-ﬂedged libraries, tools and applications are also available for
automata-learning tasks [13,27,20,21].
This work has been partially funded by NSFC under grant No. 61625206, 61972284, 61732001
and 61872341, by the ERC Advanced Project FRAPPANT under grant No. 787914, and by
the CAS Pioneer Hundred Talents Program under grant No. Y9RC585036.

c The Author(s) 2020

A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 444–462, 2020.
https://doi.org/10.1007/978-3-030-45190-5_ 25

Learning One-Clock Timed Automata

445

For real-time systems where timing constraints play a key role, however, learninga formal model is much more complicated. As a classical model for real-time systems,
timed automata [4] have an inﬁnite set of timed actions. This yields a fundamental
difference to ﬁnite automata featuring ﬁnite alphabets. Moreover, it is difﬁcult to detect
resets of clock variables from observable behaviors of the system. This makes learning
formal models of timed systems a challenging yet interesting problem.
Various attempts have been carried out in the literature on learning timed models,
which can be classiﬁed into two tracks. The ﬁrst track pursues active learning methods,
e.g. [22] for learning event-recording automata (ERA) [5] and [9] for learning real-time
automata (RTA) [17]. ERA are time automata where, for every untimed action a, a clock
is used to record the time of the last occurrence of a. The underlying learning algorithm[22], however, is prohibitively complex due to too many degrees of freedom and multiple
clocks for recording events. RTA are a class of special timed automata with one clock
to record the execution time of each action by resetting at the starting. The other track
pursues passive learning. In [42,41], an algorithm was proposed to learn deterministic
RTA. The basic idea is that the learner organizes a tree sketching traces of the data
set while merging nodes of the tree following a certain heuristic function. A passive
learning algorithm for timed automata with one clock was further proposed in [39,40].
A common weakness of passive learning methods is that the generated model merely
accepts all positive traces while it rejects all negative ones for the given set of traces,
without guaranteeing that it is a correct model of the target system. A theoretical result
was established in [40] showing it is possible to obtain the target system by continuously enriching the data set, however the number of iterations is unknown. In addition,
the passive learning methods cited above concern only discrete-time semantics of theunderlying timed models, i.e., the clock takes values from non-negative integers. We
furthermore refer the readers to [14,32] for learning specialized forms of practical timed
systems in a passive manner, [37] for passively learning timed automata using genetic
programming which scales to automata of large sizes, [33] for learning probabilistic
real-time automata incorporating clustering techniques in machine learning, and [36]for L∗ -based learning of Markov decision processes with testing and sampling.
In this paper, we present the ﬁrst active learning method for deterministic one-clock
timed automata (DOTAs) under continuous-time semantics1 . Such timed automata provide simple models while preserving adequate expressiveness, and therefore have been
widely used in practical real-time systems [35,3,16]. We present our approach in two
steps. First, we describe a simpler algorithm, under the assumption that the teacher issmart in the sense of being able to provide information about clock resets in membership and equivalence queries. The basic idea is as follows. We deﬁne the reset-logicaltimed language of a DOTA and show that the timed languages of two DOTAs are equivalent if their reset-logical-timed languages are equivalent, which reduces the learning
problem to that of learning a reset-logical-timed language.Then we show how to learn
the reset-logical-timed language following Maler and D’Antoni’s learning algorithms
for symbolic automata [29,18]. We claim the correctness, termination and polynomial
complexity of this learning algorithm. Next, we extend this algorithm to the case of anormal teacher. The main difference is that the learner now needs to guess the reset
1

The proposed learning method applies trivially to discrete-time semantics too.

446

J. An et al.

information on transitions discovered in the observation table. Due to these guesses,
the latter algorithm features exponential complexity in the size of the learned automata.
The proposed learning methods are implemented and evaluated on randomly generated
examples. We also demonstrate the simpler, polynomial algorithm on a practical casestudy concerning the functional speciﬁcation of the TCP protocol. Detailed proofs fortheorems and lemmas in this paper can be found in Appendix A of the full version [7].
In what follows, Sect. 2 provides preliminary deﬁnitions on one-clock timed automata. The learning algorithm with a smart teacher is presented and analyzed in Sect. 3.
We then present the situation with a normal teacher in Sect. 4. The experimental results
are reported in Sect. 5. Finally, Sect. 6 concludes this paper.

2

Preliminaries

Let R≥0 and N be the set of non-negative reals and natural numbers, respectively, and B
the Boolean set. We use  to stand for true and ⊥ for false. The projection of an n-tuple
x onto its ﬁrst two components is denoted by Π{1,2} x, which extends to a sequence oftuples as Π{1,2} (x1 , . . . , xk ) = Π{1,2} x1 , . . . , Π{1,2} xk .
Timed automata [4], a kind of ﬁnite automata extended with a ﬁnite set of realvalued clocks, are widely used to model real-time systems. In this paper, we consider
a subclass of timed automata with a single clock, termed one-clock timed automata(OTAs). Let c be the clock variable, denote by Φc the set of clock constraints of theform φ ::=  | c  m | φ ∧ φ, where m ∈ N and  ∈ {=, <, >, ≤, ≥}.
Deﬁnition 1 (One-clock timed automata). A one-clock timed automaton A = (Σ, Q,
q0 , F, c, Δ), where Σ is a ﬁnite set of actions, called the alphabet; Q is a ﬁnite set of
locations; q0 ∈ Q is the initial location; F ⊆ Q is a set of accepting locations; c is theunique clock; and Δ ⊆ Q × Σ × Φc × B × Q is a ﬁnite set of transitions.
A transition δ = (q, σ, φ, b, q  ) allows a jump from the source location q to thetarget location q  by performing the action σ ∈ Σ if the constraint φ ∈ Φc is satisﬁed.
Meanwhile, clock c is reset to zero if b = , and remains unchanged otherwise.
A clock valuation is a function ν : c → R≥0 that assigns a non-negative real number
to the clock. For t ∈ R≥0 , let ν + t be the clock valuation with (ν + t)(c) = ν(c) + t.
According to the deﬁnitions of clock valuation and clock constraint, a transition guard
can be represented as an interval whose endpoints are in N∪{∞}. For example, φ1 : c <5 ∧ c ≥ 3 is represented as [3, 5), φ2 : c = 6 as [6, 6], and φ3 :  as [0, ∞). We will use
the inequality- and interval-representation interchangeably in this paper.
A state s of A is a pair (q, ν), where q ∈ Q and ν is a clock valuation. A run
t1 ,σ1t2 ,σ2tn ,σnρ of A is a ﬁnite sequence ρ = (q0 , ν0 ) −−−→ (q1 , ν1 ) −−−→ · · · −−−→ (qn , νn ),where ν0 (c) = 0, ti ∈ R≥0 stands for the time delay spending on qi−1 before δi =(qi−1 , σi , φi , bi , qi ) ∈ Δ is taken, only if (1) νi−1 +ti satisﬁes φi , (2) νi (c) = νi−1 (c)+ti if bi = ⊥, otherwise νi (c) = 0, for all 1 ≤ i ≤ n. A run ρ is accepting if qn ∈ F .
The trace of a run ρ is a timed word, denoted by trace(ρ). trace(ρ) = if ρ =t1 ,σ1t2 ,σ2(q0 , ν0 ), and trace(ρ) = (σ1 , t1 )(σ2 , t2 ) · · · (σn , tn ) if ρ = (q0 , ν0 ) −−−→ (q1 , ν1 ) −−−→
tn ,σn· · · −−−→ (qn , νn ). Since ti is the time delay on qi−1 , for 1 ≤ i ≤ n, such a timed

Learning One-Clock Timed Automata

447

word is also called delay-timed word. The corresponding reset-delay-timed word canbe deﬁned as tracer (ρ) = (σ1 , t1 , b1 )(σ2 , t2 , b2 ) · · · (σn , tn , bn ), where bi is the reset
indicator for δi , for 1 ≤ i ≤ n. If ρ is an accepting run of A, trace(ρ) is called an accepting timed word. The recognized timed language of A is the set of accepting delay-timed
words, i.e., L(A) = {trace(ρ) | ρ is an accepting run of A}. The recognized reset-timed
language Lr (A) is deﬁned as {tracer (ρ) | ρ is an accepting run of A}.
The delay-timed word ω = (σ1 , t1 )(σ2 , t2 ) · · · (σn , tn ) is observed outside, fromthe view of the global clock. On the other hand, the behavior can also be observed
inside, from the view of the local clock. This results in a logical-timed word of the form
γ = (σ1 , μ1 )(σ2 , μ2 ) · · · (σn , μn ) with μi = ti if i = 1 ∨ bi−1 =  and μi = μi−1 + ti
otherwise. We will denote the mapping from delay-timed words to logical-timed words
above by Γ .
Similarly, we introduce reset-logical-timed word γr = (σ1 , μ1 , b1 )(σ2 , μ2 , b2 ) · · ·(σn , μn , bn ) as the counterpart of ωr = (σ1 , t1 , b1 )(σ2 , t2 , b2 ) · · · (σn , tn , bn ) in termsof the local clock. Without any substantial change, we can extend the mapping Γ to map
reset-delay-timed words to reset-logical-timed words. The recognized logical-timed
language of A is given as L(A) = {Γ (trace(ρ)) | ρ is an accepting run of A}, andthe recognized reset-logical-timed language of A as Lr (A) = {Γ (tracer (ρ)) | ρ is anaccepting run of A}.
An OTA is a deterministic one-clock timed automaton (DOTA) if there is at mostone run for a given delay-timed word. In other words, for any location q ∈ Q and actionσ ∈ Σ, the guards of transitions outgoing from q labelled with σ are disjoint subsets ofR≥0 . We say a DOTA is complete if for any of its location q ∈ Q and action σ ∈ Σ,
the corresponding guards form a partition of R≥0 . This means any given delay-timed
word has exactly one run. Any DOTA A can be transformed into a complete DOTA
(referred to as COTA) A accepting the same timed language as follows: (1) Augment Q
with a “sink” location qs which is not an accepting location; (2) For every q ∈ Q andσ ∈ Σ, if there is no outgoing transition from q labelled with σ, introduce a (resetting)transition from q to qs with label σ and guard [0, ∞); (3) Otherwise, let S be the subsetof R≥0 not covered by the guards of transitions from q with label σ. Write S as a unionof intervals I1 , . . . , Ik in a minimal way, then introduce a (resetting) transition from q
to qs with label σ and guard Ij for each 1 ≤ j ≤ k.
From now on, we therefore assume that we are working with COTAs.
Example 1. Fig. 1 depicts the transformation of a DOTA A (left part) into a COTA A(right part). First, a non-accepting “sink” location qs is introduced. Second, we introduce three fresh transitions (marked in blue) from q1 to qs as well as transitions fromqs to itself. At last, for location q0 and label a, the existing guards cover (1, 3), withcomplement [0, 1] ∪ [3, ∞). Hence, we introduce transitions (q0 , a, [0, 1], , qs ) and(q0 , a, [3, ∞), , qs ). Two fresh transitions from q1 to qs are introduced similarly.

3

Learning from a Smart Teacher

In this section, we consider the case of learning a COTA A with a smart teacher. Ourlearning algorithm relies on the following reduction of the equivalence over timed languages to that of reset-logical timed languages.

448

J. An et al.
b, [2, 4), b, [0, ∞), ,1

q1a, [0, ∞), 

q1

], 

), 

a, (1, 3), ⊥

,∞

q0

[0
a,

start

b, [2, 4), [3a,b, [0, ∞), a, (1, 3), ⊥

q0

a,
[
b, 0, ∞
[0, 2 ), 
),
b,

[4
,∞
),


start

qs

b, [0, ∞), Fig. 1: A DOTA A on the left and the corresponding COTA A on the right. The initial location isindicated by ‘start’ and an accepting location is doubly circled.

Theorem 1. Given two DOTAs A and B, if Lr (A) = Lr (B), then L(A) = L(B).
Theorem 1 assures that Lr (H) = Lr (A) implies L(H) = L(A), that is, to construct
a COTA A that recognizes a target timed language L = L(A), it sufﬁces to learn a hypothesis H which recognizes the same reset-logical timed language. For equivalence
queries, instead of checking directly whether Lr (H) = Lr (A), the contraposition ofTheorem 1 guarantees that we can perform equivalence queries over their timed counterparts: if L(H) = L(A), then H recognizes the target language already; otherwise, acounterexample making L(H) = L(A) yields an evidence also for Lr (H) = Lr (A).
We now describe the behavior of the teacher who keeps an automaton A to be learnt,
while providing knowledge about the automaton by answering membership and equivalence queries through an oracle she maintains. For the membership query, the teacher
receives a logical-timed word γ and returns whether γ is in L(A). In addition, she issmart enough to return the reset-logical-timed word γr that corresponds to γ (the exact correspondence is described in Sect. 3.1). For the equivalence query, the teacher isgiven a hypothesis H and decides whether L(H) = L(A). If not, she is smart enoughto return a reset-delayed-timed word ωr as a counterexample. The usual case where ateacher can deal with only standard delay-timed words will be discussed in Sect. 4.
Remark 1. The assumption that the teacher can respond with timed words coupled withreset information is reasonable, in the sense that the learner can always infer and detect
the resets of the logical clock by referring to a global clock on the wall, as long as he canobserve running states of A, i.e., observing the clock valuation of the system wheneveran event happens therein. This conforms with the idea of combining automata learningwith white-box techniques, as exploited in [24], providing that in many application
scenarios source code is available for the analysis.
In what follows, we elaborate the learning procedure including membership queries,
hypotheses construction, equivalence queries and counterexample processing.
3.1

Membership query

In our setting, the oracle maintained by the smart teacher can be regarded as a COTA
A that recognizes the target timed language L, and thereby its logical-timed language
L(A) and reset-logical-timed counterpart Lr (A). In order to collect enough information

Learning One-Clock Timed Automata

449

for constructing a hypothesis, the learner makes membership queries as “Is the logicaltimed word γ in L(A)?”. If there does not exist a run ρ such that Γ (trace(ρ)) = γ,meaning that there is some k such that the run is blocked after the k’th action (i.e.
γ is invalid) and hence the teacher gives a negative answer, associated with a resetlogical-timed word γr where all bi ’s with i > k are set to ; If there exists a run ρ(which is unique due to the determinacy of A) that admits γ (i.e., γ is valid), the teacher
answers “Yes”, if ρ is accepting, or “No” otherwise, while in both cases providing thecorresponding reset-logical-timed word γr , with Π{1,2} γr = γ.
For the sake of simplicity, we deﬁne a function π that maps a logical-timed word toits unique reset-logical-timed counterpart in membership queries. Information gatheredfrom the membership queries is stored in a timed observation table deﬁned as follows.
Deﬁnition 2 (Timed observation table). A timed observation table for a COTA A is a
7-tuple T = (Σ, Σ, Σr , S, R, E, f ) where Σ is the ﬁnite alphabet; Σ = Σ × R≥0
is the inﬁnite set of logical-timed actions; Σr = Σ × R≥0 × B is the inﬁnite set ofreset-logical-timed actions; S, R ⊂ Σr∗ and E ⊂ Σ ∗ are ﬁnite sets of words, where S
is called the set of preﬁxes, R the boundary, and E the set of sufﬁxes. Speciﬁcally,– S and R are disjoint, i.e., S ∪ R = S  R;
– The empty word is by default both a preﬁx and a sufﬁx, i.e., ∈ E and ∈ S;
– f : (S ∪ R) · E → {−, +} is a classiﬁcation function such that for a reset-logicaltimed word γr , γr ·e ∈ (S ∪R)·E, f (γr ·e) = − if Π{1,2} γr ·e is invalid, otherwise/ L(A), f (γr · e) = −, and f (γr · e) = + if Π{1,2} γr · e ∈ L(A).
if Π{1,2} γr · e ∈Given a table T, we deﬁne row : S ∪ R → (E → {+, −}) as a function mapping
each γr ∈ S ∪ R to a vector indexed by e ∈ E, each of whose components is deﬁned
as f (γr · e), denoting a potential location.
Before constructing a hypothesis H based on the timed observation table T, thelearner has to ensure that T satisﬁes the following conditions:– Reduced: ∀s, s ∈ S : s = s implies row (s) = row (s );– Closed: ∀r ∈ R, ∃s ∈ S : row (s) = row (r);– Consistent: ∀γr , γr  ∈ S ∪ R, row (γr ) = row (γr  ) implies row (γr · σr ) =row (γr  · σr  ), for all σr , σr  ∈ Σr satisfying γr · σr , γr  · σr  ∈ S ∪ R andΠ{1,2} σr = Π{1,2} σr  ;– Evidence-closed: ∀s ∈ S and ∀e ∈ E, the reset-logical-timed word π(Π{1,2} s · e)belongs to S ∪ R;
– Preﬁx-closed: S ∪ R is preﬁx-closed.
A timed observation table T is prepared if it satisﬁes the above ﬁve conditions. To
get the table prepared, the learner can perform the following operations:
Making T closed. If T is not closed, there exists r ∈ R such that for all s ∈ S
row (r) = row (s). The learner thus can move such r from R to S. Moreover, eachreset-logical-timed word π(Π{1,2} r · σ) needs to be added to R, where σ = (σ, 0) forall σ ∈ Σ. Such an operation is important since it guarantees that at every location all
actions in Σ are enabled, while specifying a clock valuation of these actions, despitethat some invalid logical-timed words might be involved. Particularly, giving a bottom
value 0 as the clock valuation satisﬁes the precondition of the partition functions thatwill be described in Sect. 3.2.

450

J. An et al.

Making T consistent. If T is not consistent, one inconsistency is resolved by adding
σ · e to E, where σ and e can be determined as follows. T being inconsistent implies
that there exist two reset-logical-timed words γr , γr  ∈ S ∪ R at least, such that γr ·σr , γr  · σr  ∈ S ∪ R and Π{1,2} σr = Π{1,2} σr  for some σr , σr  ∈ Σr , withrow (γr ) = row (γr  ) but row (γr · σr ) = row (γr  · σr  ). So, let σ = Π{1,2} σr =
Π{1,2} σr  and e ∈ E such that f (γr σr · e) = f (γr  σr  · e). Thereafter, the learnerﬁlls the table by making membership queries. Note that this operation keeps the set E
of sufﬁxes being a set of logical-timed words.
Making T evidence-closed. If T is not evidence-closed, then the learner needs to add
all preﬁxes of π(Π{1,2} s · e) to R for every s ∈ S and e ∈ E, except those already in
S ∪ R. Similarly, the learner needs to ﬁll the table through membership queries.
The condition that a timed observation table T is reduced and preﬁx-closed is inherently preserved by the aforementioned operations, together with the counterexample
processing described later in Sect. 3.3. Furthermore, a table may need several rounds ofthese operations before being prepared (cf. Algorithm 1), since certain conditions may
be violated by different, interleaved operations.
3.2

Hypothesis construction

As soon as the timed observation table T is prepared, a hypothesis can be constructedin two steps, i.e., the learner ﬁrst builds a DFA M based on the information in T, andthen transforms M to a hypothesis H, which will later be shown as a COTA.
Given a prepared timed observation table T = (Σ, Σ, Σr , S, R, E, f ), a DFA
0, FM ) can be built as follows:
M = (QM , ΣM , ΔM , qM
– the ﬁnite set of locations QM = {qrow (s) | s ∈ S};
0= qrow () for ∈ S;
– the initial location qM– the set of accepting locations FM = {qrow (s) | f (s · ) = + for s ∈ S and ∈ E};– the ﬁnite alphabet ΣM = {σr ∈ Σr | γr · σr ∈ S ∪ R for γr ∈ Σr∗ };– the ﬁnite set of transitions ΔM = {(qrow (γr ) , σr , qrow (γr ·σr ) ) | γr · σr ∈ S ∪R for γr ∈ Σr∗ and σr ∈ Σr }.
The constructed DFA M is compatible with the timed observation table T in thesense captured by the following lemma.
Lemma 1. For a prepared timed observation table T = (Σ, Σ, Σr , S, R, E, f ), for0, FM ) accepts
every γr ·e ∈ (S ∪R)·E, the constructed DFA M = (QM , ΣM , ΔM , qM
π(Π{1,2} γr · e) if and only if f (γr · e) = +.
The learner then transforms the DFA M to a hypothesis H = (Σ, Q, q0 , F, c, Δ),0with Q = QM , q0 = qM
, F = FM , c being the clock and Σ the given alphabet as in T.
The set of transitions Δ in H can be constructed as follows: For any q ∈ QM and σ ∈Σ, let Ψq,σ = {μ | (q, (σ, μ, b), q  ) ∈ ΔM }, then applying the partition function P c (·)(deﬁned below) to Ψq,σ returns k intervals, written as I1 , · · · , Ik , satisfying μi ∈ Ii forany 1 ≤ i ≤ k, where k = |Ψq,σ |; consequently, for every (q, (σ, μi , bi ), q  ) ∈ ΔM , afresh transition δi = (q, σ, Ii , bi , q  ) is added to Δ.

Learning One-Clock Timed Automata
T5 −(a, 1.1, ⊥) +(a, 0, ) −(b, 0, ) −(a, 1.1, ⊥)(a, 0, ) −(a, 1.1, ⊥)(b, 0, ) −(a, 1.1, ⊥)(b, 2, ) +(a, 3, ) −(a, 0, )start(a, 3, )q−(b, 0, )(a, 1.1, ⊥)(a, 0, )M5(b, 0, )(b, 2, )a, [0, 1], 
q+

start

a, [3, ∞), q−b, [0, ∞), 451b, [2, ∞), a, (1, 3), ⊥q+a, [0, ∞), H5b, [0, 2), 

Fig. 2: The prepared timed observation table T5 , the corresponding DFA M5 and hypothesis H5 .

Deﬁnition 3 (Partition function). Given a list of clock valuations  = μ0 , μ1 , · · · , μnwith 0 = μ0 < μ1 · · · < μn , and μi  = μj  if μi , μj ∈ R≥0 \ N and i = j forall 1 ≤ i, j ≤ n, let μn+1 = ∞, then a partition function P c (·) mapping  to a set ofintervals {I0 , I1 , . . . , In }, which is a partition of R≥0 , is deﬁned as⎧[μi , μi+1 ),⎪⎪⎪⎨(μ , μ ),
i
i+1
Ii =
⎪[μi , μi+1 ],⎪⎪⎩(μi , μi+1 ],if μi ∈ N ∧ μi+1 ∈ N;if μi ∈ R≥0 \ N ∧ μi+1 ∈ N;if μi ∈ N ∧ μi+1 ∈ R≥0 \ N;if μi ∈ R≥0 \ N ∧ μi+1 ∈ R≥0 \ N.

Remark 2. Deﬁnition 3 is adapted from that in [18] by imposing additional assumptionsof the list of clock valuations in order to guarantee μi ∈ Ii , for any 0 ≤ i ≤ n, due to theunderlying continuous-time semantics. Whereas, by T being prepared and the normalization function described in Sect. 3.3, the set of clock valuations Ψq,σ can be arranged
into a list q,σ = μ0 , μ1 , . . . , μn satisfying such assumptions given in Deﬁnition 3 forany q ∈ QM and σ ∈ Σ.
Example 2. Suppose A in Fig. 1 recognizes the target timed language. Then the prepared table T5 , the corresponding DFA M5 and hypothesis H5 are depicted in Fig. 2.
Here, the subscript 5 indicates the ﬁfth iteration of T (Details concerning the constructions and the entire learning process are enclosed in Appendix B of [7].).
0
Lemma 2. Given a DFA M = (QM , ΣM , δM , qM
, FM ), which is generated from aprepared timed observation table T, the hypothesis H = (Σ, Q, q0 , F, c, Δ) is transformed from M. For all γr · e ∈ (S ∪ R) · E, H accepts the reset-logical-timed word
π(Π{1,2} γr · e) iff f (γr · e) = +.

Theorem 2. The hypothesis H is a COTA.
Given a clock valuation μ, we denote the region containing μ as μ, deﬁned asμ = [μ, μ] if μ ∈ N, and μ = (μ, μ + 1) otherwise. The following theorem
establishes the compatibility of the constructed hypothesis H with the timed observationtable T.
Theorem 3. For γr ·e ∈ (S ∪R)·E, let π(Π{1,2} γr ·e) = (σ1 , μ1 , b1 ) · · · (σn , μn , bn ).
Then for every μi ∈ μi , the hypothesis H accepts the reset-logical-timed word γr =(σ1 , μ1 , b1 ) · · · (σn , μn , bn ) if f (γr · e) = +, and cannot accept it if f (γr · e) = −.

452

3.3

J. An et al.

Equivalence query and counterexample processing

Suppose that the teacher knows a COTA A which recognizes the target timed language
L. Then to answer an equivalence query is to determine whether L(H) = L(A), which
can be divided into two timed language inclusion problems, i.e., whether L(H) ⊆L(A) and L(A) ⊆ L(H). Most decision procedures for language inclusion proceedby complementation and emptiness checking of the intersection [23]: L(A) ⊆ L(B) iff
L(A) ∩ L(B) = ∅. The fact that deterministic timed automata can be complemented [6]enables solving the inclusion problem by checking the emptiness of the resulted productautomata H×A and H×A. The complementation technique, however, does not apply tonondeterministic timed automata even if with only one single clock [4], which we plan
to incorporate in our learning framework in future work. We therefore opt for2 the alternative method presented by Ouaknine and Worrell in [31] showing that the language
inclusion problem of timed automata with one clock (regardless of their determinacy)
is decidable by reduction to a reachability problem on an inﬁnite graph. That is, there
exists a delay-timed word ω that leads to a bad conﬁguration if L(H)  L(A). In detail, the corresponding run ρ of ω ends in an accepting location in H but the counterpartρ of ω in A is not accepting. Consequently, the teacher can provide the reset-delaytimed word ωr resulted from ω as a negative counterexample ctx − . Similarly, a positive counterexample ctx + = (ωr , +) can be generated if L(A)  L(H). An algorithm
elaborating the equivalence query is provided in Appendix C of the full version [7].
When receiving a counterexample ctx = (ωr , +/−), the learner ﬁrst converts it toa reset-logical-timed word γr = Γ (ωr ) = (σ1 , μ1 , b1 )(σ2 , μ2 , b2 ) · · · (σn , μn , bn ). By
deﬁnition, γr and ωr share the same sequence of transitions in A. Furthermore, by thecontraposition of Theorem 1, γr is an evidence for Lr (H) = Lr (A) if ωr is an evidence
for L(H) = L(A).
Additionally, by the deﬁnition of clock constraints Φc , at any location, if an action σ
is enabled, i.e., its guard is satisﬁed, w.r.t. the clock value μ ∈ R≥0 \N, then σ should beenabled w.r.t. any clock value μ+θ at the location, where θ ∈ (0, 1). Speciﬁcally, only
one transition is available for σ at the location on the interval μ, because the target
automaton is deterministic. Therefore, in order to avoid unnecessarily distinguishingtimed words and violating the assumptions of the list  for the partition function, thelearner needs to apply a normalization function g to normalize γr .
Deﬁnition 4 (Normalization). A normalization function g maps a reset-logical-timed
word γr = (σ1 , μ1 , b1 )(σ2 , μ2 , b2 ) · · · (σn , μn , bn ) to another reset-logical-timed word
by resetting any logical clock to its integer part plus a constant fractional part, i.e.,g(γr ) = (σ1 , μ1 , b1 )(σ2 , μ2 , b2 ) · · · (σn , μn , bn ), where μi = μi if μi ∈ N, μi = μi +θ for some ﬁxed constant θ ∈ (0, 1) otherwise.
We will instantiate θ = 0.1 in what follows. Clearly our approach works for any
other θ valued in (0, 1). This normalization process guarantees the assumptions needed
for Deﬁnition 3.
2

Remark that the learning complexity (Sect. 3.5) is measured in terms of the number of queriesrather than the time complexity of the speciﬁc method for checking the equivalence (nor membership). Additionally, the speciﬁc method of equivalence checking is not the main concern.

Learning One-Clock Timed Automata
T5 −(a, 1.1, ⊥) +(a, 0, ) −(b, 0, ) −(a, 1.1, ⊥)(a, 0, ) −(a, 1.1, ⊥)(b, 0, ) −(a, 1.1, ⊥)(b, 2, ) +(a, 3, ) −ωr =(a,0,)(a,1.3,),−==============⇒
γr =(a,0,)(a,1.3,)T6 
−(a, 1.1, ⊥) +(a, 0, ) −(b, 0, ) −(a, 1.1, ⊥)(a, 0, ) −(a, 1.1, ⊥)(b, 0, ) −(a, 1.1, ⊥)(b, 2, ) +(a, 3, ) −(a, 0, )(a, 1.3, ) −(a, 3, )(a, 0, )
start

q−

(b, 0, )453(b, 2, )(a, 1.3, )(a, 1.1, ⊥)q+(a, 0, )M6(b, 0, )

Fig. 3: An illustration of the necessity of normalization by the normalization function.

Algorithm 1: Learning one-clock timed automaton with a smart teacher
input : the timed observation table T = (Σ, Σ, Σr , S, R, E, f ).
output: the hypothesis H recognizing the target language L.
1 S ← {}; R ← {Γ (ω) | ω = (σ, 0), ∀σ ∈ Σ}; E ← {} ;// initialization
2 ﬁll T by membership queries;
3 equivalent ← ⊥;4 while equivalent = ⊥ do
5prepared ← is prepared(T) ;// whether the table is prepared6
while prepared = ⊥ do
7
if T is not closed then make closed(T) ;8
if T is not consistent then make consistent(T) ;9
if T is not evidence-closed then make evidence closed(T) ;10
prepared ← is prepared(T);
11
12
13
14
15
16

M ← build DFA(T) ;H ← build hypothesis(M) ;equivalent, ctx ← equivalence query(H);if equivalent = ⊥ thenctx processing(T, ctx ) ;// transforming T to a DFA M// constructing a hypothesis H from M// counterexample processing

return H;

Example 3. Consider the prepared table T5 in Fig. 3 (as in Fig. 2). When the leaner asks
an equivalence query with hypothesis H5 , the teacher answers that L(H5 ) = L(A),where A in Fig. 1 is the target automaton, and provides a counterexample (ωr , −) withωr = (a, 0, )(a, 1.3, ), which can be transformed to a reset-logical-timed word γr =(a, 0, )(a, 1.3, ). If he adds preﬁxes of γr to the table directly, the learner will get a
prepared table T6 and thus construct a DFA M6 . Unfortunately, the partition function
deﬁned in Deﬁnition 3 is not applicable to (a, 1.3, ) and (a, 1.1, ⊥) any more. On
the other hand, if he adds the preﬁxes of the normalized reset-logical-timed word, i.e.,γr = (a, 0, )(a, 1.1, ), to T5 , the learner will then get an inconsistent table whose
consistency can be retrieved by the operation of “making T consistent” as expected.
The following theorem guarantees that the normalized reset-logical-timed word γr
is also an evidence for Lr (H) = Lr (A). Therefore, the learner can use it as a counterexample and thus adds all the preﬁxes of γr to R except those already in S ∪ R.
Theorem 4. Given a valid reset-logical-timed word γr of A, its normalization γr =g(γr ) shares the same sequence of transitions in A.
3.4

Learning algorithm

We present in Algorithm 1 the learning procedure integrating all the previously statedingredients, including preparing the table, membership and equivalence queries, hypothesis construction and counterexample processing. The learner ﬁrst initializes the454

J. An et al.

timed observation table T = (Σ, Σ, Σr , S, R, E, f ), where S = { }, E = { },while for every σ ∈ Σ, he builds a logical-timed word γ = (σ, 0) and then obtains
its reset counterpart π(γ) = (σ, 0, b) by triggering a membership query to the teacher,which is then added to R. Thereafter, the learner can ﬁll the table by additional membership queries. Before constructing a hypothesis, the learner performs several roundsof operations described in Sect. 3.1 until T is prepared. Then, a hypothesis H is constructed leveraging an intermediate DFA M and submitted to the teacher for an equivalence query. If the answer is positive, H recognizes the target language. Otherwise, thelearner receives a counterexample ctx and then conducts the counterexample processing to update T as described in Sect. 3.3. The whole procedure repeats until the teacher
gives a positive answer to an equivalence query.
To facilitate the analysis of correctness, termination and complexity of Algorithm 1,
we introduce the notion of symbolic state that combines each location with its clock
regions: a symbolic state of a COTA A = (Σ, Q, q0 , F, c, Δ) is a pair (q, μ), whereq ∈ Q and μ is a region containing μ. If κ is the maximal constant appearing in
the clock constraints of A, then there exist 2κ + 2 such regions, including [n, n] with0 ≤ n ≤ κ, (n, n+1) with 0 ≤ n < κ, and (κ, ∞) for each location, so there are a totalof |Q| × (2κ + 2) symbolic states. Then the correctness and termination of Algorithm 1is stated in the following theorem, based on the fact that there is an injection from S (orequivalently, the locations of H) to symbolic states of A.
Theorem 5. Algorithm 1 terminates and returns a COTA H which recognizes the target
timed language L.
3.5

Complexity

Given a target timed language L which is recognized by a COTA A, let n = |Q| be thenumber of locations of A, m = |Σ| the size of the alphabet, and κ the maximal constantappearing in the clock constraints of A. In what follows, we derive the complexity of
Algorithm 1 in terms of the number of queries.
By the proof of Theorem 5, H has at most n(2κ + 2) locations ( the size of S) distinguished by E. Thus, |E| is at most n(2κ + 2) in order to distinguish these locations.
Therefore, the number of transitions of H is bounded by mn2 (2κ + 2)3 . Furthermore,as every counterexample adds at least one fresh transition to the hypothesis H, where
we consider each interval of the partition corresponds to a transition, this means thatthe number of counterexamples and equivalence queries is at most mn2 (2κ + 2)3 .
Now, we consider the number of membership queries, that is, to compute (|S| +|R|) × |E|. Let h be the maximal length of counterexamples returned by the teacher,which is polynomial in the size of A according to Theorem 5 in [40], bounded by
n2 . There are three cases of extending R by adding fresh rows, namely during theprocessing of counterexamples, making T closed, and making T evidence-closed. The
ﬁrst case adds at most hmn2 (2κ + 2)3 rows to R, while the latter two add at mostn(2κ + 2) × m and n2 (2κ + 2)2 , respectively, yielding that the size of R is bounded byO(hmn2 κ3 ), where O(·) is the big Omicron notation. As a consequence, the number ofmembership queries is bounded by O(mn5 κ4 ). So, the total complexity is O(mn5 κ4 ).

Learning One-Clock Timed Automata

455

It is worth noting the above analysis is given in the worst case, where all partitions
need to be fully reﬁned. But, in practice we can learn the automaton without reﬁning
most partitions, and therefore the number of equivalence and membership queries, aswell as the number of locations in the learned automaton are much fewer than the corresponding worst-case bounds. This will be demonstrated by examples in Sect. 5.
3.6

Accelerating Trick

In the timed observation table, the function f maps invalid reset-logical-timed words aswell as certain valid ones to “−” when the teacher maintains a COTA A as the oracle.
The learner thus needs multiple rounds of queries to distinguish the “sink” location fromother unaccepting locations. If the function f is extended to map invalid reset-logicaltimed words to a distinct symbol, say “×”, when we let a DOTA A be the oracle, thenthe learner will take much fewer queries. We will later show in the experiments thatsuch a trick signiﬁcantly accelerates the learning process.

4

Learning from a Normal Teacher

In this section, we consider the problem of learning timed automata with a normal
teacher. As before, we assume the timed language to be learned comes from a complete
DOTA. For the normal teacher, inputs to membership queries are delay-timed words,
and the teacher returns whether the word is in the language (without giving any additional information). Inputs to equivalence queries are candidate DOTAs, and the teacher
either answers they are equivalent or provides a delay-timed word as a counterexample.
The algorithm here is based on the procedure in the previous section. We still maintain observation tables where the elements in S ∪ R are reset-logical-timed words andthe elements in E are logical-timed words. In order to obtain delay-timed words for themembership queries, we need to guess clock reset information for transitions in the table. More precisely, in order to convert a logical-timed word to a delay-timed word, it isnecessary to know clock reset information for all but the last transition. Hence, it is necessary to guess reset information for each word in S ∪ R (since S ∪ R is preﬁx-closed,
this is equivalent to guessing reset information for the last transition of each word).
Also, for each entry in (S ∪ R) × E, it is necessary to guess all but the last transition in E. The algorithm can be thought of as exploring a search tree, where branchingis caused by guesses, and successor nodes are constructed by the usual operations ofpreparing a table and dealing with a counterexample.
The detailed process is given in Algorithm 2. The learner maintains a set of table instances, named ToExplore, which contains all table instances that need to be explored.
The initial tables in ToExplore are as follows. Each table has S = E = { }. For
each σ ∈ Σ, there is one row in R corresponding to the logical-timed word ω = (σ, 0).
It is necessary to guess a reset b for each ω thereby transforming it to a reset-logicaltimed word γr = (σ, 0, b). There are 2|Σ| possible combinations of guesses. Thesetables are ﬁlled by making membership queries (in this case, the membership queries foreach table are the same). The resulting 2|Σ| tables form the initial tables in ToExplore.

456

J. An et al.

Algorithm 2: Learning one-clock timed automaton with a normal teacher
input : the timed observation table T = (Σ, Σ, Σr , S, R, E, f ).
output: the hypothesis H recognizing the target language L.
1 ToExplore ← ∅; S ← {}; R ← {π(Γ (ω)) | ω = (σ, 0), ∀σ ∈ Σ}; E ← {};2 currentTable ← (Σ, Σ, Σr , S, R, E, f );3 tables ← guess and ﬁll(currentTable);// guess resets and fill all table instances
4 ToExplore.insert(tables);// insert table instances tables into ToExplore
5 currentTable ← ToExplore.pop();// pop out head instance as the current table
6 equivalent ← ⊥;7 while equivalent = ⊥ do
8
prepared ← is prepared(currentTable); // whether the current table is prepared9
while prepared = ⊥ do
10
if currentTable is not closed then11tables ← guess and make closed(currentTable); ToExplore.insert(tables);12
currentTable ← ToExplore.pop();
if currentTable is not consistent thentables ← guess and make consistent(currentTable); ToExplore.insert(tables);currentTable ← ToExplore.pop();

13
14
15

if currentTable is not evidence-closed thentables ← guess and make evidence closed(currentTable); ToExplore.insert(tables);currentTable ← ToExplore.pop();

16
17
18

prepared ← is prepared(currentTable);

19
20
21
22
23
24
25
26
27

M ← build DFA(currentTable) ;// transforming currentTable to a DFA M
H ← build hypothesis(M) ;// constructing a hypothesis H from M
equivalent, ctx ← equivalence query(H);// ctx is a delay-timed word
if equivalent = ⊥ thentables ← guess and ctx processing(currentTable, ctx ) ;// counterexample
processing
ToExplore.insert(tables);currentTable ← ToExplore.pop();return H;

In each iteration of the algorithm, one table instance is taken out of ToExplore. The
learner checks whether the table is closed, consistent, and evidence closed. If the table is
not closed, i.e. there exists r ∈ R such that row(r) = row(s) for all s ∈ S, the learnermoves r from R to S. Then for each σ ∈ Σ, the element r · (σ, 0) is added to R, and aguess has to be made for its reset information. Hence, 2|Σ| unﬁlled table instances will
be generated. Next, for each entry in the |Σ| new rows of R, it is necessary to guess reset
information for all but the last transition in e ∈ E. After this guess, it is now possible
to ﬁll the table instances by makingmembership queries with transformed delay-timed
words. Hence, there are at most 2( ei ∈E\{} (|ei |−1))×|Σ| ﬁlled table instances for one
unﬁlled table instance. All ﬁlled table instances are inserted into ToExplore.
If the table is not consistent, i.e. there exist some γr , γr ∈ S ∪ R and σr ∈ Σr suchthat γr ·σr , γr ·σr ∈ S ∪R and row(γr ) = row(γr ), but row(γr ·σr ) = row(γr ·σr ).
Let e ∈ E be one place where they are different. Then σr ·e needs to be added to E. For
each entry in S ∪ R, all but the last transition in σr · e need to be guessed, then the table
can be ﬁlled. 2(|σ·e|−1)×(|S|+|R|) ﬁlled table instances will be generated and inserted
into ToExplore. The operation for making tables evidence-closed is analogous.
Once the current table is prepared, the learner builds a hypothesis H and makes anequivalence query to the teacher. If the answer is positive, then H is a COTA which recognizes the target timed language L; otherwise, the teacher gives a delay-timed word
ω as a counterexample. The learner ﬁrst ﬁnds the longest reset-logical-timed word inLearning One-Clock Timed Automata

457

R which, when converted to a delay-timed word, agrees with a preﬁx of ω. The remainder of ω, however, needs to be converted to a reset-logical-timed word by guessing
reset information. The corresponding preﬁxes are then added to R. Hence, at most2|ω|
 unﬁlled table instances are generated. For each unﬁlled table instance, at most2( ei ∈E\{} (|ei |−1))×|ω| ﬁlled tables are produced and inserted into ToExplore.
Throughout the learning process, the learner adds a ﬁnite number of table instances
to ToExplore at every iteration. Hence, the search tree is ﬁnite-branching. Moreover, if
all guesses are correct, the resulting table instance will be identical to the observationtable in the learning process with a smart teacher (apart from the guessing processes,
the basic table operations are the same as those in Section 3.1). This means, with anappropriate search order, for example, taking the table instance that requires the least
number of guesses in ToExplore at every iteration, the algorithm terminates and returns the same table as in the learning process with a smart teacher, which is a COTA
that recognizes the target language L. In conformity to Theorem 1, the algorithm may
terminate even if the corresponding reset-logical-timed languages are not equivalent,
while yielding correct COTAs recognizing the same delay-timed language.
Theorem 6. Algorithm 2 terminates and returns a COTA H which recognizes the target
timed language L.
Complexity analysis. If T = (Σ, Σ, Σr , S, R, E, f ) is the ﬁnal observation table forthe correct candidate COTA, the number of guessed resets in S ∪R
is |S|+|R|, and thenumber of guessed resets for entries in each row of the table is ei ∈E\{} (|ei | − 1).
Hence, the total number of guessed resets is (|S| + |R|) × (1 + ei ∈E\{} (|ei | − 1)).
Assuming an appropriate search order (for example according to the number of guesses
in each table), this yields
the number of table instances considered before termination
as O(2(|S|+|R|)×(1+ ei ∈E\{} (|ei |−1)) ).

5

Implementation and Experimental Results

To investigate the efﬁciency and scalability of the proposed methods, we implemented
a prototype3 in P YTHON for learning deterministic one-clock timed automata. The examples include a practical case concerning the functional speciﬁcation of the TCP protocol [26] and a set of randomly generated DOTAs to be learnt. All of the evaluations
have been carried out on a 3.6GHz Intel Core-i7 processor with 8GB RAM running
64-bit Ubuntu 16.04.
Functional speciﬁcation of the TCP protocol. In [26], a state diagram on page 23 speciﬁes state changes during a TCP connection triggered by causing events while leading
to resulting actions. As observed by Ouaknine and Worrell in [31], such a functional
speciﬁcation of the protocol can be represented as a one-clock timed automaton. In our
setting, the corresponding DOTA A to be learnt is conﬁgured to have |Q| = 11 stateswith the two CLOSED states collapsed, |Σ| = 10 after abstracting the causing eventsand the resulting actions, |F | = 2, and |Δ| = 19 with appropriately speciﬁed timing
constraints including guards and resets. Using the algorithm with the smart teacher, a3Available at https://github.com/Leslieaj/OTALearning. The evaluated artifact is archived in [8].

458

J. An et al.
Table 1: Experimental results on random examples for the smart teacher situation.
Case ID |Δ|mean
4 4 207 2 107 4 107 6 107 4 20
10 4 20
12 4 20
14 4 20

16.3
16.9
25.7
26.0
34.3
39.1
47.6
58.4

#Membership
Nmin#Equivalence

Nmean Nmax Nmin Nmean Nmax

118 245.0
568 920.8
348 921.7
351 634.5
411 1183.4
920 1580.9
1090 2731.6
1390 2238.6

650
1393
1296
1050
1890
2160
5733
4430

20 30.1 42
23 31.3 37
34 50.9 64
35 44.7 70
52 70.5 93
61 73.1 88
66 97.4 125
79 107.7 135

nmean

tmean

4.5
9.1
9.3
7.8
9.5
11.7
16.0
16.0

24.7
14.6
38.0
49.6
101.7
186.7
521.8
515.5

Case ID: n m κ, consisting of the number of locations, the size of the alphabet and the maximum
constant appearing in the clock constraints, respectively, of the corresponding group of A’s.
|Δ|mean : the average number of transitions in the corresponding group.
#Membership & #Equivalence: the number of conducted membership and equivalence queries,
respectively. Nmin : the minimal, Nmean : the mean, Nmax : the maximum.
nmean : the average number of locations of the learned automata in the corresponding group.
tmean : the average wall-clock time in seconds, including that taken by the learner and the teacher.

correct DOTA H is learned in 155 seconds after 2600 membership queries and 28 equivalence queries. Speciﬁcally, H has 15 locations excluding a sink location connected by
28 transitions. The introduction of 4 new locations comes from splitting of guards alongtransitions, which however can be trivially merged back with other locations. The ﬁgures depicting A and H can be found in Appendix D of [7].
Random examples for a smart teacher. We randomly generated 80 DOTAs in eightgroups, with each group having different numbers of locations, size of alphabet, andmaximum constant appearing in clock constraints. As shown in Table 1, the proposed
learning method succeeds in all cases in identifying a DOTA that recognizes the same
timed language. In particular, the number of membership queries and that of equivalence queries appear to grow polynomially with the size of the problem4 , and aremuch smaller than the worst-case bounds estimated in Sect. 3.5. Moreover, the learned
DOTAs do not have prominent increases in the number of locations (by comparing
nmean with the ﬁrst component of Case IDs). The average wall-clock time including
both time taken by the learner and by the teacher is recorded in the last column tmean , ofwhich, however, often over 90% is spent by the teacher for checking equivalences w.r.t.
small T’s while around 50% by the learner for checking the preparedness condition
w.r.t. large T’s.
It is worth noting that all of the results reported above are carried out on an implementation equipped with the accelerating trick discussed in Sect. 3.6. We remark thatwhen dropping this trick, the average number of membership queries blow up with afactor of 0.83 (min) to 15.02 (max) with 2.16 in average for all the 8 groups, and 0.84(min) to 1.71 (max) with 1.04 for the average number of equivalence queries, leading
to dramatic increases also in the computation time (including that in operating tables).
4

An exception w.r.t. the group 7 6 10 is due to relatively simple DOTAs generated occasionally.

Learning One-Clock Timed Automata

459

Table 2: Experimental results on random examples for the normal teacher situation.
Case ID |Δ|mean
3 2 104 2 105 2 106 2 104 4 20

4.8
6.8
8.8
11.9
16.3

#Membership#Equivalence

Nmin Nmean Nmax

Nmin Nmean Nmax

43 83.7
67 134.0
75 223.9
73 348.3
231 371.0

167
345
375
708
564

5
6
9
10
27

8.8
13.3
15.2
16.7
30.9

14
24
24
30
40

nmean tmean #Texplored #Learnt
3.0 0.9
4.0 7.4
5.0 35.5
5.6 59.8
4.0 137.5

149.1
563.0
2811.65077.68590.0

10/10
10/10
10/10
7/10
6/10

#Membership & #Equivalence: the number of conducted membership and equivalence queries
with the cached methods, respectively. Nmin : the minimal, Nmean : the mean, Nmax : the maximum.
#Texplored : the average number of the explored table instances.
#Learnt: the number of the learnt DOTAs in the group (learnt/total).

The alternative implementation and experimental results without the accelerating trick
can also be found in the tool page (under the dev branch).
Random examples for a normal teacher. Due to its high, exponential complexity, thealgorithm with a normal teacher failed (out of memory) in identifying DOTAs for almost all the above examples, except 6 cases out of the 10 in group 4 4 20. We therefore
randomly generated 40 extra DOTAs of smaller size classiﬁed into 4 groups. With theaccelerating trick, the learner need not guess the resets in elements of E for an entry
in S ∪ R if the querying result of the entry is the sink location. We also omitted thechecking of the evidence-closed condition, since it may add redundant rows in R, leading to more guesses and thereby a larger search space. The omission does not affect thecorrectness of the learnt DOTAs. Moreover, as different table instances may generate
repeated queries, we cached the results of membership queries and counterexamples,such that the numbers of membership and equivalence queries to the teacher can besigniﬁcantly reduced. Table 2 shows the performance of the algorithm in this setting.
Results without caching are available in the tool page (under the normal branch).

6

Conclusion

We have presented a polynomial active learning method for deterministic one-clock
timed automata from a smart teacher who can tell information about clock resets inmembership and equivalence queries. Our technique is based on converting the problem to that of learning reset-logical-timed languages. We then extend the method tolearning DOTAs from a normal teacher who receives delay-timed words for membership queries, while the learner guesses the reset information in the observation table.
We evaluate both algorithms on randomly generated examples and, for the former case,the functional speciﬁcation of the TCP protocol.
Moving forward, an extension of our active learning method to nondeterministic
OTAs and timed automata involving multiple clocks is of particular interest.
Data Availability Statement The datasets generated and/or analyzed during the current study
are available in the Figshare repository: https://doi.org/10.6084/m9.ﬁgshare.11545983.v3.

460

J. An et al.

References
1. Aarts, F., Fiterau-Brostean, P., Kuppens, H., Vaandrager, F.W.: Learning register automata
with fresh value generation. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015.
LNCS, vol. 9399, pp. 165–183. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3319-25150-9 11
2. Aarts, F., Vaandrager, F.W.: Learning I/O automata. In: Gastin, P., Laroussinie, F.
(eds.) CONCUR 2010. LNCS, vol. 6269, pp. 71–85. Springer, Heidelberg (2010).
https://doi.org/10.1007/978-3-642-15375-4 6
3. Abdullah, J., Dai, G., Mohaqeqi, M., Yi, W.: Schedulability analysis and software synthesis
for graph-based task models with resource sharing. In: Proceedings of 24th IEEE Real-Timeand Embedded Technology and Applications Symposium, RTAS 2018. pp. 261–270. IEEE
Computer Society (2018)
4. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
5. 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)
6. Alur, R., Madhusudan, P.: Decision problems for timed automata: A survey. In: Bernardo,
M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1–24. Springer, Heidelberg(2004). https://doi.org/10.1007/978-3-540-30080-9 1
7. An, J., Chen, M., Zhan, B., Zhan, N., Zhang, M.: Learning one-clock timed automata (fullversion). arXiv:1910.10680 (2019), https://arxiv.org/abs/1910.10680
8. An, J., Chen, M., Zhan, B., Zhan, N., Zhang, M.: Learning one-clock timed automata.
Figshare (2020), https://doi.org/10.6084/m9.ﬁgshare.11545983.v3
9. An, J., Wang, L., Zhan, B., Zhan, N., Zhang, M.: Learning real-time automata. SCIENCECHINA Information Sciences (2020). https://doi.org/10.1007/s11432-019-2767-4, to appear.
10. Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2),87–106 (1987)
11. Argyros, G., D’Antoni, L.: The learnability of symbolic automata. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 427–445. Springer, Heidelberg(2018). https://doi.org/10.1007/978-3-319-96145-3 23
12. Bollig, B., Habermehl, P., Kern, C., Leucker, M.: Angluin-style learning of NFA. In: Proceedings of the 21st International Joint Conference on Artiﬁcial Intelligence, IJCAI 2009.
pp. 1004–1009. AAAI Press (2009)
13. Bollig, B., Katoen, J.P., Kern, C., Leucker, M., Neider, D., Piegdon, D.R.: libalf: The automata learning framework. In: Touili, T., Cook, B., Jackson, P.B. (eds.) CAV 2010. LNCS,
vol. 6174, pp. 360–364. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-64214295-6 32
14. Caldwell, B., Cardell-Oliver, R., French, T.: Learning time delay Mealy machines from programmable logic controllers. IEEE Trans. Automation Science and Engineering 13(2), 1155–
1164 (2016)
15. Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Active learning for extended ﬁnite state machines. Formal Asp. Comput. 28(2), 233–263 (2016)
16. Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Communications of
the ACM 24(8), 533–536 (1981)
17. Dima, C.: Real-time automata. Journal of Automata, Languages and Combinatorics 6(1),
3–23 (2001)
18. Drews, S., D’Antoni, L.: Learning symbolic automata. In: Legay, A., Margaria, T.
(eds.) TACAS 2017. LNCS, vol. 10205, pp. 173–189. Springer, Heidelberg (2017).
https://doi.org/10.1007/978-3-662-54577-5 10

Learning One-Clock Timed Automata

461

19. Farzan, A., Chen, Y., Clarke, E.M., Tsay, Y., Wang, B.: Extending automated compositional veriﬁcation to the full class of omega-regular languages. In: Ramakrishnan, C.R.,
Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 2–17. Springer, Heidelberg (2008).
https://doi.org/10.1007/978-3-540-78800-3 2
20. Fiterau-Brostean, P., Janssen, R., Vaandrager, F.W.: Combining model learning and model
checking to analyze TCP implementations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016.
LNCS, vol. 9780, pp. 454–471. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3319-41540-6 25
21. Fiterau-Brostean, P., Lenaerts, T., Poll, E., de Ruiter, J., Vaandrager, F.W., Verleg, P.: Modellearning and model checking of SSH implementations. In: Proceedings of the 24th ACM
SIGSOFT International SPIN Symposium on Model Checking of Software, SPIN 2017. pp.
142–151. ACM (2017)
22. Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theor.
Comput. Sci. 411(47), 4029–4054 (2010)23. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company (1979)
24. Howar, F., Jonsson, B., Vaandrager, F.W.: Combining black-box and white-box techniques
for learning register automata. In: Steffen, B., Woeginger, G.J. (eds.) Computing and Software Science - State of the Art and Perspectives, LNCS, vol. 10000, pp. 563–588. Springer,
Cham (2019). https://doi.org/10.1007/978-3-319-91908-9 26
25. Howar, F., Steffen, B., Jonsson, B., Cassel, S.: Inferring canonical register automata. In:
Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 251–266. Springer,
Heidelberg (2012). https://doi.org/10.1007/978-3-642-27940-9 17
26. Information Science Institute, University of Southern California: Transmission control protocol (DARPA internet program protocol speciﬁcation). https://www.rfc-editor.org/rfc/rfc793.
txt (1981)
27. Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib - A framework for active
automata learning. In: Kroening, D., Pasareanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp.
487–495. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-319-21690-4 32
28. Li, Y., Chen, Y., Zhang, L., Liu, D.: A novel learning algorithm for Büchi automata basedon family of DFAs and classiﬁcation trees. In: Legay, A., Margaria, T. (eds.) TACAS 2017.
LNCS, vol. 10205, pp. 208–226. Springer, Heidelberg (2017). https://doi.org/10.1007/9783-662-54577-5 12
29. Maler, O., Mens, I.: Learning regular languages over large alphabets. In: Ábrahám, E.,
Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 485–499. Springer, Heidelberg(2014). https://doi.org/10.1007/978-3-642-54862-8 41
30. Margaria, T., Niese, O., Raffelt, H., Steffen, B.: Efﬁcient test-based model generation for
legacy reactive systems. In: Proceedings of the 9th IEEE International High-Level Design
Validation and Test Workshop, HLDVT 2004. pp. 95–100. IEEE Computer Society (2004)
31. Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: Closing
a decidability gap. In: Proceedings of the 19th IEEE Symposium on Logic in Computer
Science, LICS 2004. pp. 54–63. IEEE Computer Society (2004)
32. Pastore, F., Micucci, D., Mariani, L.: Timed k-Tail: Automatic inference of timed automata.
In: Proceedings of 10th IEEE International Conference on Software Testing, Veriﬁcation andValidation, ICST 2017. pp. 401–411. IEEE Computer Society (2017)33. Schmidt, J., Ghorbani, A., Hapfelmeier, A., Kramer, S.: Learning probabilistic real-time automata from multi-attribute event logs. Intell. Data Anal. 17(1), 93–123 (2013)34. Shahbaz, M., Groz, R.: Inferring Mealy machines. In: Cavalcanti, A., Dams, D.
(eds.) FM 2009. LNCS, vol. 5850, pp. 207–222. Springer, Heidelberg (2009).
https://doi.org/10.1007/978-3-642-05089-3 14

462

J. An et al.

35. Stigge, M., Ekberg, P., Guan, N., Yi, W.: The digraph real-time task model. In: Proceedingsof 17th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS
2011. pp. 71–80. IEEE Computer Society (2011)
36. Tappler, M., Aichernig, B.K., Bacci, G., Eichlseder, M., Larsen, K.G.: L∗ -based learning ofMarkov decision processes. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019.
LNCS, vol. 11800, pp. 651–669. Springer, Heidelberg (2019). https://doi.org/10.1007/9783-030-30942-8 38
37. Tappler, M., Aichernig, B.K., Larsen, K.G., Lorber, F.: Time to learn - learning timed automata from tests. In: André, É., Stoelinga, M. (eds.) FORMATS 2019. LNCS, vol. 11750,
pp. 216–235. Springer, Heidelberg (2019). https://doi.org/10.1007/978-3-030-29662-9 13
38. Vaandrager, F.W.: Model learning. Communications of the ACM 60(2), 86–95 (2017)
39. Verwer, S., de Weerdt, M., Witteveen, C.: One-clock deterministic timed automata are efﬁciently identiﬁable in the limit. In: Dediu, A., Ionescu, A., Martı́n-Vide, C. (eds.) LATA 2009.
LNCS, vol. 5457, pp. 740–751. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3642-00982-2 63
40. Verwer, S., de Weerdt, M., Witteveen, C.: The efﬁciency of identifying timed automata andthe power of clocks. Information and Computation 209(3), 606–625 (2011)
41. Verwer, S., de Weerdt, M., Witteveen, C.: Efﬁciently identifying deterministic real-time automata from labeled data. Machine Learning 86(3), 295–333 (2012)
42. Verwer, S., Weerdt, M.D., Witteveen, C.: An algorithm for learning real-time automata. In:
Proceedings of the 18th Annual Machine Learning Conference of Belgium and the Netherlands, Benelearn 2007. pp. 57–64 (2007)

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0
International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing,
adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license
and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter’s Creative
Commons license, unless indicated otherwise in a credit line to the material. If material is notincluded in the chapter’s Creative Commons license and your intended use is not permitted bystatutory regulation or exceeds the permitted use, you will need to obtain permission directly fromthe copyright holder.