Learning One-Clock Timed Automata
447
word is also called delay-timed word. The corresponding reset-delay-timed word can
be defined as trace r (ρ) = (σ 1 , t 1 , b 1 )(σ 2 , t 2 , b 2 ) · · · (σ n , t n , b n ), where b i is the reset
indicator for δ i , for 1 ≤ i ≤ n. If ρ is an accepting run of A, trace(ρ) is called an accepting timed word. The recognized timed language of A is the set of accepting delay-timed
words, i.e., L(A) = {trace(ρ) | ρ is an accepting run of A}. The recognized reset-timed
language L r (A) is defined as {trace r (ρ) | ρ is an accepting run of A}.
The delay-timed word ω = (σ 1 , t 1 )(σ 2 , t 2 ) · · · (σ n , t n ) is observed outside, from
the view of the global clock. On the other hand, the behavior can also be observed
inside, from the view of the local clock. This results in a logical-timed word of the form
γ = (σ 1 , μ 1 )(σ 2 , μ 2 ) · · · (σ n , μ n ) with μ i = t i if i = 1 ∨ b i−1 = and μ i = μ i−1 + t i
otherwise. We will denote the mapping from delay-timed words to logical-timed words
above by Γ .
Similarly, we introduce reset-logical-timed word γ r = (σ 1 , μ 1 , b 1 )(σ 2 , μ 2 , b 2 ) · · ·
(σ n , μ n , b n ) as the counterpart of ω r = (σ 1 , t 1 , b 1 )(σ 2 , t 2 , b 2 ) · · · (σ n , t n , b n ) in terms
of the local clock. Without any substantial change, we can extend the mapping Γ to map
reset-delay-timed words to reset-logical-timed words. The recognized logical-timed
language of A is given as L(A) = {Γ (trace(ρ)) | ρ is an accepting run of A}, and
the recognized reset-logical-timed language of A as L r (A) = {Γ (trace r (ρ)) | ρ is an
accepting run of A}.
An OTA is a deterministic one-clock timed automaton (DOTA) if there is at most
one run for a given delay-timed word. In other words, for any location q ∈ Q and action
σ ∈ Σ, the guards of transitions outgoing from q labelled with σ are disjoint subsets of
R ≥0 . We say a DOTA is complete if for any of its location q ∈ Q and action σ ∈ Σ,
the corresponding guards form a partition of R ≥0 . This means any given delay-timed
word has exactly one run. Any DOTA A can be transformed into a complete DOTA
(referred to as COTA) A accepting the same timed language as follows: (1) Augment Q
with a “sink” location q s which is not an accepting location; (2) For every q ∈ Q and
σ ∈ Σ, if there is no outgoing transition from q labelled with σ, introduce a (resetting)
transition from q to q s with label σ and guard [0, ∞); (3) Otherwise, let S be the subset
of R ≥0 not covered by the guards of transitions from q with label σ. Write S as a union
of intervals I 1 , . . . , I k in a minimal way, then introduce a (resetting) transition from q
to q s with label σ and guard I j for each 1 ≤ j ≤ k.
From now on, we therefore assume that we are working with COTAs.
Example 1. Fig. 1 depicts the transformation of a DOTA A (left part) into a COTA A
(right part). First, a non-accepting “sink” location q s is introduced. Second, we introduce three fresh transitions (marked in blue) from q 1 to q s as well as transitions from
q s to itself. At last, for location q 0 and label a, the existing guards cover (1, 3), with
complement [0, 1] ∪ [3, ∞). Hence, we introduce transitions (q 0 , a, [0, 1], , q s ) and
(q 0 , a, [3, ∞), , q s ). Two fresh transitions from q 1 to q s are introduced similarly.
3 Learning from a Smart Teacher
In this section, we consider the case of learning a COTA A with a smart teacher. Our
learning algorithm relies on the following reduction of the equivalence over timed languages to that of reset-logical timed languages.
447
word is also called delay-timed word. The corresponding reset-delay-timed word can
be defined as trace r (ρ) = (σ 1 , t 1 , b 1 )(σ 2 , t 2 , b 2 ) · · · (σ n , t n , b n ), where b i is the reset
indicator for δ i , for 1 ≤ i ≤ n. If ρ is an accepting run of A, trace(ρ) is called an accepting timed word. The recognized timed language of A is the set of accepting delay-timed
words, i.e., L(A) = {trace(ρ) | ρ is an accepting run of A}. The recognized reset-timed
language L r (A) is defined as {trace r (ρ) | ρ is an accepting run of A}.
The delay-timed word ω = (σ 1 , t 1 )(σ 2 , t 2 ) · · · (σ n , t n ) is observed outside, from
the view of the global clock. On the other hand, the behavior can also be observed
inside, from the view of the local clock. This results in a logical-timed word of the form
γ = (σ 1 , μ 1 )(σ 2 , μ 2 ) · · · (σ n , μ n ) with μ i = t i if i = 1 ∨ b i−1 = and μ i = μ i−1 + t i
otherwise. We will denote the mapping from delay-timed words to logical-timed words
above by Γ .
Similarly, we introduce reset-logical-timed word γ r = (σ 1 , μ 1 , b 1 )(σ 2 , μ 2 , b 2 ) · · ·
(σ n , μ n , b n ) as the counterpart of ω r = (σ 1 , t 1 , b 1 )(σ 2 , t 2 , b 2 ) · · · (σ n , t n , b n ) in terms
of the local clock. Without any substantial change, we can extend the mapping Γ to map
reset-delay-timed words to reset-logical-timed words. The recognized logical-timed
language of A is given as L(A) = {Γ (trace(ρ)) | ρ is an accepting run of A}, and
the recognized reset-logical-timed language of A as L r (A) = {Γ (trace r (ρ)) | ρ is an
accepting run of A}.
An OTA is a deterministic one-clock timed automaton (DOTA) if there is at most
one run for a given delay-timed word. In other words, for any location q ∈ Q and action
σ ∈ Σ, the guards of transitions outgoing from q labelled with σ are disjoint subsets of
R ≥0 . We say a DOTA is complete if for any of its location q ∈ Q and action σ ∈ Σ,
the corresponding guards form a partition of R ≥0 . This means any given delay-timed
word has exactly one run. Any DOTA A can be transformed into a complete DOTA
(referred to as COTA) A accepting the same timed language as follows: (1) Augment Q
with a “sink” location q s which is not an accepting location; (2) For every q ∈ Q and
σ ∈ Σ, if there is no outgoing transition from q labelled with σ, introduce a (resetting)
transition from q to q s with label σ and guard [0, ∞); (3) Otherwise, let S be the subset
of R ≥0 not covered by the guards of transitions from q with label σ. Write S as a union
of intervals I 1 , . . . , I k in a minimal way, then introduce a (resetting) transition from q
to q s with label σ and guard I j for each 1 ≤ j ≤ k.
From now on, we therefore assume that we are working with COTAs.
Example 1. Fig. 1 depicts the transformation of a DOTA A (left part) into a COTA A
(right part). First, a non-accepting “sink” location q s is introduced. Second, we introduce three fresh transitions (marked in blue) from q 1 to q s as well as transitions from
q s to itself. At last, for location q 0 and label a, the existing guards cover (1, 3), with
complement [0, 1] ∪ [3, ∞). Hence, we introduce transitions (q 0 , a, [0, 1], , q s ) and
(q 0 , a, [3, ∞), , q s ). Two fresh transitions from q 1 to q s are introduced similarly.
3 Learning from a Smart Teacher
In this section, we consider the case of learning a COTA A with a smart teacher. Our
learning algorithm relies on the following reduction of the equivalence over timed languages to that of reset-logical timed languages.