Główne pojęcia
The core message of this paper is to present two active learning algorithms for deterministic timed automata (DTA) with multiple clocks. The first algorithm learns from a powerful teacher who can provide reset information, while the second algorithm learns from a normal teacher who can only answer membership and equivalence queries. The authors show that the learning problem can be reduced to learning the corresponding reset-clocked language of the target DTA, and prove the termination and correctness of the proposed algorithms.
Streszczenie
This paper presents algorithms for actively learning deterministic timed automata (DTA) with multiple clocks. The key ideas are:
The authors define an equivalence relation over the reset-clocked language of a DTA and show that it has a finite number of equivalence classes. This allows them to reduce the problem of learning the timed language of a DTA to learning its corresponding reset-clocked language.
For the case of learning from a powerful teacher, the authors introduce reset information queries in addition to membership and equivalence queries. The learner can ask the teacher about the reset information along a run, which helps in constructing the hypothesis DTA.
For the case of learning from a normal teacher who can only answer membership and equivalence queries, the learner has to guess the reset information. This results in an exponential increase in the number of table instances the learner has to handle.
The authors prove the termination and correctness of both algorithms, and provide complexity analyses in terms of the number of queries needed.
The paper also includes a preliminary implementation of the proposed learning methods.