456
J. An et al.
Algorithm 2: Learning one-clock timed automaton with a normal teacher
input : the timed observation table T = (Σ, Σ, Σr, S, R, E, f).
output: the hypothesis H recognizing the target language L.
1 ToExplore ← ∅; S ← { R ← {π(Γ (ω)) | ω = (σ, 0), ∀σ ∈ Σ}; E ← {
2 currentTable ← (Σ, Σ, Σr, S, R, E, f);
3 tables ← guess and fill(currentTable);
// guess resets and fill all table instances
4 ToExplore.insert(tables);
// insert table instances tables into ToExplore
5 currentTable ← ToExplore.pop();
// pop out head instance as the current table
6 equivalent ← ⊥;
7 while equivalent = ⊥ do
8
prepared ← is prepared(currentTable); // whether the current table is prepared
9
while prepared = ⊥ do
10
if currentTable is not closed then
11
tables ← guess and make closed(currentTable); ToExplore.insert(tables);
12
currentTable ← ToExplore.pop();
13
if currentTable is not consistent then
14
tables ← guess and make consistent(currentTable); ToExplore.insert(tables);
15
currentTable ← ToExplore.pop();
16
if currentTable is not evidence-closed then
17
tables ← guess and make evidence closed(currentTable); ToExplore.insert(tables);
18
currentTable ← ToExplore.pop();
19
prepared ← is prepared(currentTable);
20
M ← build DFA(currentTable) ;
// transforming currentTable to a DFA M
21
H ← build hypothesis(M) ;
// constructing a hypothesis H from M
22
equivalent, ctx ← equivalence query(H);
// ctx is a delay-timed word
23
if equivalent = ⊥ then
24
tables ← guess and ctx processing(currentTable, ctx ) ;
// counterexample
processing
25
ToExplore.insert(tables);
26
currentTable ← ToExplore.pop();
27 return H;
In each iteration of the algorithm, one table instance is taken out of ToExplore.
The learner checks whether the table is closed, consistent, and evidence closed. If the
table is not closed, i.e. there exists r ∈ R such that row(r) = row(s) for all s ∈ S,
the learner moves r from R to S. Then for each σ ∈ Σ, the element r · (σ, 0) is
added to R, and a guess has to be made for its reset information. Hence, 2
|Σ| unfilled
table instances will be generated. Next, for each entry in the |Σ| new rows of R, it is
necessary to guess reset information for all but the last transition in e ∈ E. After this
guess, it is now possible to fill the table instances by making membership queries with
transformed delay-timed words. Hence, there are at most 2
(
e i ∈E\{ (|ei|−1))×|Σ| filled
table instances for one unfilled table instance. All filled table instances are inserted into
ToExplore.
If the table is not consistent, i.e. there exist some γ r , γ
r ∈ S ∪R and σ r ∈ Σ r such
that γ r ·σ r , γ
r ·σ r ∈ S ∪R and row(γ r ) = row(γ
r ), but row(γ r ·σ r ) = row(γ
r ·σ r ).
Let e ∈ E be one place where they are different. Then σ r ·e needs to be added to E. For
each entry in S ∪ R, all but the last transition in σ r · e need to be guessed, then the table
can be filled. 2
(|σ·e|−1)×(|S|+|R|) filled table instances will be generated and inserted
into ToExplore. The operation for making tables evidence-closed is analogous.
Once the current table is prepared, the learner builds a hypothesis H and makes an
equivalence query to the teacher. If the answer is positive, then H is a COTA which recognizes the target timed language L; otherwise, the teacher gives a delay-timed word
ω as a counterexample. The learner first finds the longest reset-logical-timed word in
J. An et al.
Algorithm 2: Learning one-clock timed automaton with a normal teacher
input : the timed observation table T = (Σ, Σ, Σr, S, R, E, f).
output: the hypothesis H recognizing the target language L.
1 ToExplore ← ∅; S ← { R ← {π(Γ (ω)) | ω = (σ, 0), ∀σ ∈ Σ}; E ← {
2 currentTable ← (Σ, Σ, Σr, S, R, E, f);
3 tables ← guess and fill(currentTable);
// guess resets and fill all table instances
4 ToExplore.insert(tables);
// insert table instances tables into ToExplore
5 currentTable ← ToExplore.pop();
// pop out head instance as the current table
6 equivalent ← ⊥;
7 while equivalent = ⊥ do
8
prepared ← is prepared(currentTable); // whether the current table is prepared
9
while prepared = ⊥ do
10
if currentTable is not closed then
11
tables ← guess and make closed(currentTable); ToExplore.insert(tables);
12
currentTable ← ToExplore.pop();
13
if currentTable is not consistent then
14
tables ← guess and make consistent(currentTable); ToExplore.insert(tables);
15
currentTable ← ToExplore.pop();
16
if currentTable is not evidence-closed then
17
tables ← guess and make evidence closed(currentTable); ToExplore.insert(tables);
18
currentTable ← ToExplore.pop();
19
prepared ← is prepared(currentTable);
20
M ← build DFA(currentTable) ;
// transforming currentTable to a DFA M
21
H ← build hypothesis(M) ;
// constructing a hypothesis H from M
22
equivalent, ctx ← equivalence query(H);
// ctx is a delay-timed word
23
if equivalent = ⊥ then
24
tables ← guess and ctx processing(currentTable, ctx ) ;
// counterexample
processing
25
ToExplore.insert(tables);
26
currentTable ← ToExplore.pop();
27 return H;
In each iteration of the algorithm, one table instance is taken out of ToExplore.
The learner checks whether the table is closed, consistent, and evidence closed. If the
table is not closed, i.e. there exists r ∈ R such that row(r) = row(s) for all s ∈ S,
the learner moves r from R to S. Then for each σ ∈ Σ, the element r · (σ, 0) is
added to R, and a guess has to be made for its reset information. Hence, 2
|Σ| unfilled
table instances will be generated. Next, for each entry in the |Σ| new rows of R, it is
necessary to guess reset information for all but the last transition in e ∈ E. After this
guess, it is now possible to fill the table instances by making membership queries with
transformed delay-timed words. Hence, there are at most 2
(
e i ∈E\{ (|ei|−1))×|Σ| filled
table instances for one unfilled table instance. All filled table instances are inserted into
ToExplore.
If the table is not consistent, i.e. there exist some γ r , γ
r ∈ S ∪R and σ r ∈ Σ r such
that γ r ·σ r , γ
r ·σ r ∈ S ∪R and row(γ r ) = row(γ
r ), but row(γ r ·σ r ) = row(γ
r ·σ r ).
Let e ∈ E be one place where they are different. Then σ r ·e needs to be added to E. For
each entry in S ∪ R, all but the last transition in σ r · e need to be guessed, then the table
can be filled. 2
(|σ·e|−1)×(|S|+|R|) filled table instances will be generated and inserted
into ToExplore. The operation for making tables evidence-closed is analogous.
Once the current table is prepared, the learner builds a hypothesis H and makes an
equivalence query to the teacher. If the answer is positive, then H is a COTA which recognizes the target timed language L; otherwise, the teacher gives a delay-timed word
ω as a counterexample. The learner first finds the longest reset-logical-timed word in