Learning One-Clock Timed Automata
455
It is worth noting the above analysis is given in the worst case, where all partitions
need to be fully refined. But, in practice we can learn the automaton without refining
most partitions, and therefore the number of equivalence and membership queries, as
well as the number of locations in the learned automaton are much fewer than the corresponding worst-case bounds. This will be demonstrated by examples in Sect. 5.
3.6 Accelerating Trick
In the timed observation table, the function f maps invalid reset-logical-timed words as
well as certain valid ones to “−” when the teacher maintains a COTA A as the oracle.
The learner thus needs multiple rounds of queries to distinguish the “sink” location from
other unaccepting locations. If the function f is extended to map invalid reset-logicaltimed words to a distinct symbol, say “×”, when we let a DOTA A be the oracle, then
the learner will take much fewer queries. We will later show in the experiments that
such a trick significantly accelerates the learning process.
4 Learning from a Normal Teacher
In this section, we consider the problem of learning timed automata with a normal
teacher. As before, we assume the timed language to be learned comes from a complete
DOTA. For the normal teacher, inputs to membership queries are delay-timed words,
and the teacher returns whether the word is in the language (without giving any additional information). Inputs to equivalence queries are candidate DOTAs, and the teacher
either answers they are equivalent or provides a delay-timed word as a counterexample.
The algorithm here is based on the procedure in the previous section. We still maintain observation tables where the elements in S ∪ R are reset-logical-timed words and
the elements in E are logical-timed words. In order to obtain delay-timed words for the
membership queries, we need to guess clock reset information for transitions in the table. More precisely, in order to convert a logical-timed word to a delay-timed word, it is
necessary to know clock reset information for all but the last transition. Hence, it is necessary to guess reset information for each word in S ∪ R (since S ∪ R is prefix-closed,
this is equivalent to guessing reset information for the last transition of each word).
Also, for each entry in (S ∪ R) × E, it is necessary to guess all but the last transition in E. The algorithm can be thought of as exploring a search tree, where branching
is caused by guesses, and successor nodes are constructed by the usual operations of
preparing a table and dealing with a counterexample.
The detailed process is given in Algorithm 2. The learner maintains a set of table instances, named ToExplore, which contains all table instances that need to be explored.
The initial tables in ToExplore are as follows. Each table has S = E = {}. For
each σ ∈ Σ, there is one row in R corresponding to the logical-timed word ω = (σ, 0).
It is necessary to guess a reset b for each ω thereby transforming it to a reset-logicaltimed word γ r = (σ, 0, b). There are 2
|Σ| possible combinations of guesses. These
tables are filled by making membership queries (in this case, the membership queries for
each table are the same). The resulting 2
|Σ| tables form the initial tables in ToExplore.
455
It is worth noting the above analysis is given in the worst case, where all partitions
need to be fully refined. But, in practice we can learn the automaton without refining
most partitions, and therefore the number of equivalence and membership queries, as
well as the number of locations in the learned automaton are much fewer than the corresponding worst-case bounds. This will be demonstrated by examples in Sect. 5.
3.6 Accelerating Trick
In the timed observation table, the function f maps invalid reset-logical-timed words as
well as certain valid ones to “−” when the teacher maintains a COTA A as the oracle.
The learner thus needs multiple rounds of queries to distinguish the “sink” location from
other unaccepting locations. If the function f is extended to map invalid reset-logicaltimed words to a distinct symbol, say “×”, when we let a DOTA A be the oracle, then
the learner will take much fewer queries. We will later show in the experiments that
such a trick significantly accelerates the learning process.
4 Learning from a Normal Teacher
In this section, we consider the problem of learning timed automata with a normal
teacher. As before, we assume the timed language to be learned comes from a complete
DOTA. For the normal teacher, inputs to membership queries are delay-timed words,
and the teacher returns whether the word is in the language (without giving any additional information). Inputs to equivalence queries are candidate DOTAs, and the teacher
either answers they are equivalent or provides a delay-timed word as a counterexample.
The algorithm here is based on the procedure in the previous section. We still maintain observation tables where the elements in S ∪ R are reset-logical-timed words and
the elements in E are logical-timed words. In order to obtain delay-timed words for the
membership queries, we need to guess clock reset information for transitions in the table. More precisely, in order to convert a logical-timed word to a delay-timed word, it is
necessary to know clock reset information for all but the last transition. Hence, it is necessary to guess reset information for each word in S ∪ R (since S ∪ R is prefix-closed,
this is equivalent to guessing reset information for the last transition of each word).
Also, for each entry in (S ∪ R) × E, it is necessary to guess all but the last transition in E. The algorithm can be thought of as exploring a search tree, where branching
is caused by guesses, and successor nodes are constructed by the usual operations of
preparing a table and dealing with a counterexample.
The detailed process is given in Algorithm 2. The learner maintains a set of table instances, named ToExplore, which contains all table instances that need to be explored.
The initial tables in ToExplore are as follows. Each table has S = E = {}. For
each σ ∈ Σ, there is one row in R corresponding to the logical-timed word ω = (σ, 0).
It is necessary to guess a reset b for each ω thereby transforming it to a reset-logicaltimed word γ r = (σ, 0, b). There are 2
|Σ| possible combinations of guesses. These
tables are filled by making membership queries (in this case, the membership queries for
each table are the same). The resulting 2
|Σ| tables form the initial tables in ToExplore.