Active Learning of One-Clock Timed Automata
Using Constraint Solving
Runqing Xu1,2(B) , Jie An3(B) , and Bohua Zhan1,2(B)1State Key Laboratory of Computer Science, Institute of Software, CAS, Beijing, China{xurq,bzhan}@ios.ac.cn
2
University of Chinese Academy of Sciences, Beijing, China
3
Max Planck Institute for Software Systems, Kaiserslautern, Germany
jiean@mpi-sws.org
Abstract. Active automata learning in the framework of Angluin’s L∗ algorithm
has been applied to learning many kinds of automata models. In applications totimed models such as timed automata, the main challenge is to determine guards
on the clock value in transitions as well as which transitions reset the clock. In
this paper, we introduce a new algorithm for active learning of deterministic oneclock timed automata and timed Mealy machines. The algorithm uses observationtables that do not commit to specific choices of reset, but instead rely on constraint
solving to determine reset choices that satisfy readiness conditions. We evaluate
our algorithm on randomly-generated examples as well as practical case studies,
showing that it is applicable to larger models, and competitive with existing work
for learning other forms of timed models.
Keywords: Active learning · Timed automata · Constraint solving

1 Introduction
Within Angluin’s L∗ framework [7], active learning is a type of model inference tolearn an unknown language by making queries to a teacher. There are two kinds ofqueries: membership queries and equivalence queries. For a membership query, theteacher answers whether the queried word is in the target language. Usually, the learnercollects query results in an observation table. When the observation table satisfies somereadiness conditions, it can be transformed to a candidate automaton for an equivalence query. The teacher answers whether the candidate automaton recognizes the target language, and returns a counterexample if the answer is negative. In recent decades,
the core algorithm has seen many technical improvements, has been extended to learn
different kinds of models, and has been applied to many realistic settings. We referto [17, 20] for surveys.
For timed systems, timing constraints play a key role in the correctness of the system. In general, automata learning of timed systems require learning a timed modelfrom either passive or active observations of the system, consisting of a collection ofThis work has been partially funded by NSFC under grant No. 62032024, and by DFG project
389792660-TRR 248.
c The Author(s), under exclusive license to Springer Nature Switzerland AG 2022
A. Bouajjani et al. (Eds.): ATVA 2022, LNCS 13505, pp. 249–265, 2022.
https://doi.org/10.1007/978-3-031-19992-9_16

250

R. Xu et al.

time-event sequences. The learned model should describe these timing behaviors correctly. Timed automata [2], extending DFAs with clock variables, is a popular formal
model of timed systems. However, there are several obstacles to active learning of timed
automata. Since the transitions of timed automata contain both timing constraints thattest the values of clocks, and resets that update the clocks, we need to determine (1)the number of clocks, (2) the reset information, and (3) the timing constraints, none ofwhich are directly observable from time-event sequences. Hence, existing work consider timed automata with different restrictions. Among them, An et al. introduced
an active learning algorithm for deterministic one-clock timed automata (DOTAs) [4].
They first suppose that the teacher can return reset information in the queries, thenthe assumption is dropped by allowing the algorithm to search through possible combinations of reset information. However, this search process results in an exponential
blow up, limiting the scalability of the algorithm in practical applications. Vaandrager
et al. [21] considered a different class of timed models called Mealy machines with one
timer, and proposed a learning algorithm with polynomial complexity.
In this paper, we present a new active learning algorithm for deterministic one-clock
timed automata1 . The main innovation of the algorithm is to maintain all available
observations in a single observation table, without committing to a particular choiceof resets. The readiness conditions of the observation table, such as closedness, consistency, etc., are encoded as formulas in terms of variables for reset information andlocation assignments. These constraints are then solved using SMT solvers to determine feasible assignments of resets and locations that make the observation table ready,and from which a candidate automaton can be constructed. The learning algorithm isguaranteed to terminate and return a correct automaton. While the theoretical worstcase complexity of the algorithm is still exponential, by leveraging the efficiency of
SMT solvers, it is much more efficient than the algorithm in [4] in practice. In order toapply the algorithm to learning real-time reactive systems, we extend it to timed Mealy
machines, which can be considered as an extension of Mealy machines with one clock,or extension of deterministic one-clock timed automata to include inputs and outputs.
The algorithm is implemented and evaluated on a number of randomly generated
models and four models from practical applications. The experimental results showthat our algorithm is scalable to much larger models compared to [4]. Additionally, ourmethod successfully learns all four models from practical applications, with costs thatis competitive against algorithms designed for other forms of models.
The organization of the paper is as follows. We give some background material in
Sect. 2. The algorithm for learning DOTAs is described in Sect. 3, and its extension to
timed Mealy machines in Sect. 4. We describe the implementation and experiments in
Sect. 5, and finally conclude in Sect. 6.
Related Work. Active learning of timed systems has been studied on many kinds ofmodels with different restrictions. In [10, 11], Grinchtein et al. proposed learning algorithms for event-recording automata (ERAs) [3], a kind of timed automata associating
every action a with a clock xa that records the length of time since the last occurrenceof a. Henry et al. considered in [12] reset-free ERAs, where some transitions may reset
1

The full version is available at https://arxiv.org/abs/2208.00412.

Active Learning of One-Clock Timed Automata Using Constraint Solving

251

no clocks. An et al. introduced a learning algorithm for deterministic one-clock timed
automata (DOTAs) in [4], but due to the brute-force search over choice of resets, thealgorithm is limited to timed automata with a small number of locations. For real-time
automata (RTA) [8], efficient learning algorithms have been designed in both the deterministic [5] and nondeterministic case [6]. Recently, Vaandrager et al. introduced a newkind of timed models named Mealy machine with one timer (MM1T), and proposed anefficient active learning algorithm for such models [21]. It extends Mealy machine witha single timer which can be set to an integer value at transitions.
Passive learning has also been investigated for learning timed automata based on
different methods [1, 18, 22–24]. Constraint solving has been used extensively in passive learning. For example, Smetsers et al. used this technique in passive learning ofDFAs, Mealy machines and register automata [16], by encoding the existence of an
automaton with n locations consistent with a set of observations in a logical formula.
Recent work [19] also applied constraint solving to passive learning of timed automata.
Compared to these works, we remain in the active learning setting, encoding constraints
for the readiness of observation tables rather than consistency with a set of observations.
Our work demonstrates that constraint solving can be fruitfully applied in active learning, determining not only location assignments but also other hidden parts of the modelsuch as clock-reset information.

