Learning Deterministic One-Clock Timed
Automata via Mutation Testing
Xiaochen Tang1 , Wei Shen1 , Miaomiao Zhang1(B) , Jie An2 ,Bohua Zhan3,4 , and Naijun Zhan3,4
1

School of Software Engineering, Tongji University, Shanghai, China{xiaochen9697,weishen,miaomiao}@tongji.edu.cn
2
Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
3
State Key Laboratory of Computer Science, Institute of Software,
CAS, Beijing, China
4
University of Chinese Academy of Sciences, Beijing, China
Abstract. In active learning, an equivalence oracle is supposed toanswer whether a hypothesis model is equivalent to the system underlearning. Its implementation in real applications is considered a majorbottleneck for active automata learning. The problem is especially diﬃcult in the context of learning timed automata due to the inﬁnitely large
state space involved. In this paper, following the framework of combining mutation analysis and random testing, we propose an implementationof equivalence oracle in the context of learning deterministic one-clock
timed automata (DOTAs). This includes two learning-friendly mutation
operators, a heuristic test-case generation method, and a score-based
test-case selection method. We implemented a prototype applying ourapproach by extending an existing tool on active learning of DOTAs andconducted extensive experiments. The results indicate that our method
improves upon existing methods on the rate of learning correct models,
the number of test cases required, and accumulated delay time in test
cases.
Keywords: Active learning · Timed automata · Model-based
mutation testing1

Introduction

Active (model) learning [28] has emerged as a highly eﬀective technique for learning the model of a system under learning (SUL). Most of active learning methods follow the L∗ framework proposed by Angluin [12]. The learning process toachieve a hypothesis of the SUL can be viewed as an interaction between a learnerand a teacher, where the learner asks membership queries (MQs) and equivalence
queries (EQs) to a teacher who holds oracles to answer these queries. The former
corresponds to a single test of the SUL to check whether a sequence of actions
This work has been partially funded by NSFC under grant No. 61972284, 62032019,
62032024, 62192732, 62192730, and 61625206, 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. 233–248, 2022.
https://doi.org/10.1007/978-3-031-19992-9_15

234

X. Tang et al.

can be executed. EQs check whether a learned hypothesis represents the SUL.
The teacher either answers aﬃrmatively or generates a counterexample showing
the diﬀerence between the SUL and the hypothesis. Compared to active learningof deterministic ﬁnite state automata (DFAs) [12], learning timed automata [7] ismuch more complex since it involves an inﬁnite set of timed actions and clock reset
information while the alphabets of DFAs is ﬁnite. Among the existing works [8–10,16,17,29] on active learning of the diﬀerent timed models, An et al. proposed
an active learning method for deterministic one-clock timed automata (DOTAs)
in [8]. Inherited from L∗ , this method also assumes an ideal setting where the EQs
can be answered exactly by an oracle. However, exact equivalence oracles are usually unrealistic in most practical situations, which is a well-known problem thatlearning methods based on L∗ in practice face and can be considered as “the true
bottleneck of automata learning” [13].
To address the issues mentioned above, various attempts have been carriedout. For real applications, one of the most widely studied approach for EQs
is conformance testing [1,13–15,22,25]. However, the size of the constructed
test suite is usually exponential in the number of states of the SUL, whichmakes it ineﬃcient in many industrial scenarios. Another limitation is that mostof the existing methods for timed systems do not consider the accumulateddelay time of test suites. Therefore, a new target for conformance testing is toﬁnd counterexamples fast, rather than trying to prove equivalence [19]. Modelbased testing [27], a popular technique for automated test-case generation, canbe used as an approach for conformance testing. Commonly relying on somecoverage criterion, it produces new test cases until that criterion is satisﬁed.
Model-based mutation testing [2,3,23] uses faults as such a criterion: the originalmodel is modiﬁed by diﬀerent fault injections, called mutation operators, which
results in a set of faulty models called mutants. In [6], Aichernig et al. combined
random testing and mutation analysis [11] to learn Mealy machines and show
their eﬀectiveness. Here random testing is used to achieve high variability oftests, while mutation analysis is used to ensure appropriate coverage.
In this paper, we propose a conformance testing approach combining random
testing and mutation-based testing to replace exact EQs in the active learningof DOTAs. Even though many existing studies proposed mutation operators fortimed automata, which generate mutants covering speciﬁc faults [4,26,31], there
are many redundancies among these mutation operators, and the mutants generated by these operators are possibly non-deterministic. These make the existing
mutation operators not well-suited to the context of active automata learning.
Thus, we design two mutation operators to address DOTAs learning. The approach we presented aims at ﬁnding counterexamples quickly, and reducing thetotal amount of time of executing test cases, in addition to the reduction of tests
as in [6]. Moreover, to design the test suits, we take previous counterexamples
into consideration and the modiﬁcations between two successive hypotheses in
the learning procedure for DOTAs. Our contributions are summarized as follows.
– A heuristic algorithm for random test-case generation. We take counterexamples into consideration and apply three heuristics to random testing, aiming
at generating more useful test cases.

