452
J. An et al.
3.3 Equivalence query and counterexample processing
Suppose that the teacher knows a COTA A which recognizes the target timed language
L. Then to answer an equivalence query is to determine whether L(H) = L(A), which
can be divided into two timed language inclusion problems, i.e., whether L(H) ⊆
L(A) and L(A) ⊆ L(H). Most decision procedures for language inclusion proceed
by complementation and emptiness checking of the intersection [23]: L(A) ⊆ L(B) iff
L(A)∩L(B) = ∅. The fact that deterministic timed automata can be complemented [6]
enables solving the inclusion problem by checking the emptiness of the resulted product
automata H×A and H×A. The complementation technique, however, does not apply to
nondeterministic timed automata even if with only one single clock [4], which we plan
to incorporate in our learning framework in future work. We therefore opt for
2 the alternative method presented by Ouaknine and Worrell in [31] showing that the language
inclusion problem of timed automata with one clock (regardless of their determinacy)
is decidable by reduction to a reachability problem on an infinite graph. That is, there
exists a delay-timed word ω that leads to a bad configuration if L(H) L(A). In detail, the corresponding run ρ of ω ends in an accepting location in H but the counterpart
ρ
of ω in A is not accepting. Consequently, the teacher can provide the reset-delaytimed word ω r resulted from ω as a negative counterexample ctx − . Similarly, a positive counterexample ctx + = (ω r , +) can be generated if L(A) L(H). An algorithm
elaborating the equivalence query is provided in Appendix C of the full version [7].
When receiving a counterexample ctx = (ω r , +/−), the learner first converts it to
a reset-logical-timed word γ r = Γ (ω r ) = (σ 1 , μ 1 , b 1 )(σ 2 , μ 2 , b 2 ) · · · (σ n , μ n , b n ). By
definition, γ r and ω r share the same sequence of transitions in A. Furthermore, by the
contraposition of Theorem 1, γ r is an evidence for L r (H) = L r (A) if ω r is an evidence
for L(H) = L(A).
Additionally, by the definition of clock constraints Φ c , at any location, if an action σ
is enabled, i.e., its guard is satisfied, w.r.t. the clock value μ ∈ R ≥0 \N, then σ should be
enabled w.r.t. any clock value at the location, where θ ∈ (0, 1). Specifically, only
one transition is available for σ at the location on the interval μ, because the target
automaton is deterministic. Therefore, in order to avoid unnecessarily distinguishing
timed words and violating the assumptions of the list for the partition function, the
learner needs to apply a normalization function g to normalize γ r .
Definition 4 (Normalization). A normalization function g maps a reset-logical-timed
word γ r = (σ 1 , μ 1 , b 1 )(σ 2 , μ 2 , b 2 ) · · · (σ n , μ n , b n ) to another reset-logical-timed word
by resetting any logical clock to its integer part plus a constant fractional part, i.e.,
g(γ r ) = (σ 1 , μ
1 , b 1 )(σ 2 , μ
2 , b 2 ) · · · (σ n , μ
n , b n ), where μ
i = μ i if μ i ∈ N, μ
i = i
θ for some fixed constant θ ∈ (0, 1) otherwise.
We will instantiate θ = 0.1 in what follows. Clearly our approach works for any
other θ valued in (0, 1). This normalization process guarantees the assumptions needed
for Definition 3.
2 Remark that the learning complexity (Sect. 3.5) is measured in terms of the number of queries
rather than the time complexity of the specific method for checking the equivalence (nor membership). Additionally, the specific method of equivalence checking is not the main concern.
J. An et al.
3.3 Equivalence query and counterexample processing
Suppose that the teacher knows a COTA A which recognizes the target timed language
L. Then to answer an equivalence query is to determine whether L(H) = L(A), which
can be divided into two timed language inclusion problems, i.e., whether L(H) ⊆
L(A) and L(A) ⊆ L(H). Most decision procedures for language inclusion proceed
by complementation and emptiness checking of the intersection [23]: L(A) ⊆ L(B) iff
L(A)∩L(B) = ∅. The fact that deterministic timed automata can be complemented [6]
enables solving the inclusion problem by checking the emptiness of the resulted product
automata H×A and H×A. The complementation technique, however, does not apply to
nondeterministic timed automata even if with only one single clock [4], which we plan
to incorporate in our learning framework in future work. We therefore opt for
2 the alternative method presented by Ouaknine and Worrell in [31] showing that the language
inclusion problem of timed automata with one clock (regardless of their determinacy)
is decidable by reduction to a reachability problem on an infinite graph. That is, there
exists a delay-timed word ω that leads to a bad configuration if L(H) L(A). In detail, the corresponding run ρ of ω ends in an accepting location in H but the counterpart
ρ
of ω in A is not accepting. Consequently, the teacher can provide the reset-delaytimed word ω r resulted from ω as a negative counterexample ctx − . Similarly, a positive counterexample ctx + = (ω r , +) can be generated if L(A) L(H). An algorithm
elaborating the equivalence query is provided in Appendix C of the full version [7].
When receiving a counterexample ctx = (ω r , +/−), the learner first converts it to
a reset-logical-timed word γ r = Γ (ω r ) = (σ 1 , μ 1 , b 1 )(σ 2 , μ 2 , b 2 ) · · · (σ n , μ n , b n ). By
definition, γ r and ω r share the same sequence of transitions in A. Furthermore, by the
contraposition of Theorem 1, γ r is an evidence for L r (H) = L r (A) if ω r is an evidence
for L(H) = L(A).
Additionally, by the definition of clock constraints Φ c , at any location, if an action σ
is enabled, i.e., its guard is satisfied, w.r.t. the clock value μ ∈ R ≥0 \N, then σ should be
enabled w.r.t. any clock value at the location, where θ ∈ (0, 1). Specifically, only
one transition is available for σ at the location on the interval μ, because the target
automaton is deterministic. Therefore, in order to avoid unnecessarily distinguishing
timed words and violating the assumptions of the list for the partition function, the
learner needs to apply a normalization function g to normalize γ r .
Definition 4 (Normalization). A normalization function g maps a reset-logical-timed
word γ r = (σ 1 , μ 1 , b 1 )(σ 2 , μ 2 , b 2 ) · · · (σ n , μ n , b n ) to another reset-logical-timed word
by resetting any logical clock to its integer part plus a constant fractional part, i.e.,
g(γ r ) = (σ 1 , μ
1 , b 1 )(σ 2 , μ
2 , b 2 ) · · · (σ n , μ
n , b n ), where μ
i = μ i if μ i ∈ N, μ
i = i
θ for some fixed constant θ ∈ (0, 1) otherwise.
We will instantiate θ = 0.1 in what follows. Clearly our approach works for any
other θ valued in (0, 1). This normalization process guarantees the assumptions needed
for Definition 3.
2 Remark that the learning complexity (Sect. 3.5) is measured in terms of the number of queries
rather than the time complexity of the specific method for checking the equivalence (nor membership). Additionally, the specific method of equivalence checking is not the main concern.