2 Preliminaries
In this section, we introduce several concepts of one-clock timed automata. Let R≥0 and
N be the set of non-negative reals and natural numbers, respectively. The set of boolean
values is denoted as B = {, ⊥}, where  stands for true and ⊥ for false.
Let c be the single clock variable, denote by Φc the set of clock constraints of theform φ:: =  | c  m | φ ∧ φ, where m ∈ N and  ∈ {=, <, >, ≤, ≥}. Since there
is only one clock, a clock constraint can be represented as an integer-bounded interval
whose endpoints are in N ∪ {∞}. For example, c ≤ 5 ∧ c > 4 is represented as (4, 5],
c = 6 as [6, 6], and  as [0, ∞). We will use inequality and interval representations
interchangeably in this paper. Let the finite set of actions Σ be fixed.
Definition 1 (One-clock timed automata [4]). A one-clock timed automaton (OTA) A
is a 6-tuple (Σ, Q, q0 , F, c, Δ), where Σ is a finite set of actions, called the alphabet;
Q is a finite set of locations; q0 ∈ Q is the initial location; F ⊆ Q is a set of accepting
locations; c is the unique clock; and Δ ⊆ Q × Σ × Φc × B × Q is a finite set oftransitions.
A transition δ = (q, σ, φ, b, q  ) allows a jump from the source location q to the target
location q  by performing the action σ ∈ Σ if the guard φ ∈ Φc is satisfied. Meanwhile,clock c is reset to zero if b = , and remains unchanged otherwise. Clock valuation isa function ν : c → R≥0 that assigns a non-negative real number to the clock. A state of
A is a pair (q, ν), where q ∈ Q and ν is a clock valuation.
Given an OTA A, with κ being the maximum constant appearing in the guards, thenthe clock valuations can be divided into regions, where each region is of the form [n, n]
for n ≤ κ, or (n, n + 1) for n < κ, or (κ, ∞). This gives a partition of R≥0 . For clock252

R. Xu et al.

valuation ν, we denote by ν the region containing it. Regions are commonly used inalgorithms for analyzing timed automata, making the state space essentially finite.
Given a timed word ω = (σ1 , t1 )(σ2 , t2 ) · · · (σn , tn ) ∈ (Σ × R≥0 )∗ , where ti represents the delay time between two actions σi−1 and σi , there is a run of A such that
t1 ,σ1t2 ,σ2tn ,σnρ = (q0 , ν0 ) −−−→ (q1 , ν1 ) −−−→ · · · −−−→ (qn , νn ), where ν0 (c) = 0, only if(1) (qi−1 , σi , φi , bi , qi ) ∈ Δ, (2) νi−1 (c) + ti satisfies φi , (3) νi (c) = νi−1 (c) + ti
if bi = ⊥ and νi (c) = 0 otherwise, for all 1 ≤ i ≤ n. Let |ω| denote its length.
When the timed automaton A is known, each timed word ω can be extended byincluding the reset information bi , indicating whether there is a reset after taking
the transition for (σi , ti ). We denote the corresponding reset timed word as ωr =(σ1 , t1 , b1 )(σ2 , t2 , b2 ) · · · (σn , tn , bn ). If qn ∈ F , then ω is an accepting timed wordof A. The (recognized) timed language L(A) is the set of accepting timed words of A.
An OTA is a deterministic one-clock timed
automaton (DOTA) if there is at most one run for
any timed word (equivalently, if the guards of transitions from any location under the same action do
not intersect each other). Two DOTAs are equivalent
if they recognize the same timed language. A DOTA
is complete if for any q ∈ Q and action σ ∈ Σ, thecorresponding guards form a partition of R≥0 . Thismeans any given timed word has exactly one run.
Any DOTA A can be transformed into a complete Fig. 1. An example of complete
DOTA (COTA) accepting the same timed language DOTA
by introducing a non-accepting “sink” location andletting all invalid or non-described behaviors go to the sink. We therefore assume that
we are working with complete DOTAs. Figure 1 shows a DOTA A, with q2 added as
the sink location to make it complete.
The classic method of active learning is L∗ algorithm [7] which can be regarded
as an interaction between a learner and a teacher, where the teacher can answer membership and equivalence queries. In a membership query, the learner can ask if a word
belongs to the target language, or if a constructed automaton accepts that language as
an equivalence query. The teacher can answer “yes” or “no” for the queries and returncounterexamples for the equivalence queries. The learner collects query results andcounterexamples in the observation table consisting of three sets of words: a prefixclosed set S, a set R and a suffix-closed set E. Each word in S corresponds to a uniquelocation. Words in R can be considered the “boundary” of S, and E contains suffixes
to distinguish different words in S ∪ R.
An et al. [4] described an active learning algorithm for DOTAs. Inherited from L∗ ,in a membership query, the teacher is given a timed word. We use MQ : (Σ × R≥0 )∗ →{+, −} to denote the function mapping timed words to + if it is accepted, and − otherwise. In an equivalence query, the teacher receives a hypothesis DOTA H, and return acounterexample in the negative case in addition. In that work, a “smart” teacher is first
assumed, who also returns the reset information for any timed word given as membership query. With this reset information, an observation table can be maintained where
each row in S ∪ R and each column in E is a logical timed word, which contains theclock valuation after each transition rather than the delay times. When the observation

Active Learning of One-Clock Timed Automata Using Constraint Solving

253

table satisfies readiness conditions, a candidate automaton is constructed in a manner
similar to the learning of symbolic automata [9]. Next, in the “normal” teacher setting,where the teacher does not return reset information, the algorithm searches over all
possible choices of resets for timed words in S ∪ R, constructing one observation tablefor each. Due to the large time and memory requirements, the algorithm has limited
scalability (up to six locations for the randomly constructed examples in the paper).