Learning Deterministic One-Clock Timed Automata via Mutation Testing235– Two learning-friendly mutation operators. In contrast to generating only ﬁrstorder mutants [4,26,31], which usually contain one fault, we take into accountthe deterministic behaviours of the model and the modiﬁcations between two
successive hypotheses obtained in the learning process, so that more faults
are considered in the construction of mutants.
– A mutation and score-based selection of test cases. In addition to mutation
coverage, we also take the length and accumulated delay time of the test cases
into consideration to achieve faster testing.
– An implementation of our method. To investigate the eﬀectiveness and eﬃciency of our method, we extend the prototype tool for DOTAs learning [8]and compare our method with various existing methods.
The rest of the paper is organized as follows. In Sect. 2, we review the learningalgorithm for DOTAs in [8] and the model-based mutation testing framework. In
Sect. 3, we describe the mutation-based testing in the context of active learningof DOTAs in detail. In Sect. 4, we introduce two mutation operators used in
the mutation-based testing framework. The experimental results are reported in
Sect. 5. Finally, Sect. 6 concludes this paper.

2

Preliminaries

2.1

Deterministic One-Clock Timed Automata

In this paper, we consider a subclass of timed automata [7] that are deterministic
and contain only a single clock, called Deterministic One-Clock Timed Automata(DOTAs). Let N be the natural numbers and R≥0 be the non-negative real
numbers. We use  to stand for true and ⊥ for false. Let B = {, ⊥}. Letc be the clock variable, denote by Φc the set of clock constraints of the form
φ:: =  | c  m | φ ∧ φ, where m ∈ N and  ∈ {=, <, >, ≤, ≥}.
Definition 1 (One-clock timed automata). A one-clock timed automaton(OTA) is a 6-tuple A = (Σ, Q, q0 , F, c, Δ), where Σ is a finite set of actions,
Q is a finite set of locations, q0 is the initial location, F ⊆ Q is a set of final
locations, c is the unique clock and Δ ⊆ Q × Σ × Φc × B × Q is a finite set oftransitions.
A transition δ ∈ Δ is a 5-tuple (q, σ, φ, b, q  ), where q, q  ∈ Q are the source
and target locations respectively, σ ∈ Σ is an action, φ ∈ Φc is a clock constraint,
and b is the reset indicator. Such δ allows a jump from q to q  by performing anaction σ if the current clock valuation ν satisﬁes the constraint φ. We also call φas a guard. 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 nonnegative real number to the clock. For t ∈ R≥0 , let ν + t be the clock valuation
with (ν + t) (c) = ν (c) + t. A state is a pair (q, ν), where q ∈ Q and ν is a clock
valuation. A timed action is a pair (σ, t) that indicates the action σ is applied
after t time units since the occurrence of the previous action. A timed trace is a

236

X. Tang et al.

sequence ω = (σ1 , t1 ) (σ2 , t2 ) . . . (σn , tn ) of timed actions (σi , ti ) ∈ Σ × R≥0 . A
ﬁnite run ρ of A over a timed trace ω = (σ1 , t1 ) (σ2 , t2 ) . . . (σn , tn ) is a sequence
σ1 ,t1σ2 ,t2
σn ,tnof timed states and timed actions ρ = (q0 , ν0 ) −→ (q1 , ν1 ) −→ · · · −→ (qn , νn )where ν0 = 0, and for all 1 ≤ i ≤ n there exists a transitions (qi−1 , σi , φi , bi , qi ) ∈Δ such that νi−1 + ti satisﬁes φi , and νi (c) = 0 if bi = , νi (c) = νi−1 (c) + ti
otherwise. Since time values ti represents delay times, we call such a timed trace
a delay-timed word. The delay-timed word is observed outside from the view ofthe global clock. On the other hand, the behavior can also be observed insidefrom 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 or bi−1 = , otherwise
μi = μi−1 + ti . The time spent in a timed trace ω, denoted time(ω) is the sumof all delays in ω, for example, time() = 0 and time((a, 1.0)(b, 1.5)) = 2.5.
Definition 2 (Deterministic OTA). An OTA is a deterministic one-clock
timed automaton (DOTA) if there is at most one run for a given timed word.
A DOTA A is complete if for any location q and action σ, the constraints forma partition of R≥0 . Any incomplete DOTA A can be transformed into a complete DOTA accepting the same timed language by adding a non-accepting sinklocation qsink , and adding transitions to the sink location for each unavailable
action [8]. We therefore assume that we are working with complete DOTAs.
2.2

Active Learning Algorithm for DOTAs

In this section, we provide a brief description of the active learning algorithm [8]for a black-box SUL which can be represented by a DOTA A. The existing
work distinguishes two learning scenarios: learning from a normal teacher or asmart teacher. As the work in this paper concerns EQs only, it applies to bothnormal teacher and smart teacher scenarios. For the experiments, we mainly
consider the case of smart teachers. In practical applications, this corresponds
to executing the test case, where information about clock-resets is known bycode instrumentation or watchdogs (refer to the concept of testable systems in[15,18]). The learner maintains an observation table to collect the answers of
MQs. The table will be transformed to a DOTA H as a hypothesis if it satisﬁes
several preparedness conditions. The learner then performs an EQ by submitting
H to the teacher. In theory, we assume that the teacher holds an equivalenceoracle to answer EQs, returning whether the timed languages of H and A are
equivalent. If the answer is no, the teacher also returns a logical-timed wordwith reset information as a counterexample. The learner then performs more
MQs guided by the counterexample. The learning loop terminates when an EQ
returns a positive answer. We refer to [8] for more details.
However, since such equivalence oracles may not exist in practical situations,the equivalence oracle is often achieved through conformance testing, i.e., asking
a lot of MQs to answer a single EQ. If, for every MQ, the output producedby the SUL is consistent with hypothesis H, the answer to the EQ is “Yes”.
Otherwise, the answer “No” is provided, together with a counterexample that

Learning Deterministic One-Clock Timed Automata via Mutation Testing237

