Learning One-Clock Timed Automata
453
T5
−
(a, 1.1, ⊥) +
(a, 0, −
(b, 0, −
(a, 1.1, ⊥)(a, 0, −
(a, 1.1, ⊥)(b, 0, −
(a, 1.1, ⊥)(b, 2, +
(a, 3, −
ωr=(a,0,)(a,1.3,
= =========== =⇒
γr=(a,0,)(a,1.3,
T6
−
(a, 1.1, ⊥) +
(a, 0, −
(b, 0, −
(a, 1.1, ⊥)(a, 0, −
(a, 1.1, ⊥)(b, 0, −
(a, 1.1, ⊥)(b, 2, +
(a, 3, −
(a, 0, )(a, 1.3, −
q−
start
q+
(a, 0,
(a, 3,
(a, 1.3,
(b, 0,
(a, 1.1, ⊥)
(b, 2,
(a, 0,
(b, 0,
M6
Fig. 3: An illustration of the necessity of normalization by the normalization function.
Algorithm 1: Learning one-clock timed automaton with a smart teacher
input : the timed observation table T = (Σ, Σ, Σr, S, R, E, f).
output: the hypothesis H recognizing the target language L.
1 S ← { R ← {Γ (ω) | ω = (σ, 0), ∀σ ∈ Σ}; E ← { ;
// initialization
2 fill T by membership queries;
3 equivalent ← ⊥;
4 while equivalent = ⊥ do
5
prepared ← is prepared(T) ;
// whether the table is prepared
6
while prepared = ⊥ do
7
if T is not closed then make closed(T) ;
8
if T is not consistent then make consistent(T) ;
9
if T is not evidence-closed then make evidence closed(T) ;
10
prepared ← is prepared(T);
11
M ← build DFA(T) ;
// transforming T to a DFA M
12
H ← build hypothesis(M) ;
// constructing a hypothesis H from M
13
equivalent, ctx ← equivalence query(H);
14
if equivalent = ⊥ then
15
ctx processing(T, ctx ) ;
// counterexample processing
16 return H;
Example 3. Consider the prepared table T 5 in Fig. 3 (as in Fig. 2). When the leaner asks
an equivalence query with hypothesis H 5 , the teacher answers that L(H 5 ) = L(A),
where A in Fig. 1 is the target automaton, and provides a counterexample (ω r , −) with
ω r = (a, 0, )(a, 1.3, which can be transformed to a reset-logical-timed word γ r =
(a, 0, )(a, 1.3, If he adds prefixes of γ r to the table directly, the learner will get a
prepared table T 6 and thus construct a DFA M 6 . Unfortunately, the partition function
defined in Definition 3 is not applicable to (a, 1.3, and (a, 1.1, ⊥) any more. On
the other hand, if he adds the prefixes of the normalized reset-logical-timed word, i.e.,
γ
r = (a, 0, )(a, 1.1, to T 5 , the learner will then get an inconsistent table whose
consistency can be retrieved by the operation of “making T consistent” as expected.
The following theorem guarantees that the normalized reset-logical-timed word γ
r
is also an evidence for L r (H) = L r (A). Therefore, the learner can use it as a counterexample and thus adds all the prefixes of γ
r to R except those already in S ∪ R.
Theorem 4. Given a valid reset-logical-timed word γ r of A, its normalization γ
r =
g(γ r ) shares the same sequence of transitions in A.
3.4 Learning algorithm
We present in Algorithm 1 the learning procedure integrating all the previously stated
ingredients, including preparing the table, membership and equivalence queries, hypothesis construction and counterexample processing. The learner first initializes the
453
T5
−
(a, 1.1, ⊥) +
(a, 0, −
(b, 0, −
(a, 1.1, ⊥)(a, 0, −
(a, 1.1, ⊥)(b, 0, −
(a, 1.1, ⊥)(b, 2, +
(a, 3, −
ωr=(a,0,)(a,1.3,
= =========== =⇒
γr=(a,0,)(a,1.3,
T6
−
(a, 1.1, ⊥) +
(a, 0, −
(b, 0, −
(a, 1.1, ⊥)(a, 0, −
(a, 1.1, ⊥)(b, 0, −
(a, 1.1, ⊥)(b, 2, +
(a, 3, −
(a, 0, )(a, 1.3, −
q−
start
q+
(a, 0,
(a, 3,
(a, 1.3,
(b, 0,
(a, 1.1, ⊥)
(b, 2,
(a, 0,
(b, 0,
M6
Fig. 3: An illustration of the necessity of normalization by the normalization function.
Algorithm 1: Learning one-clock timed automaton with a smart teacher
input : the timed observation table T = (Σ, Σ, Σr, S, R, E, f).
output: the hypothesis H recognizing the target language L.
1 S ← { R ← {Γ (ω) | ω = (σ, 0), ∀σ ∈ Σ}; E ← { ;
// initialization
2 fill T by membership queries;
3 equivalent ← ⊥;
4 while equivalent = ⊥ do
5
prepared ← is prepared(T) ;
// whether the table is prepared
6
while prepared = ⊥ do
7
if T is not closed then make closed(T) ;
8
if T is not consistent then make consistent(T) ;
9
if T is not evidence-closed then make evidence closed(T) ;
10
prepared ← is prepared(T);
11
M ← build DFA(T) ;
// transforming T to a DFA M
12
H ← build hypothesis(M) ;
// constructing a hypothesis H from M
13
equivalent, ctx ← equivalence query(H);
14
if equivalent = ⊥ then
15
ctx processing(T, ctx ) ;
// counterexample processing
16 return H;
Example 3. Consider the prepared table T 5 in Fig. 3 (as in Fig. 2). When the leaner asks
an equivalence query with hypothesis H 5 , the teacher answers that L(H 5 ) = L(A),
where A in Fig. 1 is the target automaton, and provides a counterexample (ω r , −) with
ω r = (a, 0, )(a, 1.3, which can be transformed to a reset-logical-timed word γ r =
(a, 0, )(a, 1.3, If he adds prefixes of γ r to the table directly, the learner will get a
prepared table T 6 and thus construct a DFA M 6 . Unfortunately, the partition function
defined in Definition 3 is not applicable to (a, 1.3, and (a, 1.1, ⊥) any more. On
the other hand, if he adds the prefixes of the normalized reset-logical-timed word, i.e.,
γ
r = (a, 0, )(a, 1.1, to T 5 , the learner will then get an inconsistent table whose
consistency can be retrieved by the operation of “making T consistent” as expected.
The following theorem guarantees that the normalized reset-logical-timed word γ
r
is also an evidence for L r (H) = L r (A). Therefore, the learner can use it as a counterexample and thus adds all the prefixes of γ
r to R except those already in S ∪ R.
Theorem 4. Given a valid reset-logical-timed word γ r of A, its normalization γ
r =
g(γ r ) shares the same sequence of transitions in A.
3.4 Learning algorithm
We present in Algorithm 1 the learning procedure integrating all the previously stated
ingredients, including preparing the table, membership and equivalence queries, hypothesis construction and counterexample processing. The learner first initializes the