3 Learning Algorithm
In this section, we describe a new algorithm for active learning of DOTAs by incorporating constraint solving using SMT solvers. The main idea of the algorithm is tomaintain a single observation table that collects all results from previous membership
queries, rather than one observation table for each possible choice of resets. Instead, thereset information is encoded as boolean variables with unknown values. At any time,
the observation table may be ready for some choice of resets, but not for others. We
encode the readiness conditions for the observation table as a formula on the variables
for reset information, as well as for the location assignments of rows in the table. An
SMT solver is then used to solve these constraints, returning a choice of resets that makethe table ready, as well as a candidate automaton that can be sent for equivalence query.
Several difficulties must be addressed in order to realize this idea. In particular,
whether two rows in the observation table are distinguishable is no longer clear-cut, but
may depend on the choice of resets. This also means the partition of rows into S and R
in the traditional L∗ algorithm need to be extended, by adding a category S+ of rowsthat are distinguishable from rows in S only for some choice of resets, that are needed
for building candidate automaton.
In the remainder of this section, we first discuss comparison of timed words without
being certain of clock-reset information, then extensions made to the observation table,
method of encoding readiness constraints, and finally the main algorithm together withtermination and complexity analysis.
3.1 Alignment and Comparison of Timed Words
In the L∗ framework, one key step is to determine if two words w1 and w2 belong
to different equivalence classes of the target regular language, i.e., arrive at different
locations of the underlying target DFA A. It is achieved by membership queries via
testing words w1 and w2 after appending some suffix e. If w1 · e is an accepting word
and w2 · e is not (or vice versa), then w1 and w2 must arrive at different locations.
In our case, suppose A is the target DOTA to be learned. Given two timed words ω1
and ω2 , we wish to determine whether they arrive at different locations of A. However,since the reset information is not observable when running timed words ω1 and ω2 , thevalues of the clock at the end is unknown. If the values of the clock are not the same,the result of running ω1 · e and ω2 · e may be different even if ω1 and ω2 arrive at thesame location. In order to effectively test using the suffix e, we need to suppose thatthe last time when the clock resets in ω1 and ω2 are known, and then align the valuesof the clock before executing the suffix e. We state these concepts more formally in thefollowing definitions.

254

R. Xu et al.

Definition 2 (Last reset of a timed word). Given a timed word ω = (σ1 , t1 )(σ2 , t2 )· · · (σn , tn ), and DOTA A. Let ωr = (σ1 , t1 , b1 )(σ2 , t2 , b2 ) · · · (σn , tn , bn ) be the reset
timed word that results from running ω on A. The last reset kA (ω) is defined to be 0 if
bi = ⊥ for all 1 ≤ i ≤ n, and kA (ω) = i if bi =  and bj = ⊥ for all j > i.
Suppose the last reset kA (ω) is known for a timed word ω, then we can computethe value of clock after executing ω on A. Let νc (ω, i) be the value of clock after
executing ω if the last reset equals i. This is computed as the sum of ti+1 to tn , where
n is the length of ω (if i = n, for the case where the last reset occurs after (σn , tn ),then νc (ω, i) = 0). Hence, given two timed words ω1 and ω2 with known values of lastresets i1 , i2 , it is possible to align the two timed words for testing a suffix e.
Definition 3 (Alignment for testing on a suffix). Consider two timed words ω1 , ω2 ,and suppose their last resets are i1 , i2 respectively. Let e = (σ1 , t1 )(σ2 , t2 ) · · · (σm , tm )be a nonempty suffix. Let ν1 = νc (ω1 , i1 ) and ν2 = νc (ω2 , i2 ). Then form the suffixes
e1 , e2 depending on the following cases:– If ν1 > ν2 , then let e1 = e and e2 = (σ1 , t1 + (ν1 − ν2 )) · (σ2 , t2 ) · · · (σm , tm ).
– If ν1 < ν2 , then let e1 = (σ1 , t1 + (ν2 − ν1 )) · (σ2 , t2 ) · · · (σm , tm ) and e2 = e.
– If ν1 = ν2 , then let e1 = e2 = e.
Define a test T (ω1 , ω2 , i1 , i2 , e) between ω1 and ω2 with suffix e and last resets i1 , i2
as follows. If e is nonempty, then the test compares results for two membership queries
ω1 · e1 and ω2 · e2 . The test succeeds, i.e. T (ω1 , ω2 , i1 , i2 , e) = , if MQ(ω1 · e1 ) =MQ(ω2 · e2 ). Otherwise T (ω1 , ω2 , i1 , i2 , e) = ⊥. If e is empty, the test simply compares
the results for membership queries ω1 and ω2 .
It is clear that with the definition of e1 and e2 , the value of clock when executing
the first timed action of e1 and e2 during the tests must be the same. Hence, if ω1 andω2 arrive at the same location, then the behavior on e1 and e2 must be the same as well.
Hence, we obtain the following lemma.
Lemma 1 (Distinguishable timed words). If the test T between ω1 and ω2 with suffix
e and last resets i1 , i2 fails, then for any DOTA A such that i1 = kA (ω1 ) and i2 =kA (ω2 ), the timed words ω1 and ω2 must arrive at different locations in A.
Example 1. Consider two timed words ω1 = (a, 4) and ω2 = . They are both acceptedby A in Fig. 1. Consider suffix e = (a, 5.5). If the last resets are i1 = 0 and i2 = 0(the correct reset for A), then e1 = (a, 5.5) and e2 = (a, 9.5), and MQ(ω1 · e1 ) =+, MQ(ω2 · e2 ) = −, so they can be distinguished, and indeed ω1 and ω2 arrive at
different locations as required by Lemma 1. If the last resets are i1 = 1 and i2 = 0,then e1 = e2 = (a, 5.5), and MQ(ω1 · e1 ) = MQ(ω2 · e2 ) = +, so they cannot be
distinguished. Hence, when we do not know the true reset information, whether ω1 andω2 are distinguishable by e = (a, 5.5) depends on the choice of resets.
Since A is unknown during learning, we need to iterate over all possible combinations of last resets. For two timed words ω1 and ω2 , we define the set of valid combinations of last resets as follows.

Active Learning of One-Clock Timed Automata Using Constraint Solving

255

Definition 4 (Valid combinations of last resets). Consider two timed words ω1 , ω2and suppose the length of the longest common prefix of ω1 and ω2 is m. Then the set
C(ω1 , ω2 ) of valid combinations of last resets isC(ω1 , ω2 ) = {(i1 , i2 ) | 0 ≤ i1 ≤ |ω1 |∧0 ≤ i2 ≤ |ω2 |∧(i1 ≤ m∧i2 ≤ m ⇒ i1 = i2 )}.
Example 2. Suppose ω1 = (a, 4) and ω2 = (a, 4)(a, 5.5), then m = 1, and the setof valid combinations are C(ω1 , ω2 ) = {(0, 0), (0, 2), (1, 1), (1, 2)}. In particular (0, 1)
or (1, 0) are not allowed, since they give contradicting reset choices for the transition
taken by (a, 4).