indicates a diﬀerence between H and the SUL. In this paper, we address theimplementation of equivalence oracle through a combination of random testing
and mutation analysis.
2.3

Model-Based Mutation Testing

Model-based mutation testing [2,3,23] is a promising technique combining thecentral ideas of mutation testing [21] and model-based testing [27]. By making some adaptions, it can be regarded as an equivalence oracle in the context
of active learning. The process starts with the current hypothesis H. A set ofmutants from H are generated by mutation operators. Once all mutants are created, the actual test suite generation starts. The original H is compared to eachmutant via an equivalence check (this can be done exactly since models for both
H and the mutant are available). If a mutant M is not equivalent to H, thechecking procedure returns a trace that serves as a witness, and this trace canbe converted into a test case.
The equivalence checks in the above process can be computationally expensive. Therefore, the work in [6] considers a new model-based mutation testing
framework combined with random testing for learning Mealy machines, and theexperiments have demonstrated that a combination of random exploration andmutation-based test-case generation is beneﬁcial. Brieﬂy, the framework includes
the following steps to generate test suites for conformance testing. First, it utilizes random testing to generate a large set of test cases T. Then it analyzes
the mutation coverage of each test case in T, i.e., it executes each test case anddetermines which of the mutants produces outputs diﬀerent from H. Finally, thetest suite is created by selecting a subset of T based on the computed mutation
coverage. After that, the conformance testing between H and the SUL can be
conducted by executing test cases of the test suite on both respectively. The test
case producing diﬀerent outputs between H and the SUL is a counterexample
to the equivalence, which is utilized to further reﬁne the current hypothesis H.

3

Mutation-Based Testing for DOTAs

In this section, we introduce our mutation-based testing process for solving theEQs in learning DOTAs. We ﬁrst describe the whole process and then present
the heuristic method to generate test cases and the mutation-based selection of
the test suite. The details on the mutation operators and mutation generation
are described in Sect. 4.
3.1

The Process Overview

Following the idea in [6], we use a combination of random testing, to achieve
high variability of tests, and mutation analysis, to address coverage appropriately. However, given the particular characteristics of DOTAs learning, that is,counterexample processing will generate two kinds of modiﬁcations between two

238

X. Tang et al.

Fig. 1. The overview of mutation-testing-based equivalence checking for learning
DOTAs.

successive hypotheses, we have to design new mutation operators and adapt theframework accordingly. The whole process is depicted in Fig. 1. The input forthis process is a hypothesis H, a learned intermediate DOTA, while the output
is the answer of an EQ.
1. From the model H, we ﬁrst develop a heuristic test-case generation algorithm
to obtain a large set of test cases T (see Sect. 3.2).
2. Independently, we generate a set of mutants M from H based on the timed
mutation operator (see Sect. 4.1) and the split-location mutation operator(see Sect. 4.2).
3. Using a score-based test-case selection method, together with mutation analysis, a subset Tsel of T is selected (see Sect. 3.3). The purpose is to select a
subset of test cases from T that are likely to distinguish between the original
hypothesis H and the mutants as the test suite to execute, i.e. to select thetest cases that cover the mutants.
4. Finally, we execute all test cases in Tsel on the hypothesis H and the SUL
respectively. A test case is a counterexample if producing diﬀerent outputs
on the SUL and H. If such a counterexample is found, it is returned to thelearning algorithm. Otherwise, the EQ returns a positive answer.
Diﬀerent from [6] using only one mutation operator for generating mutants,
we hereby use two mutation operators to cover the diﬀerent possibilities of mutations for timed automata. This produces a set of mutants helpful for generating
a more complete test suite that is able to ﬁnd potential diﬀerences between H
and the SUL. Our experiments have shown that both mutation operators arenecessary for improving the rate of learning the correct model of the SUL. In
addition, to avoid interleaving complexity, instead of simultaneously using two
mutation operators to generate test cases, we divide the process into two phases
using two operators respectively. In our case, we choose to ﬁrst use the timed

Learning Deterministic One-Clock Timed Automata via Mutation Testing239

Algorithm 1. Heuristic test-case generation
Input: hypothesis H = (Σ, Q, q0 , F, c, Δ);
the previous counterexample ctx;
the maximal length len of “xy”
part of a test case; three probability values pstart , pvalid and pstop .
Output: a test case t.
1: t ← ;
2: qc ← q0 ; ν ← 0;
3: Qvisited ← ∅;4: if prob(pstart ) then t ← ctx;
5:for i ← 0 to |ctx| − 1 do
6:
qc , ν ← execute((qc , ν), ctx[i]);7:
Qvisited ← Qvisited ∪ {qc };8: while |t| < len do
9:
if prob(pvalid ) then10:Δ ← {δ|δ = (q, σ, φ, b, q  ) ∈Δ ∧ q = qc ∧ q  = qsink };

11:

else

Δ ← {δ|δ = (q, σ, φ, b, q  ) ∈Δ ∧ q = qc ∧ q  = qsink };
13:
if Δ = ∅ then14:(q, σ, φ, b, q  ) ← getRandom(Δ );15:
t ← getRandomDelay(ν, φ);16:
if t = None then17:t ← t · (σ, t);
18:
qc , ν ← execute((qc , ν), (σ, t));19:
Qvisited ← Qvisited ∪ {qc };20:
if prob(pstop ) then21:
break;
22: if Q\Qvisited = ∅ then23:
qt ← getRandomLocation(Q\Qvisited );24:
ω ← findTimedTrace((qc , ν), qt );25:
if ω =  then26:t ← t · ω;
27: return t;

