454
J. An et al.
timed observation table T = (Σ, Σ, Σ r , S, R, E, f), where S = {}, E = {},
while for every σ ∈ Σ, he builds a logical-timed word γ = (σ, 0) and then obtains
its reset counterpart π(γ) = (σ, 0, b) by triggering a membership query to the teacher,
which is then added to R. Thereafter, the learner can fill the table by additional membership queries. Before constructing a hypothesis, the learner performs several rounds
of operations described in Sect. 3.1 until T is prepared. Then, a hypothesis H is constructed leveraging an intermediate DFA M and submitted to the teacher for an equivalence query. If the answer is positive, H recognizes the target language. Otherwise, the
learner receives a counterexample ctx and then conducts the counterexample processing to update T as described in Sect. 3.3. The whole procedure repeats until the teacher
gives a positive answer to an equivalence query.
To facilitate the analysis of correctness, termination and complexity of Algorithm 1,
we introduce the notion of symbolic state that combines each location with its clock
regions: a symbolic state of a COTA A = (Σ, Q, q 0 , F, c, Δ) is a pair (q, μ), where
q ∈ Q and μ is a region containing μ. If κ is the maximal constant appearing in
the clock constraints of A, then there exist 2κ + 2 such regions, including [n, n] with
0 ≤ n ≤ κ, (n, n+1) with 0 ≤ n < κ, and (κ, ∞) for each location, so there are a total
of |Q| × (2κ + 2) symbolic states. Then the correctness and termination of Algorithm 1
is stated in the following theorem, based on the fact that there is an injection from S (or
equivalently, the locations of H) to symbolic states of A.
Theorem 5. Algorithm 1 terminates and returns a COTA H which recognizes the target
timed language L.
3.5 Complexity
Given a target timed language L which is recognized by a COTA A, let n = |Q| be the
number of locations of A, m = |Σ| the size of the alphabet, and κ the maximal constant
appearing in the clock constraints of A. In what follows, we derive the complexity of
Algorithm 1 in terms of the number of queries.
By the proof of Theorem 5, H has at most n(2κ + 2) locations ( the size of S) distinguished by E. Thus, |E| is at most n(2κ + 2) in order to distinguish these locations.
Therefore, the number of transitions of H is bounded by mn
2
(2κ + 2)
3 . Furthermore,
as every counterexample adds at least one fresh transition to the hypothesis H, where
we consider each interval of the partition corresponds to a transition, this means that
the number of counterexamples and equivalence queries is at most mn
2
(2κ + 2)
3 .
Now, we consider the number of membership queries, that is, to compute (|S| +
|R|) × |E|. Let h be the maximal length of counterexamples returned by the teacher,
which is polynomial in the size of A according to Theorem 5 in [40], bounded by
n
2 . There are three cases of extending R by adding fresh rows, namely during the
processing of counterexamples, making T closed, and making T evidence-closed. The
first case adds at most hmn
2
(2κ + 2)
3 rows to R, while the latter two add at most
n(2κ + 2) × m and n
2
(2κ + 2)
2 , respectively, yielding that the size of R is bounded by
O(hmn
2 κ
3
), where O(·) is the big Omicron notation. As a consequence, the number of
membership queries is bounded by O(mn
5 κ
4
). So, the total complexity is O(mn
5 κ
4
).
J. An et al.
timed observation table T = (Σ, Σ, Σ r , S, R, E, f), where S = {}, E = {},
while for every σ ∈ Σ, he builds a logical-timed word γ = (σ, 0) and then obtains
its reset counterpart π(γ) = (σ, 0, b) by triggering a membership query to the teacher,
which is then added to R. Thereafter, the learner can fill the table by additional membership queries. Before constructing a hypothesis, the learner performs several rounds
of operations described in Sect. 3.1 until T is prepared. Then, a hypothesis H is constructed leveraging an intermediate DFA M and submitted to the teacher for an equivalence query. If the answer is positive, H recognizes the target language. Otherwise, the
learner receives a counterexample ctx and then conducts the counterexample processing to update T as described in Sect. 3.3. The whole procedure repeats until the teacher
gives a positive answer to an equivalence query.
To facilitate the analysis of correctness, termination and complexity of Algorithm 1,
we introduce the notion of symbolic state that combines each location with its clock
regions: a symbolic state of a COTA A = (Σ, Q, q 0 , F, c, Δ) is a pair (q, μ), where
q ∈ Q and μ is a region containing μ. If κ is the maximal constant appearing in
the clock constraints of A, then there exist 2κ + 2 such regions, including [n, n] with
0 ≤ n ≤ κ, (n, n+1) with 0 ≤ n < κ, and (κ, ∞) for each location, so there are a total
of |Q| × (2κ + 2) symbolic states. Then the correctness and termination of Algorithm 1
is stated in the following theorem, based on the fact that there is an injection from S (or
equivalently, the locations of H) to symbolic states of A.
Theorem 5. Algorithm 1 terminates and returns a COTA H which recognizes the target
timed language L.
3.5 Complexity
Given a target timed language L which is recognized by a COTA A, let n = |Q| be the
number of locations of A, m = |Σ| the size of the alphabet, and κ the maximal constant
appearing in the clock constraints of A. In what follows, we derive the complexity of
Algorithm 1 in terms of the number of queries.
By the proof of Theorem 5, H has at most n(2κ + 2) locations ( the size of S) distinguished by E. Thus, |E| is at most n(2κ + 2) in order to distinguish these locations.
Therefore, the number of transitions of H is bounded by mn
2
(2κ + 2)
3 . Furthermore,
as every counterexample adds at least one fresh transition to the hypothesis H, where
we consider each interval of the partition corresponds to a transition, this means that
the number of counterexamples and equivalence queries is at most mn
2
(2κ + 2)
3 .
Now, we consider the number of membership queries, that is, to compute (|S| +
|R|) × |E|. Let h be the maximal length of counterexamples returned by the teacher,
which is polynomial in the size of A according to Theorem 5 in [40], bounded by
n
2 . There are three cases of extending R by adding fresh rows, namely during the
processing of counterexamples, making T closed, and making T evidence-closed. The
first case adds at most hmn
2
(2κ + 2)
3 rows to R, while the latter two add at most
n(2κ + 2) × m and n
2
(2κ + 2)
2 , respectively, yielding that the size of R is bounded by
O(hmn
2 κ
3
), where O(·) is the big Omicron notation. As a consequence, the number of
membership queries is bounded by O(mn
5 κ
4
). So, the total complexity is O(mn
5 κ
4
).