3.2 Timed Observation Table
Definition 5 (Observation table). An observation table O = (S, S+ , R, E, f, N ) is a
6-tuple, satisfying the following conditions:– S, S+ , R are disjoint finite sets of timed words called prefixes. S ∪ S+ ∪ R is prefixclosed and  ∈ S. If ω ∈ S ∪ S+ and σ ∈ Σ, then ω · (σ, 0) ∈ S ∪ S+ ∪ R.
– E is a finite set of timed words called suffixes, with  ∈ E.
– f is a function mapping pairs ω1 , ω2 ∈ S ∪ S+ ∪ R and (i1 , i2 ) ∈ C(ω1 , ω2 ) to B,
indicating whether ω1 and ω2 are currently distinguished under last resets i1 , i2 .
– N is the current limit on the number of locations in the candidate automaton.
The value f (ω1 , ω2 , i1 , i2 ) is computed as follows. For each suffix e ∈ E, test thepair ω1 , ω2 under last resets i1 , i2 and suffix e as in Definition 3. If T (ω1 , ω2 , i1 , i2 , e) = for all e ∈ E, then f (ω1 , ω2 , i1 , i2 ) = , otherwise f (ω1 , ω2 , i1 , i2 ) = ⊥.
Definition 6 (Certainly distinct rows). Given an observation table O, two rows
ω1 , ω2 are certainly distinct if f (ω1 , ω2 , i1 , i2 ) = ⊥ for all i1 , i2 ∈ C(ω1 , ω2 ).
We first explain the different components of O in an intuitive way. The set S contains timed words that are certainly distinct from each other. The set S+ are additionalrows in the observation table that are distinct from rows in S under some choice of
resets, that are required to be in the interior for some candidate automata. The set R
is the boundary of the observation table as usual for L∗ algorithms. The condition that
ω · (σ, 0) ∈ S ∪ S+ ∪ R is analogous to the condition that ω · σ ∈ S ∪ R in the DFA
case. It enforces that information is available to construct the transitions in the candidate
automaton for each location and action σ ∈ Σ.

Fig. 2. Left: an instance of observation table O during learning of A in Fig. 1; Right: candidate
DOTA constructed from the table after moving (a, 4)(a, 5.5) to S+ .

256

R. Xu et al.

Example 3. Figure 2 shows an instance of the observation table. The rows of the table
are timed words in S, S+ and R (here S+ is empty). The columns of the table areindexed by the same timed words. Each cell in the table summarizes when two timed
words are distinguished (the function f ), using formulas in terms of reset variables
b introduced in Sect. 3.3. The table also shows the list of suffixes E. For example,
for timed words (a, 4) and , we need to compare them on suffix (a, 5.5) after alignment. According to the analysis in Example 1, we have f ((a, 4), , 0, 0) = ⊥ and
f ((a, 4), , 1, 0) = . This is summarized as the expression b3 .
The main difference between the observation table defined here and the usual ones
for L∗ algorithms is that we do not record a particular query result for each prefix in
S ∪ S+ ∪ R and suffix E, as these results cannot be used effectively without knowing
reset information. In contrast, we maintain which pairs of rows can be distinguishedfor each possible choice of reset information. This can be contrasted with the approachin [4]. Rather than maintaining a copy of the observation table for each combination ofreset information, our method records all information obtained so far in a single table,with reset information determined by constraint solving.
3.3

Encoding of Readiness Constraints

To obtain a hypothesis DOTA H from observation table O, we should provide an assignment for the location and reset information of each timed word in S ∪ S+ ∪ R, which
ensure readiness conditions for the table, such as closedness and consistency. The mainidea is to encode such readiness conditions as formulas in terms of location and reset
assignments, and then use SMT solvers to find feasible solutions to these constraints orprove that they are not satisfiable. The constraints are stated in terms of two variables
for each row ω ∈ S ∪ S+ ∪ R: an ending reset variable bω and a location variable qω .
Definition 7 (Ending reset variable and location variable). Given a timed word ω =(σ1 , t1 ) . . . (σn , tn ) ∈ S ∪ S+ ∪ R, define the ending reset variable bω ∈ {, ⊥} todenote whether clock resets after running the final timed action (σn , tn ) (for the empty
timed word , we declare b = ). Define the location variable qω ∈ {1, . . . , N } torepresent the location after running ω in the candidate automaton.
Since the set of timed words S ∪ S+ ∪ R is prefix-closed, the ending reset variables{bω }ω∈S∪S+ ∪R in fact determine whether the clock resets after each timed action foreach row in S ∪ S+ ∪ R. In particular, we can encode the last reset for ω in terms of theending reset variables.
Definition 8 (Encoding of last reset). Given ω = (σ1 , t1 )...(σn , tn ) ∈ S ∪ S+ ∪ R.
Let ω|i for 0 ≤ i ≤ n be the prefix of ω with length i. Since S ∪ S+ ∪ R is prefix-closed,
we have each ω|i ∈ S ∪ S+ ∪ R as well. Let lr(ω, i), encoding the condition that thelast reset of ω equals i, be defined as follows.
¬bω|j .
lr(ω, i)  bω|i ∧i<j≤nActive Learning of One-Clock Timed Automata Using Constraint Solving

257

For each pair of rows ω1 , ω2 ∈ S ∪ S+ ∪ R and each pair of last resets (i, j) ∈C(ω1 , ω2 ), the condition that the last resets of ω1 , ω2 equal i, j respectively is encoded
as follows.
LR(ω1 , ω2 , i, j)  lr(ω1 , i) ∧ lr(ω2 , j).
Based on the encoding of last reset, the readiness constraints for the observationtable can be encoded in terms of the above variables as follows.
Constraint 1 (Distinctness of rows). Given timed words ω1 , ω2 ∈ S ∪ S+ ∪ R, andlast resets i, j ∈ C(ω1 , ω2 ), suppose f (ω1 , ω2 , i, j) = ⊥ (meaning ω1 and ω2 can be
distinguished under last resets i, j in the observation table), then we have the following
constraint, indicating ω1 and ω2 cannot be assigned to the same location.
C1 (ω1 , ω2 , i, j)  LR(ω1 , ω2 , i, j) ⇒ qω1 = qω2 .
Define the constraint C1 to be the conjunction of all C1 (ω1 , ω2 , i, j), for all pairs ofrows and valid last resets that can be distinguished.