12:mutation operator only, and if no counterexample is found, then use the splitlocation mutation operator and repeat Step 2 to Step 4.
3.2

Heuristic Test-Case Generation

Random testing is a widely-used method and has been integrated in the learning
library LearnLib [20] as an EQ method for untimed models. In this section, weapply three heuristics to generate test cases randomly, aiming at generating
more useful test cases. Algorithm 1 presents the generation process, containing
three main steps corresponding to the heuristics. The inputs include the current
hypothesis H and several relevant parameters, and the output is a test caset ∈ (Σ × R≥0 )∗ of the form xyz, where x is the preﬁx, y a random sequence of
timed actions, and z the suﬃx. Function prob(p) returns true with probability
p and false with probability 1 − p. The generation process is performed manytimes to generate a large-size (can be parameterized by the user) test set T,
whose size is related to the number of actions and transitions, and the timing
parameters of H (see Sect. 5).
1. Firstly, according to our observation that a counterexample is often preﬁxed
with its previous counterexample, we reuse the previous counterexample ctx
as the preﬁx x with probability pstart (Line 4 to Line 7).
2. Then, consider for many reactive systems, from the current timed state, randomly selecting an action is likely to transit to a sink location, since not all
timed actions can be executed or make sense at the current state. Therefore,
we prefer to explore non-sink locations with probability pvalid when using
random walking method to ﬁnd timed actions (σ, t). Such timed actions form
the segment y extending the test case (Line 8 to Line 21). The parameter len

240

X. Tang et al.

Algorithm 2. Mutation and score-based test-case selection
Input: M; TM for all M ∈ M;
Vt for all t ∈ T.
Output: a subset of test cases Tsel .
1: Tsel ← ∅;2: while M = ∅ do
3:
Mopt ← argmin M∈M |TM |;4:5:

if TMopt = ∅ and TMopt ∩ Tsel= ∅ then
topt ← argmax t∈TM Vt ;opt

6:
Tsel ← Tsel ∪ {topt };7:
M ← M\{Mopt };8: return Tsel ;limits the maximal length of the “xy” part. The exploring process stops withprobability pstop at the end of each round.
3. Finally, we add the path from the current location to a non-visited location
as suﬃx z to increase the coverage of each test case (Line 22 to Line 26).
3.3

Mutation and Score-Based Test-Case Selection

In order to improve the mutation coverage of test cases, we deﬁne a special
output function in response to a given delay-timed word. Let D = {+, −} be theoutput domain, indicating whether the trace is accepted (+) or not (−).
Definition 3 (Output function). Given a test case (delay-timed word) t =(σ1 , t1 ) (σ2 , t2 ) · · · (σn , tn ) and a (complete) DOTA A = (Σ, Q, q0 , F, c, Δ), corσ1 ,t1
σ2 ,t2
σn ,tnresponding a run ρ = (q0 , ν0 ) −→ (q1 , ν1 ) −→ · · · −→ (qn , νn ) in A, the output
function for the test case is defined as outA (t) = o1 o2 · · · on , where oi = + if
qi ⊆ F and oi = − otherwise.
Given two models A1 and A2 , we say t passes if out A1 (t) = out A2 (t), otherwise,
it fails and serves as a counterexample to the equivalence.
After the heuristic test-case generation described previously, we haveobtained a large-size test set T. However, it may contain just a small number of test cases that can be counterexamples due to the randomness. Therefore,
we further need to select a subset Tsel from T consisting of test cases that are
more likely to be counterexamples. Normally, the selection is based purely on akind of coverage, e.g. location or transition coverage. However, unlike testing for
Mealy machines [6,14] or other ﬁnite labeled transition systems, for timed systems, we should also consider the time elapsed in two consecutive input actions.
Therefore, the main objective in addition to the number of test cases is to reduce
the accumulated delay time of all test cases used in conformance testing, provided that the maximum mutant coverage is achieved. Our selection process isbased on a set of mutants of the hypothesis H. We leave the details of mutation
generation in Sect. 4 and suppose that a set of mutants M has been generated.
Algorithm 2 presents the mutation and score-based selection method, which
considers several factors of the test cases. At beginning, we need to prepare
the inputs. First, we associate each test case t ∈ T with a set of mutants Mt
covered by t, i.e. Mt = {M ∈ M | outH (t) = outM (t)}, and associate eachLearning Deterministic One-Clock Timed Automata via Mutation Testing241

mutant M ∈ M with a set of test cases TM ∈ T that can cover M, i.e.
TM = {t ∈ T | outH (t) = outM (t)}. Then, we use the following four attributes
to decide whether a test case t is selected: (1) time(t) is the total delay timeof t, (2) |t| is the length of t, (3) |Mt | is the mutation coverage of t, and (4)|Ct | is the transition coverage of t. After normalization for the attributes, we
acquire the score Vt = a · (1 − time(t) ) + b · (1 − |t| ) + c · |Mt | + d · |Ct | , wherea, b, c, d are the weights. Upon obtaining TM for each mutant M and Vt for eachtest case t, the algorithm follows the basic idea that the higher the score value,
the more likely the test case will be selected. So, at each round, ﬁrst select the
mutant M covered by the least number of test cases (Line 3). If the currently
selected test cases Tsel cannot cover it, the test case t with the largest score Vt
is chosen from TMopt and added to Tsel (Line 4 to Line 6). Then remove M
from M. The steps repeat until all mutants covered by at least one test case areconsidered, i.e. the selected test cases have been able to achieve the maximum
possible coverage of the mutant set. Mutants that cannot be covered by any test
case are removed by constraint TMopt = ∅ in Line 4.

