448
J. An et al.
q0
start
q1
a, (1, 3), ⊥
b, [0, ∞),
b, [2, 4),
q0
start
q1
qs
a, (1, 3), ⊥
b, [0, ∞),
b, [2, 4),
a , [0 , 1 ],
a , [3 , ∞
) ,
a , [ 0 , ∞
) ,
b , [ 0 , 2 ) ,
b , [ 4 , ∞
) ,
a, [0, ∞),
b, [0, ∞),
Fig. 1: A DOTA A on the left and the corresponding COTA A on the right. The initial location is
indicated by ‘start’ and an accepting location is doubly circled.
Theorem 1. Given two DOTAs A and B, if L r (A) = L r (B), then L(A) = L(B).
Theorem 1 assures that L r (H) = L r (A) implies L(H) = L(A), that is, to construct
a COTA A that recognizes a target timed language L = L(A), it suffices to learn a hypothesis H which recognizes the same reset-logical timed language. For equivalence
queries, instead of checking directly whether L r (H) = L r (A), the contraposition of
Theorem 1 guarantees that we can perform equivalence queries over their timed counterparts: if L(H) = L(A), then H recognizes the target language already; otherwise, a
counterexample making L(H) = L(A) yields an evidence also for L r (H) = L r (A).
We now describe the behavior of the teacher who keeps an automaton A to be learnt,
while providing knowledge about the automaton by answering membership and equivalence queries through an oracle she maintains. For the membership query, the teacher
receives a logical-timed word γ and returns whether γ is in L(A). In addition, she is
smart enough to return the reset-logical-timed word γ r that corresponds to γ (the exact correspondence is described in Sect. 3.1). For the equivalence query, the teacher is
given a hypothesis H and decides whether L(H) = L(A). If not, she is smart enough
to return a reset-delayed-timed word ω r as a counterexample. The usual case where a
teacher can deal with only standard delay-timed words will be discussed in Sect. 4.
Remark 1. The assumption that the teacher can respond with timed words coupled with
reset information is reasonable, in the sense that the learner can always infer and detect
the resets of the logical clock by referring to a global clock on the wall, as long as he can
observe running states of A, i.e., observing the clock valuation of the system whenever
an event happens therein. This conforms with the idea of combining automata learning
with white-box techniques, as exploited in [24], providing that in many application
scenarios source code is available for the analysis.
In what follows, we elaborate the learning procedure including membership queries,
hypotheses construction, equivalence queries and counterexample processing.
3.1 Membership query
In our setting, the oracle maintained by the smart teacher can be regarded as a COTA
A that recognizes the target timed language L, and thereby its logical-timed language
L(A) and reset-logical-timed counterpart L r (A). In order to collect enough information
J. An et al.
q0
start
q1
a, (1, 3), ⊥
b, [0, ∞),
b, [2, 4),
q0
start
q1
qs
a, (1, 3), ⊥
b, [0, ∞),
b, [2, 4),
a , [0 , 1 ],
a , [3 , ∞
) ,
a , [ 0 , ∞
) ,
b , [ 0 , 2 ) ,
b , [ 4 , ∞
) ,
a, [0, ∞),
b, [0, ∞),
Fig. 1: A DOTA A on the left and the corresponding COTA A on the right. The initial location is
indicated by ‘start’ and an accepting location is doubly circled.
Theorem 1. Given two DOTAs A and B, if L r (A) = L r (B), then L(A) = L(B).
Theorem 1 assures that L r (H) = L r (A) implies L(H) = L(A), that is, to construct
a COTA A that recognizes a target timed language L = L(A), it suffices to learn a hypothesis H which recognizes the same reset-logical timed language. For equivalence
queries, instead of checking directly whether L r (H) = L r (A), the contraposition of
Theorem 1 guarantees that we can perform equivalence queries over their timed counterparts: if L(H) = L(A), then H recognizes the target language already; otherwise, a
counterexample making L(H) = L(A) yields an evidence also for L r (H) = L r (A).
We now describe the behavior of the teacher who keeps an automaton A to be learnt,
while providing knowledge about the automaton by answering membership and equivalence queries through an oracle she maintains. For the membership query, the teacher
receives a logical-timed word γ and returns whether γ is in L(A). In addition, she is
smart enough to return the reset-logical-timed word γ r that corresponds to γ (the exact correspondence is described in Sect. 3.1). For the equivalence query, the teacher is
given a hypothesis H and decides whether L(H) = L(A). If not, she is smart enough
to return a reset-delayed-timed word ω r as a counterexample. The usual case where a
teacher can deal with only standard delay-timed words will be discussed in Sect. 4.
Remark 1. The assumption that the teacher can respond with timed words coupled with
reset information is reasonable, in the sense that the learner can always infer and detect
the resets of the logical clock by referring to a global clock on the wall, as long as he can
observe running states of A, i.e., observing the clock valuation of the system whenever
an event happens therein. This conforms with the idea of combining automata learning
with white-box techniques, as exploited in [24], providing that in many application
scenarios source code is available for the analysis.
In what follows, we elaborate the learning procedure including membership queries,
hypotheses construction, equivalence queries and counterexample processing.
3.1 Membership query
In our setting, the oracle maintained by the smart teacher can be regarded as a COTA
A that recognizes the target timed language L, and thereby its logical-timed language
L(A) and reset-logical-timed counterpart L r (A). In order to collect enough information