C1 
C1 (ω1 , ω2 , i, j).
ω1 ,ω2 ∈S∪S+ ∪R,(i,j)∈C(ω1 ,ω2 ),f (ω1 ,ω2 ,i,j)=⊥Constraint 2 (Consistency). Given timed words ω1 , ω2 ∈ S ∪ S+ ∪ R and last resets
i, j ∈ C(ω1 , ω2 ). Suppose ω1 = ω1 · (σ, t1 ) and ω2 = ω2 · (σ, t2 ) also appear in
S ∪ S+ ∪ R, for some σ ∈ Σ and t1 , t2 ∈ R≥0 . Suppose that under the last resets i, j,
the value of clock after executing last timed action of ω1 , but before possible resets, isin the same region as that for ω2 , then if ω1 and ω2 also go to the same location, thetransition to be carried out for the last timed action of ω1 and ω2 must be the same.
Hence both ending reset and location for ω1 and ω2 must be the same. This is encoded
as constraints as follows.
C2 (ω1 , ω2 , i, j, σ, t1 , t2 )  qω1 = qω2 ∧ LR(ω1 , ω2 , i, j) ⇒ bω1 = bω2 ∧ qω1 = qω2 .
It is added as a constraint only if νc (ω1 , i) + t1  = νc (ω2 , j) + t2 , and if
f (ω1 , ω2 , i, j) = . We define constraint C2 to be the conjunction of all such constraints.
C2 (ω1 , ω2 , i, j, σ, t1 , t2 ).
C2 
ω1 ,ω2 ∈S∪S+ ∪R,
ω1 ·(σ,t1 ),ω2 ·(σ,t2 )∈S∪S+ ∪R,(i,j)∈C(ω1 ,ω2 ),f (ω1 ,ω2 ,i,j)= ,νc (ω1 ,i)+t1 =νc (ω2 ,j)+t2 Constraint 3 (Closedness). The closedness condition for usual L∗ algorithms statesthat each row in R must be represented by a row in S. In our case, we require that eachrow in R is represented by a row in S ∪ S+ . This translates to the constraint that eachlocation in the candidate automaton must be represented by a row in S ∪ S+ , encoded
as follows (recall N is the current limit on the number of locations).
qω = i ∧ C3 where C3 
1 ≤ qω ≤ N.
C3 
1≤i≤N ω∈S∪S+ω∈S∪S+ ∪R

258

R. Xu et al.

During the algorithm, we also make constraint solving queries where the closedness
condition is not enforced. Then only the second part C3 is used.
Constraint 4 (Special assignments). In order to speed-up constraint solving, we
directly make assignments to the location variables of rows in S. Order the rows of
S as S = {ω1 , ω2 , . . . , ω|S| }, then the special assignments are encoded as follows.
C4 
qωi = i.
1≤i≤|S|In the main learning algorithm, we will use SMT solvers to attempt to find solutions
to these constraints. The algorithm will first attempt to find a solution using C3 together
with C1 , C2 and C4 . If a solution is found, it proceeds to hypothesis construction as
described in Sect. 3.4. Otherwise, it attempts to find a solution using C3 or by increasing
N . The details are described in Sect. 3.5.
3.4

Hypothesis Construction