4

Learning-Friendly Mutation Operators for DOTAs

In order to provide the mutants of hypothesis H for the processes in Sect. 3, weneed to design suitable mutation operators for DOTAs. Considering the learning
method in [8], we ﬁnd that counterexample handling will lead to generating two
kinds of modiﬁcations between the successive hypotheses H and H . Similar
to the terms used in [24], the ﬁrst is called expansive modification, which meansthat H has more locations and/or transitions than H. While the second is called
non-expansive modification, which implies that only the timed constraints and/or
the reset indicators of some transitions diﬀer between H and H . Inspired by theobservations, we design two mutation operators. The ﬁrst one is timed mutation
operator given in Sect. 4.1, which includes a series of mutation operations speciﬁc
to DOTAs learning, corresponding to the transition changes of the expansive andnon-expansive modiﬁcation. The second, split-loaction mutation operator given
in Sect. 4.2, is closely related to [6], corresponding to the location change of the
expansive modification. In terms of the two designed operators, all the mutants
generated from H are still deterministic automata.
4.1

Timed Mutation Operator

Given the current hypothesis H, the timed mutation operator is conducted
on every transition in turn to generate mutants. Consider a transition δ =(q, σ, φ, b, q  ), the basic idea is as follows. For the timed interval φ, we will ﬁrst
slice it into sub-intervals as a partition (see Deﬁnition 4), resulting in several
new transitions. Then we conduct two operations (see Deﬁnition 5) on each newtransition to generate mutants. One operation is to change the target locationof one transition, which helps us to modify the timed interval φ. The other operation is to change the reset indicator of one transition. Actually, we can also
apply the two operations to some transitions at the same time.

242

X. Tang et al.

Algorithm 3. Mutants generation via the timed mutation operator
Input: a DOTA H = (Σ, Q, q0 , F, c, Δ);
the greatest integer constant B;
a slicing step w.
OUTPUT: a set of mutants M.
1: M ← ∅2: for each δ = (q, σ, φ, b, q  ) ∈ Δ do3:
Δs ← {(q, σ, φs , b, q  ) | φs ∈Sg (φ, B, w)};for each δs ∈ Δs do
Δm ← rt(δs ) ∪ fl (δs )∪fl ◦ rt(δs );6:
for each δm ∈ Δm do
7:M ← (Σ, Q, q0 , F, c, Δ\{δ};∪Δs \{δs } ∪ {δm });8:
M ← M ∪ {M};9: return M;
4:
5:

Definition 4 (Slicing timed interval). Let B be the greatest integer constantappearing in the DOTA to be learned (can also be set by the user), and w ∈ N>0
be the slicing step. Given a timed interval α, β, where ∈ {(, [} and  ∈ {), ]},the slicing can generate a partition of α, β as follows:– If β > B (including β = ∞), Sg ( α, β, B, w)= { α, α + w) | α + w ≤ B} ∪ {[α + w ∗ i, α + w ∗ i] | α + w ∗ i ≤ B, i ∈ N>0 }∪ {(α + w ∗ i, α + w ∗ (i + 1)) | α + w ∗ (i + 1) ≤ B, i ∈ N>0 }∪ {(α + w ∗ i, β | α + w ∗ i ≤ B ∧ α + w ∗ (i + 1) > B, i ∈ N>0 }– If β ≤ B, Sg ( α, β, B, w)= { α, α + w) | α + w < β} ∪ {[α + w ∗ i, α + w ∗ i] | α + w ∗ i < β, i ∈ N>0 }∪ {(α + w ∗ i, α + w ∗ (i + 1)) | α + w ∗ (i + 1) < β, i ∈ N>0 }∪ {(α + w ∗ i, β | α + w ∗ i < β ∧ α + w ∗ (i + 1) ≥ β, i ∈ N>0 }Therefore, for a transition δ = (q, σ, φ, b, q  ) in H, φ is sliced into several
timed intervals Sg (φ, B, w). This implies that instead of δ, a new transition set
Δs = {(q, σ, φs , b, q  ) | φs ∈ Sg (φ, B, w)} with |Δs | = |Sg (φ, B, w)| is generated.
Obviously, if the slicing step w = 1, the intervals in Sg are regions [7].
Definition 5 (Timed mutation operations). Given a sliced transition δs =(q, σ, φs , b, q  ) ∈ Δs , the timed mutation operator includes the following two operations: (1) Re-target: rt(δs ) = {(q, σ, φs , b, q  ) | q  ∈ Q\q  }; (2) Flop-reset:fl (δs ) = {(q, σ, φs , b , q  ) | b ∈ B\b}.
Algorithm 3 presents the procedure generating mutants from H using thetimed mutation operator. First, for each transition δ, we build the sliced transition set Δs (Line 3). Second, for each sliced transition δs ∈ Δs , we conduct the
mutation operations rt and fl separately and both on it, and thus get a mutatedtransition set Δm (Line 5). Then, for each mutated transition δm ∈ Δm , we canbuild a mutant by removing δ, δs , and adding the new mutated transition δmto the transition set (Line 7). Therefore, every mutant is obtained from H via
the options of changing the timed constraints, or ﬂopping the reset indicator, or
adding new transitions, or a combination of the above three, so that the mutant
gets closer to the successor hypothesis H . To simplify a mutant, we merge twotransitions if they have the same source location, target location, action, andreset indicator respectively. For example, given two transitions (q, σ, [2, 4], b, q  )and (q, σ, (4, 5], b, q  ), the merged transition is (q, σ, [2, 5], b, q  ).

Learning Deterministic One-Clock Timed Automata via Mutation Testing

4.2

243

Split-Location Mutation Operator

The split-location mutation operator mainly involves modiﬁcation on locations
while not the timed information on transitions, which was ﬁrst introduced in[6] for the learning of Mealy machines. To deal with DOTAs, we make somemodiﬁcations for the operator that includes the execution of the following steps:(1) making abstraction from a DOTA to a DFA by labeling every transition witha diﬀerent abstract action u, (2) mutating the DFA using split-location operator
referring to [6], and (3) transforming the mutated DFA back to a DOTA as amutant of the original DOTA. In order to instantiate the split-location mutation
operator in our implementation and experiments, we also need two parameters:
nacc is an upper bound on the number of access sequences leading to a split
location and k is the length of a distinguishing sequence.

5

Implementation and Experiments

To further investigate the eﬃciency of the proposed method, we extend the existing DOTAs learning prototype tool in [8] with the proposed EQ implementationand evaluate it on a set of DOTAs. The experiments are meant to check whether
the proposed technique is an eﬀective implementation of equivalence oracle toﬁnd counterexamples for incorrect hypotheses under the DOTAs learning setting. The prototype tool and experiments are available on the tool page https://github.com/Anna9697/mut learn DOTAs.
5.1

Case Studies

First, we evaluated the DOTAs learning with mutation-based testing on 18 randomly generated DOTAs. We divided them into 6 groups depending on thenumber of locations (|Q|), the number of untimed actions (|Σ|), and the maximum constant appearing in the models (B). In addition, there are also threemanually created examples from the real world: a lamp touch control model(Lamp) from [5], a coﬀee vending machine model (Coﬀee) from [30], and themodel of TCP protocol (TCP) from [8].
For each case, we executed 15 times to acquire the average number of tests(#tests) and actions (#actions), the average accumulated delay time in tests(tdelay ), and the number of correct models learned (nexact ). We used the same
exact equivalence oracle in [8] to judge whether the learned automata were completely correct or not. The related parameters to run the experiments are as
follows. To generate test cases via Algorithm 1, we set parameters pstart = 0.4,
pvalid = 0.8, pstop = 0.05 and len = 2·|Q|, where |Q| is the number of locations ofmodels in each group, and sampled delay-time value at a granularity of 0.5 withthe upper bound 1.5·B. We obtain a test suite T with size |T| = 30·|QH |·|ΣH |·B
by repeatedly calling Algorithm 1, where |QH | and |ΣH | are the number of locations and actions of the current hypothesis H respectively. In the mutation generation, for the timed mutation operator, we set the slicing step w to the minimal
duration of the constraints of the models1 . While for split-location mutation
1

Set w = 1 if no additional information is known.

244

X. Tang et al.
Table 1. Experimental results of case studies.

Case ID

Mutation new#tests #actions tdelay

Mutants checking
nexact #tests #actions tdelay

Heuristic random testingnexact #tests #actions tdelay

6 2 10-1

443.1

2592.19012.3 152640.26 2 10-2559.93254.1 15934.2 15

6 2 10-3

967.1

6218.8 21540.9 15

6 2 20-1

1085.87475.5 41588.0 15

6 2 20-2

614.4

3669.9 21300.3 15

6 2 20-3

1428.38817.3 59688.2 1512931.5

40198.2

233110.7 159529.853712.3

387141.1 15

6 2 30-1

859.6

6626.6 54486.0 154244.813544.9100506.4 159238.761385.1

729274.2 15

6 2 30-2

2381.518481.1 181969.8 1543635.6 155341.7 1236780.6 15

6 2 30-31321.17378.7 68047.2 159877.727839.6

259687.3 159600.341289.2

6 4 10-1

1003.07129.3 24928.0 15

7582.019563.7

57116.9 156430.127362.5

90757.6 15

6 4 10-2

797.5

5618.1 15934.7 158857.224367.865591.0 156042.530837.7

103849.5 15

6 4 10-3805.9

5299.8 18883.0 15

9668.027604.1

60054.4 156605.833476.7

124421.4 15

6 6 10-1

1052.05822.4 19984.1 1513569.4

31987.970455.2 159058.440925.5

125318.0 15

6 6 10-2

956.8

5965.6 29055.3 1516273.2

39944.4

151809.1 1511260.350044.5

193209.0 15

6 6 10-3

1243.97204.4 25286.5 1511422.425626.368280.0 15

9161.143958.1

166033.1 15

10 2 10-1

883.7

8550.7 24911.4 15

13000.761353.5

105297.1 15

5168.239441.7

128707.0 15

10 2 10-2

1512.512905.2 38655.8 155826.226173.5

50920.1 157016.850663.2

177461.2 15

10 2 10-3

1398.512173.1 49605.8 1522901.796580.9265156.0 15

8166.563442.1

253596.7 15

5 5 10-Lamp

568.3

3396.8 18240.8 153076.38113.631719.7 1511776.951956.6

287967.0 15

4 7 10-Coﬀee

766.3

3585.8 12264.1 156329.713279.933141.1 157374.735100.8

126433.5 15

11 10 10-TCP 4525.6

26779.9 87720.3 15160482.1 480235.5

841312.0 1536427.1 206505.9

483336.1 15

nexact9295.928774.7 153372.014405.046005.1 153004.69141.636273.7 154204.320711.097402.2 159389.032769.594801.4 155640.534557.3

132976.6 1211616.642426.0171239.0 156957.636032.3

206737.9 153572.513607.7

58794.7 156885.533562.3

181704.7 1517205.5 112464.1 1346503.8 15419800.6 15

operator, we set nacc = 8 and k = 1. In the mutation-based selection of test
cases, we set the weights with a = 0.4, b = 0.4, c = 0.6, and d = 0.2 to calculate
the scores.
We refer to our mutation-based testing for DOTAs learning as Mutation
new. We also set two baseline methods, Mutants checking and Heuristic random testing. In the former, we ﬁrst generate mutants using the method in
Sect. 4 and then generate test cases by equivalence checking between the current
hypothesis and each mutant as introduced in [23]. Hence, a test case is a timed
word showing the violation of equivalence. In the latter, we directly use the test
cases T generated by repeating Algorithm 1 without any mutation or selection.
We compare our technique with the two baseline methods. To ensure the comparability of the diﬀerent techniques, the parameter settings are the same as thosementioned previously.
The experimental results of the three methods are given in Table 1. It showsthat the three methods can learn the correct model in all cases except for one failure for Heuristic random testing on model 6 2 10-3. Our method takes theleast number of test cases, actions, and accumulated delay time on all cases,
beating the two baseline methods by about an order of magnitude. Amongthe baseline methods, Mutants checking costs less on average than Heuristic random testing, but the comparison is highly variable across cases. In
order to evaluate the quality of the incorrect learned model for 6 2 10-3, we randomly generated extra 50000 test cases to test the learned model. The passing
rate is 99.27%. Additionally, we analyze why Heuristic random testing failed
once but Mutation new did not. As we know, for an EQ, Tsel is a subset of T.

Learning Deterministic One-Clock Timed Automata via Mutation Testing245

Fig. 2. Experimental results of the evaluation of improvements.

The found counterexamples for an EQ may be diﬀerent using two methods, thus
leading to diﬀerent hypotheses which will aﬀect the learning process further.
5.2

Evaluation of Improvements

We continue to use the cases in Table 1 to evaluate the improvements of thethree main contributions in the context of learning: heuristic test-case generation
method, two special mutation operators, and score-based test-case selection. The
following three experiments are conducted:
E1. Comparison of the heuristic test-case generation and the baseline.
E2. Comparison of the algorithm with and without the two mutation operators.
E3. Comparison of the mutation and score-based test-case selection, the greedy
test-case selection, and without selection.
E1. Evaluation of the Heuristic Test-Case Generation. The quality of the test
cases T obtained using heuristic test-case generation is critical, as the test cases
we execute on the system are selected from T. In order to evaluate our heuristic test-case generation method, we compare it with a purely random method(randomly select actions and delay times to form timed traces) and the A&T’s
method (another random testing approach discussed in [6]). In other words, in246

X. Tang et al.

the whole testing process, the experiments conducted only diﬀer in the test-case
generation method. For A&T’s method, we set values to the parameters in themethod as pretry = 0.9, pstop = 0.05, linfix = |Q|/2, and maxSteps = 2 · |Q|. For
each case, the original test suites generated by the three methods are of the same
size. Still, for each case, we learn the models 15 times respectively using eachmethod and observe the times of the correct models are learned. The results areshown in Fig. 2(a). It can be found that our heuristic method performs muchbetter than the other two methods on learning out correct models.
E2. Evaluation of the Two Mutation Operators. As described in Sect. 3.1, during
the process of mutation-based testing for DOTAs, we design and adopt two
kinds of mutation operators to generate mutants: timed mutation operator andsplit-location mutation operator. We would like to evaluate the eﬃciency of thetwo operators. For each case, we learn the models 15 times respectively using
only the timed mutation operator, or only the split-location operator, or both togenerate mutants, and observe the times of the correct models are learned. The
results, given in Fig. 2(b), shows that although for some cases we are able to learncorrect models 15 times using a single mutation operator, using two operators
together gives a signiﬁcant improvement on the rate of learning correct models.
Therefore, it is necessary to use both operators in mutation-based testing in thecontext of DOTAs learning.
E3. Evaluation of the Mutation and Score-Based Test-Case Selection. Our
mutation-score-based test-case selection algorithm considers various attributes
and guarantees mutation coverage at the same time. We compared the methodwith a greedy test-case selection method [6] which only guarantees that the test
suite selected provides maximum coverage of the mutants. The experiments are
conducted diﬀerently only in the selection of test cases. Running all cases without any test-case selection procedure is as the baseline. We run each experimentfor 15 times on each case and the results are shown in Fig. 2(c). Considering thenumber of times the correct model is learned, both selection methods performed
better than the baseline (this is because the found counterexamples for an EQ
are diﬀerent by diﬀerent methods, which lead to diﬀerent hypotheses and willaﬀect the learning process further). On most cases, our selection approach has
the least accumulated delay time except for case 6 6 10-3 and case 11 10 10TCP. However, for these two cases, we can still achieve better results than thegreedy test-case selection method by adjusting parameters.

6

Conclusion

We presented a conformance testing approach combining random testing andmodel-based mutation testing, which can be used for EQs in the active learningof DOTAs. The experimental results show the eﬀectiveness and eﬃciency of our
two learning-friendly mutation operators and several heuristics in the generationand selection of test cases. Since the performance depends on the instantiationof parameters and we set parameters according to our experience, one possible

Learning Deterministic One-Clock Timed Automata via Mutation Testing

247

future work is to determine automatic methods for setting or online adaption ofparameters according to the learning scenarios.

References
1. Aarts, F., Kuppens, H., Tretmans, J., Vaandrager, F., Verwer, S.: Improving active
Mealy machine learning for protocol conformance testing. Mach. Learn. 96, 189–
224 (2013). https://doi.org/10.1007/s10994-013-5405-0
2. Aichernig, B.K., et al.: Model-based mutation testing of an industrial measurement
device. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 1–19.
Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09099-3 1
3. Aichernig, B.K., Brandl, H., Jöbstl, E., Krenn, W., Schlick, R., Tiran, S.: Killing
strategies for model-based mutation testing. Softw. Test. Veriﬁcation Reliab. 25(8),716–748 (2015). https://doi.org/10.1002/stvr.1522
4. Aichernig, B.K., Lorber, F., Ničković, D.: Time for mutants—model-based mutation testing with timed automata. In: Veanes, M., Viganò, L. (eds.) TAP 2013.
LNCS, vol. 7942, pp. 20–38. Springer, Heidelberg (2013). https://doi.org/10.1007/
978-3-642-38916-0 2
5. Aichernig, B.K., Pferscher, A., Tappler, M.: From passive to active: learning timed
automata eﬃciently. 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
6. Aichernig, B.K., Tappler, M.: Eﬃcient active automata learning via mutation testing. J. Autom. Reason. 63(4), 1103–1134 (2018). https://doi.org/10.1007/s10817018-9486-0
7. Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2),
183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8
8. 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
9. 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-27674
10. An, J., Zhan, B., Zhan, N., Zhang, M.: Learning nondeterministic real-time
automata. ACM Trans. Embed. Comput. Syst. 20(5s), 1–26 (2021). https://doi.
org/10.1145/3477030
11. Andrews, J.H., Briand, L.C., Labiche, Y., Namin, A.S.: Using mutation analysis
for assessing and comparing testing coverage criteria. IEEE Trans. Software Eng.
32(8), 608–624 (2006). https://doi.org/10.1109/TSE.2006.83
12. Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput.
75(2), 87–106 (1987). https://doi.org/10.1016/0890-5401(87)90052-6
13. Berg, T., Grinchtein, O., Jonsson, B., Leucker, M., Raﬀelt, H., Steﬀen, B.: On
the correspondence between conformance testing and regular inference. In: Cerioli,
M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 175–189. Springer, Heidelberg (2005).
https://doi.org/10.1007/978-3-540-31984-9 14
14. Chow, T.: Testing software design modeled by ﬁnite-state machines. IEEE Trans.
Software Eng. 3, 178–187 (1978). https://doi.org/10.1109/TSE.1978.231496
15. En-Nouaary, A., Dssouli, R., Khendek, F.: Timed Wp-method: Testing real-timesystems. IEEE Trans. Software Eng. 28(11), 1023–1038 (2002). https://doi.org/
10.1109/TSE.2002.1049402

248

X. Tang et al.

16. Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata.
Theoret. Comput. Sci. 411(47), 4029–4054 (2010). https://doi.org/10.1016/j.tcs.
2010.07.008
17. 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-03057628-8 9
18. Howar, F., Jonsson, B., Vaandrager, F.: Combining black-box and white-box techniques for learning register automata. In: Steﬀen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 563–588. Springer, Cham (2019).
https://doi.org/10.1007/978-3-319-91908-9 26
19. Howar, F., Steﬀen, B., Merten, M.: From ZULU to RERS. In: Margaria, T., Steﬀen,
B. (eds.) ISoLA 2010. LNCS, vol. 6415, pp. 687–704. Springer, Heidelberg (2010).
https://doi.org/10.1007/978-3-642-16558-0 55
20. Isberner, M., Howar, F., Steﬀen, B.: The open-source learnlib. 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
21. Jia, Y., Harman, M.: An analysis and survey of the development of mutation
testing. IEEE Trans. Software Eng. 37(5), 649–678 (2011). https://doi.org/10.
1109/TSE.2010.62
22. Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Formal Methods Syst. Des. 34(3), 238–304 (2009). https://doi.org/10.1007/s10703-009-0065-1
23. Larsen, K.G., Lorber, F., Nielsen, B., Nyman, U.: Mutation-based test-case generation with Ecdar. In: ICST Workshops 2017, pp. 319–328. IEEE (2017). https://doi.org/10.1109/ICSTW.2017.60
24. Maler, O., Mens, I.-E.: 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
25. Peled, D.A., Vardi, M.Y., Yannakakis, M.: Black box checking. J. Autom. Lang.
Comb. 7(2), 225–246 (2002). https://doi.org/10.25596/jalc-2002-225
26. Trab, M.S.A., Counsell, S., Hierons, R.M.: Speciﬁcation mutation analysis for validating timed testing approaches based on timed automata. In: COMPSAC 2012,
pp. 660–669. IEEE Computer Society (2012). https://doi.org/10.1109/COMPSAC.
2012.93
27. Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing
approaches. Softw. Test. Veriﬁcation Reliab. 22(5), 297–312 (2012). https://doi.
org/10.1002/stvr.456
28. Vaandrager, F.: Model learning. Commun. ACM 60(2), 86–95 (2017). https://doi.
org/10.1145/2967606
29. 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
30. Van Beek, D., Man, K., Reniers, M., Rooda, J., Schiﬀelers, R.: Syntax and semantics of timed Chi. J. Symb. Comput. JSC (2005)
31. Vega, J.J.O., Perrouin, G., Amrani, M., Schobbens, P.: Model-based mutation
operators for timed systems: a taxonomy and research agenda. In: QRS 2018, pp.
325–332. IEEE (2018). https://doi.org/10.1109/QRS.2018.00045