Once the SMT solver gives a model satisfying constraints in Sect. 3.3, we can builda hypothesis DOTA H = (Σ, QH , q0H , FH , c, ΔH ) from observation table O =(S, S+ , R, E, f, N ) and assignments bω and qω to ending reset variable and location
variables in the model. We define location set QH = {qω | ω ∈ S ∪S+ }, initial location
q0H = q , and accepting locations FH = {qω | MQ(ω) = + ∧ ω ∈ S ∪ S+ }. Next, we
describe how to construct the transitions ΔH .
Given two rows ω1 , ω2 ∈ S ∪ S+ ∪ R such that ω2 = ω1 · (σ, t), we can construct an
auxiliary transition δ  = (qω1 , σ, ψ, bω2 , qω2 ) with ψ = ν(ω1 ) + t where ν(ω1 ) is thevalue of clock after executing ω1 . Since the table is prefix-closed, the reset informationfor every timed action in ω1 has been determined. Therefore, we can determine ν(ω1 ).
We collect all such auxiliary transitions as the set Δ .
For any q ∈ QH and σ ∈ Σ, let Ψq,σ = {ψ | (q, σ, ψ, b, q  ) ∈ Δ } be the list ofclock values on auxiliary transitions from q and with action σ. We sort Ψq,σ and apply
the partition function P (·) to obtain m intervals, written as g1 , · · · , gm , satisfying ψi ∈gi for any 1 ≤ i ≤ m, where m = |Ψq,σ |; consequently, for every (q, σ, ψi , b, q  ) ∈ Δ ,a transition δi = (q, σ, gi , b, q  ) is added to ΔH . This determines the transitions between
locations in H and hence finishes the construction. The partition function P (·) is takenfrom [4], and also similar to that used for learning symbolic automata [9]. Note thecondition ω · (σ, 0) ∈ S ∪ S+ ∪ R in Definition 5 enforces μ0 = 0 below.
Definition 9 (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 for all
1 ≤ i, j ≤ n, let μn+1 = ∞, then a partition function P (·) mapping  to a set ofintervals {g0 , g1 , . . . , gn }, which is a partition of R≥0 , is defined as⎧[μi , μi+1 ),if μi ∈ N ∧ μi+1 ∈ N;⎪⎪⎪⎨(μ , μ ),if μi ∈ R≥0 \N ∧ μi+1 ∈ N;
i
i+1
gi =
⎪
if μi ∈ N ∧ μi+1 ∈ R≥0 \N;[μi , μi+1 ],⎪⎪⎩(μi , μi+1 ], if μi ∈ R≥0 \N ∧ μi+1 ∈ R≥0 \N.

Active Learning of One-Clock Timed Automata Using Constraint Solving

259

Algorithm 1: Learning DOTA using constraint solving
1
2
3
4
5
6
7
8
9

input : an observation table O = (S, S+ , R, E, f, N ), the alphabet Σ.
output: an automata H recognizing the target language L.
S ← {}, S+ ← ∅, R ← {(σ, 0) | σ ∈ Σ}, E ← {}, N ← 1 ;// initialization
while doO ← move to S(O);flag, M ← SMT(C1 ∧ C2 ∧ C3 ∧ C4 ) ;// solve constraints to get model M
if flag = thenH ← build hypothesis(O, M ) ;// build H from table O and model M
equivalent, ctx ← equivalence query(H);if equivalent = thenreturn H ;// success
else

10
11
12

else

O ← ctx processing(O, ctx ) ;// counterexample processing

15

flag, M  ← SMT(C1 ∧ C2 ∧ C3 ∧ C4 ) ;// solve relaxed constraints
if flag = thenO ← move to S+ (O, M ) ;// modify table O guided by solution M 

16

else

13
14

17

N ←N +1;// try for larger number of locations

Since the table O with the feasible assignments satisfies the readiness constraints,
the constructed hypothesis is a deterministic one-clock timed automaton, and agrees
with accepting information for rows in S ∪ S+ ∪ R. This is stated as the following
theorem.
Theorem 1. Given observation table O = (S, S+ , R, E, f, N ) and feasible assignments to bω and qω , the hypothesis H = (Σ, Q, q0 , F, c, Δ) is deterministic. For eachrow ω ∈ S ∪ S+ ∪ R, H accepts the timed word ω iff MQ(ω) = +. Finally, for any tworows ω1 , ω2 ∈ S ∪ S+ ∪ R, if the value of f on ω1 , ω2 and the setting of reset variables
b is ⊥, then qω1 = qω2 , and the two rows reach distinct locations in H.
After the hypothesis H is built, it is sent for an equivalence query. If the teacher
returns a counterexample ctx, the learner adds all prefixes of ctx to R during counterexample processing.
3.5 Main Algorithm and Correctness
The overall procedure of the algorithm is given in Algorithm 1. The observation tableO = (S, S+ , R, E, f, N ) is initialized with S = {}, S+ = ∅, R = {(σ, 0) | σ ∈ Σ},
E = {}, and N = 1. The function move to S tests each row in R to see if it is certainly
distinct (according to Definition 6) from each row in S. If so the certainly distinct row
is moved to S. For each row ω moved to S, ω · (σ, 0) is added to R for every σ ∈ Σ(Line 3). After that, the formula C1 ∧ C2 ∧ C3 ∧ C4 is built and sent to an SMT
solver (Line 4). If a solution M is found for the ending reset and location variables,
then a hypothesis H is constructed from the table O and the solution M (Line 6), andan equivalence query is performed to determine whether the hypothesis H is correct. If
the answer is positive, the algorithm returns with automaton H (Line 9). Otherwise, the260

R. Xu et al.

learner updates the table O by adding all prefixes of the returned counterexample ctx
to R (Line 11), and begins a new iteration starting from finding certainly distinct rows
(Line 3) and updating constraints. Note that new suffixes may be added to E during thecomputation of constraint C2 . If two timed words ω1 · (σ, t1 ) and ω2 · (σ, t2 ) end in
the same region under some choice of resets, ω1 and ω2 are currently indistinguishable
under this choice, but ω1 · (σ, t1 ) and ω2 · (σ, t2 ) can be distinguished with suffix e ∈ E,
then the timed word (σ, min(t1 , t2 )) · e is added to E. This allows us to distinguish ω1and ω2 directly using (σ, min(t1 , t2 )) · e ∈ E. After new suffixes are added to E, theentire observation table need to be updated, with possible new distinguishable pairs andnew rows added to S.
If there is no solution to C1 ∧ C2 ∧ C3 ∧ C4 , then the learner first relaxes C3 to C3
(Line 13). It is now permitted that some rows in R are assigned to a location different
from any row in S ∪ S+ . If there is a solution for the relaxed condition, it indicates thatsome row in R may represent a new location, even though it is not certainly distinct
from all rows in S. The function move to S+ moves such rows from R to S+ , and add
ω · (σ, 0) to R for each σ ∈ Σ and each ω moved to S+ (Line 15). If there is no solution
even for the relaxed constraints, the learner increases N by 1 (Line 17), attempting tofind a model with larger size.
Example 4. In the observation table in Fig. 2, each cell at row ω1 and column ω2 records
at which choice of resets ω1 and ω2 cannot be distinguished, as an expression in termsof bω ’s. For example, the expression  means ω1 and ω2 cannot be distinguished for
all choice of resets, while ⊥ means ω1 and ω2 are certainly distinct.
Constraint 3 (Closedness) requires that each row in R is represented by some row
in S ∪ S+ . Although ω3 = (a, 4) or ω5 = (a, 4)(a, 5.5) can be represented by  bysetting b3 =  or b5 = ⊥, they are known to be certainly distinct from each other(indicated by the red ⊥ in the table), so they cannot be both represented by . This means
C1 ∧ C2 ∧ C3 ∧ C4 is not satisfiable, so we relax the constraint to C1 ∧ C2 ∧ C3 ∧ C4 .
This is solvable by setting b3 = , and let ω5 represent an additional location. Then ω5
is moved to S+ , and the candidate DOTA at the right of Fig. 2 can be constructed fromthe updated observation table.

Analysis of the Algorithm. The algorithm is sound since it returns an automaton only if
it passes equivalence queries. The termination of the algorithm can be explained througha comparison with a brute-force search version of the algorithm similar to the normal
teacher case in [4]. The brute-force search constructs a binary tree of observation tables,with each branching corresponds to a choice of reset for some row in S ∪ R (here S+ is
not needed since reset information is now certain). Our algorithm simulates a breadthfirst search on the tree based on the number of locations. Rows in S+ can be viewed
as rows that are added to S in some (but not all) branches of the search tree. A simple
estimate for the number of rows in S ∪ S+ , and hence in R gives an exponential worstcase bound in terms of N . However, in practice it usually increases slowly as shown in
our experiments.
Theorem 2 (Correctness and termination). Algorithm 1 always terminates andreturns a correct DOTA recognizing the underlying target timed language.

Active Learning of One-Clock Timed Automata Using Constraint Solving

261

4 Extension to Deterministic Timed Mealy Machines
For practical applications on real-time reactive systems with input/output behavior, weconsider a timed version of Mealy machines. Inspired by Mealy machine with one timer(MM1T) [21], we divide the actions in Σ into input and output actions. The special
empty action  represents the invisible action or nothing happening. We assume that
there is a pair of input and output actions on each transition. Hence, the model can also
be viewed as a Mealy machine with one clock.
Definition 10 (Timed Mealy Machines). A timed Mealy machine (TMM) is a 6-tuple
M = (Q, I, O, q0 , c, Δ), where Q is a finite set of locations; I is a finite set of inputs,
containing the special empty action ; O is a finite set of outputs, containing the special
empty action ; q0 is the unique initial location; c is the single clock; and Δ ⊆ Q × I ×O × Φc × B × Q is a finite set of transitions.
A transition δ = (q, i, o, φ, b, q  ) allows a jump from q to q  and generates an output
o when provided input i ∈ I and if φ ∈ Φc is satisfied. Meanwhile, clock c is reset
to zero if b = , and remains unchanged otherwise. Given a timed word over inputs
ω = (i1 , t1 )(i2 , t2 ) · · · (in , tn ) ∈ (I × R≥0 )∗ , a deterministic timed Mealy machine(DTMM) M returns at most one output sequence M(ω) = o1 o2 · · · on . Given two
DTMMs M1 and M2 , for any timed word ω over inputs I, if the output sequences of
two DTMMs are equal, i.e., M1 (ω) = M2 (ω), then the two DTMMs are equivalent,denoted as M1 ≈ M2 . We modify the learning algorithm to take into account of
inputs and outputs. By the same argument as for DOTAs, we can show correctness andtermination of the learning algorithm for DTMMs.
Theorem 3 (Correctness and termination for learning DTMMs). The learningalgorithm for DTMMs always terminates and returns a correct DTMM.

5 Implementation and Experiments
To investigate the efficiency and scalability of our methods, we implemented a prototype in Python named SL for both DOTAs and DTMMs based on the tool provided
in [4]. We use Z3 [14] as the constraint solving engine. We describe some detailed
aspects of the implementation below. The implementation and models used for experiments are available at https://github.com/Leslieaj/DOTALearningSMT.
Incremental solving Our implementation takes advantage of incremental SMT solving functionality in Z3. This allows Z3 to reuse information from previous calls toaccelerate the solving process. For each query, we push a backtracking point after
adding all new constraints in C1 ∧ C2 ∧ C4 , then insert the constraints C3 or C3
depending on the stage of the algorithm. After the query finished, we pop to theprevious backtracking point, hence removing C3 or C3 before the next query.
Sink location We use a sink location to denote timed behaviors that are invalid or nondescribed, and it is sometimes possible for membership queries to return whether
a timed word reached a sink location. Our implementation takes advantage of thisinformation when it is available. This results in a significant acceleration of the learning process. The technique has been introduced in the previous work [4].

262

R. Xu et al.
Table 1. Experimental results on DOTAs.
Group|Δ| Method #Membership
Nmin

Nmean

|QH | #Learnt t(s)#Equivalence
Nmax

Nmin Nmean Nmax

11.9 DOTAL

73

348.3

708 10

16.7

30

5.6

7/10

SL

104

1894.83929 11

20.8

35

5.6

10/10

0.78

4 4 2016.3 DOTAL

231

317.0

564 27

30.8

40

4.0

6/10

100.22SL

1740

3497.75329 24

32.8

42

4.0

10/10

1.42

7 4 2026.0 SL

6092

9393.3 15216 44

51.5

69

7.0

10/10

2.90

10 4 2039.1 SL8579 16322.3 23726 59

76.5

93

10.0

10/10

5.89

12 4 2047.6 SL13780 20345.5 29011 70

88.0 102

12.0

10/10

10.05

14 4 2058.4 SL

14.69

6 2 1039.88

18915 28569.0 40693 92

110.6 126

14.0

10/10

AKM (17 12 5) 40.0 SL

3453

3453.03453 49

49.0

49

12

1/1

7.19

22.0 SL

4713

4713.04713 32

32.0

32

20

1/1

19.04

CAS (14 10 27) 23.0 SL

4769

4769.04769 18

18.0

18

14

1/1

126.30TCP (22 13 2)

PC (26 17 10) 42.0 SL
10854 10854.0 10854 28
28.0 28 25
1/1
109.01
Group: each group has ID of the form |Q| |Σ| κ, where |Q| is the number of locations, |Σ| is the size of thealphabet, and κ is the maximum constant appearing in the clock constraints. |Δ|: average number of transitionsof a DOTA in the corresponding group. Method: DOTAL and SL represent the method in [4] and our method
respectively. #Membership & #Equivalence: number of membership and equivalence queries, respectively.
Nmin : minimal, Nmean : mean, Nmax : maximum. |QH |: average number of locations of the learned automata foreach group. #Learnt: the number of the learnt DOTAs (learnt/total). t: average wall-clock time in seconds.

Equivalence query Equivalence between timed automata with one clock is decidable.
We implemented an equivalence query oracle based on [15], but simplified for thedeterministic case. In actual applications when the target automaton is unknown, thiscan be usually replaced by techniques based on conformance testing.
We evaluated our prototype tool on two benchmarks that are previously used in [4]and [21]. They respectively contain hundreds of randomly generated DOTAs and several models from practical applications which are in the form of DOTAs and MM1Ts.
The models from practical applications consist of the abstract automata of an Authentication and Key Management service of the WiFi (AKM), the functional specification of
TCP protocol, a car alarm system (CAS), and a particle counter (PC). All experiments
have been carried out on an Intel Core i7-9750H @ 2.6 GHz processor with 16 GB
RAM running Ubuntu 20.04 Linux system.
5.1

Experiments on DOTAs

We first compared the performance of our learning algorithm SL with the algorithm
DOTAL of [4] in the normal teacher setting (see Sect. 2). In [4], the generated random
DOTAs are up to 14 locations, but the algorithm only managed to learn automata withup to 6 locations. The examples are divided into different groups depending on thenumber of locations, number of actions, and maximum clock value in guards. Eachgroup contains ten automata. Moreover, we tested translations of practical models to
DOTA provided in [21]. The experimental results are shown in Table 1.
The algorithm DOTAL fails in all of the larger examples due to time and memory limits. Hence, we omit them in the table. In the two groups of smaller examples

Active Learning of One-Clock Timed Automata Using Constraint Solving

263

Table 2. Experimental results on DTMMs and MM1Ts.
Case

DTMM
SL
|Q| |I| |Δ| #M

MM1T
MM1T-L∗M [21]#E t(s) |Q| |I| |Δ| #R #I
t(s)

AKM 5

5

28

691

34 2.6

4

TCP

11

8

19

751

10 1.9

11

CAS

8

4

17

1654 21 17.1 8

AKM 8

8

24

1194 27 6.8

8

8

5

24

5361 29693 5070.4

8

19

401

1868

65.7

4

17

494

2528

79.5

24

392

1864

85.1

6 2 10 and 4 4 20, the algorithm DOTAL can learn some of the cases. In the comparison between number of membership and equivalence queries, we see that SL takes
about the same number of equivalence queries, and several times more membership
queries. This is likely due to the fact that we exhaustively test all pairs of rows in thetable under all reset conditions. However, the algorithm SL is scalable to much larger
examples than DOTAL. SL also successfully learns the DOTA models of four practicalapplications which are all bigger than the randomly generated DOTAs, and far above
the ability of the DOTAL algorithm. This shows the potential of SL in real applications.
5.2 Experiments on TMMs
We also evaluated our learning algorithm for timed Mealy machines. We first transformed the four MM1T models to DTMMs. As shown in Table 2, for each practicalapplication, its DTMM model is more succinct than the corresponding DOTA modelin Table 1. The size of the DTMM model is also comparable to the size of the MM1T
model (the two are equal except the AKM case).
We then run our learning algorithm SL on these models. Compared to learning
the corresponding DOTA, learning DTMM takes fewer membership and equivalence
queries, except for taking more equivalence queries in the case CAS. Hence, we find
DTMMs to be more suitable for learning timed reactive systems than DOTAs. We also
run the experiment on MM1T using the algorithm MM1T-L∗M . As reported in [21], theperformance is evaluated according to the total number of resets to the system underlearning (SUL) #R and the total number of the performed input actions #I. As these
are not directly comparable to number of membership and equivalence queries, we list
the results side-by-side in the table. Note also that their implementation is based on
LearnLib [13] and uses a random word equivalence oracle with 1000 tests, while we
conduct an exact equivalence checking. The computation time is listed to show that our
method can learn the examples efficiently, but the computation times are not directlycomparable across methods with different ways to conduct equivalence queries. We
also note that [21] showed experimentally that the algorithm MM1T-L∗M compares
favorably against heuristic learning methods based on genetic programming [1, 18].

6 Conclusion
In this paper, we proposed a new algorithm for active learning of deterministic oneclock timed automata and timed Mealy machines, using constraint solving based on

264

R. Xu et al.

SMT solving to determine resets and location assignments. This takes advantage of theability of SMT to solve large constraint systems efficiently, allowing the algorithm toscale up to much larger timed automata models.
In future work, we wish to consider extension of the algorithm to learning timed
automata with multiple clocks as well as the non-determinstic case. We wish to also
consider incorporating ideas from algorithms such as TTT in order to improve efficiency, in particular reducing the number of membership queries.

References
1. Aichernig, B.K., Pferscher, A., Tappler, M.: From passive to active: learning timed automata
efficiently. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS,
vol. 12229, pp. 1–19. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-55754-6 1
2. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
3. 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)
4. An, J., Chen, M., Zhan, B., Zhan, N., Zhang, M.: Learning one-clock timed automata. In:
TACAS 2020. LNCS, vol. 12078, pp. 444–462. Springer, Cham (2020). https://doi.org/10.
1007/978-3-030-45190-5 25
5. An, J., Wang, L., Zhan, B., Zhan, N., Zhang, M.: Learning real-time automata. Sci. China
Inf. Sci. 64(9), 1–17 (2021). https://doi.org/10.1007/s11432-019-2767-4
6. An, J., Zhan, B., Zhan, N., Zhang, M.: Learning nondeterministic real-time automata. ACM
Trans. Embed. Comput. Syst. 20(5s), 1–26 (2021)
7. Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2),87–106 (1987)
8. Dima, C.: Real-time automata. J. Automata Lang. Comb 6(1), 3–23 (2001)
9. 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
10. Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theor.
Comput. Sci. 411(47), 4029–4054 (2010)
11. Grinchtein, O., Jonsson, B., Pettersson, P.: Inference of event-recording automata using
timed decision trees. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137,
pp. 435–449. Springer, Heidelberg (2006). https://doi.org/10.1007/11817949 29
12. Henry, L., Jéron, T., Markey, N.: Active learning of timed automata with unobservable
resets. In: Bertrand, N., Jansen, N. (eds.) FORMATS 2020. LNCS, vol. 12288, pp. 144–160.
Springer, Cham (2020). https://doi.org/10.1007/978-3-030-57628-8 9
13. Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib - a framework for active
automata learning. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp.
487–495. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4 32
14. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J.
(eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3 24
15. Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: closing a
decidability gap. In: LICS 2004, pp. 54–63 (2004)
16. Smetsers, R., Fiterău-Broştean, P., Vaandrager, F.: Model learning as a satisfiability modulo
theories problem. In: Klein, S.T., Martı́n-Vide, C., Shapira, D. (eds.) LATA 2018. LNCS,
vol. 10792, pp. 182–194. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-773131 14

Active Learning of One-Clock Timed Automata Using Constraint Solving

265

17. Steffen, B., Howar, F., Merten, M.: Introduction to active automata learning from a practicalperspective. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 256–296.
Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21455-4 8
18. 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, Cham (2019). https://doi.org/10.1007/978-3-030-29662-9 13
19. Tappler, M., Aichernig, B.K., Lorber, F.: Timed automata learning via SMT solving. In:
Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods. LNCS, vol. 13260,
pp. 489–507. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-06773-0 26
20. Vaandrager, F.W.: Model learning. Commun. ACM 60(2), 86–95 (2017)
21. Vaandrager, F., Bloem, R., Ebrahimi, M.: Learning mealy machines with one timer. In: Leporati, A., Martı́n-Vide, C., Shapira, D., Zandron, C. (eds.) LATA 2021. LNCS, vol. 12638,
pp. 157–170. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-68195-1 13
22. Verwer, S., de Weerdt, M., Witteveen, C.: One-clock deterministic timed automata are efficiently identifiable in the limit. In: Dediu, A.H., Ionescu, A.M., Martı́n-Vide, C. (eds.) LATA
2009. LNCS, vol. 5457, pp. 740–751. Springer, Heidelberg (2009). https://doi.org/10.1007/
978-3-642-00982-2 63
23. Verwer, S., de Weerdt, M., Witteveen, C.: The efficiency of identifying timed automata andthe power of clocks. Inf. Comput. 209(3), 606–625 (2011)
24. Verwer, S., de Weerdt, M., Witteveen, C.: Efficiently identifying deterministic real-time
automata from labeled data. Mach. Learn. 86(3), 295–333 (2011). https://doi.org/10.1007/
s10994-011-5265-4